		Search-engine friendly clone of the ACL2 documentation.

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)))))