# Equal-by-logbitp

Show a = b by showing their bits are equal.

Equal-by-logbitp may be functionally instantiated to prove
(equal a b) by showing that:

(equal (logbitp bit a) (logbitp bit b))

for any arbitrary bit less than the maximum integer-length of
a or b, where a and b are known to be integers.

This unusual (but occasionally useful) proof strategy is similar to the
*pick-a-point* proofs found in the ordered sets or ubdd libraries.

There are a couple of ways to invoke the hint. First, you might manually
appeal to the theorem using a hint such as:

:use ((:functional-instance equal-by-logbitp
(logbitp-hyp (lambda () my-hyps))
(logbitp-lhs (lambda () my-lhs))
(logbitp-rhs (lambda () my-rhs))))

But this can be irritating if your particular hyps, lhs, and rhs are large
or complex terms. See the equal-by-logbitp-hint computed hint, which
can generate the appropriate :functional-instance automatically.

### Definitions and Theorems

**Theorem: **logbitp-constraint

(defthm logbitp-constraint
(implies (and (logbitp-hyp)
(natp bit)
(<= bit
(max (integer-length (logbitp-lhs))
(integer-length (logbitp-rhs)))))
(equal (logbitp bit (logbitp-lhs))
(logbitp bit (logbitp-rhs)))))

**Theorem: **equal-by-logbitp

(defthm equal-by-logbitp
(implies (logbitp-hyp)
(equal (ifix (logbitp-lhs))
(ifix (logbitp-rhs)))))