Major Section: BIND-FREE
See bind-free for a basic discussion of the use of
bind-free to control
Note that the examples below all illustrate the common case in which a
bind-free hypothesis generates a binding alist. See bind-free, in
particular the final section, for a discussion of the case that instead a
list of binding alists is generated.
We give examples of the use of
bind-free hypotheses from the
perspective of a user interested in reasoning about arithmetic, but
it should be clear that
bind-free can be used for many other
EXAMPLE 1: Cancel a common factor.
(defun bind-divisor (a b) ; If a and b are polynomials with a common factor c, we return a ; binding for x. We could imagine writing get-factor to compute the ; gcd, or simply to return a single non-invertible factor. (let ((c (get-factor a b))) (and c (list (cons 'x c))))) (defthm cancel-factor ;; We use case-split here to ensure that, once we have selected ;; a binding for x, the rest of the hypotheses will be relieved. (implies (and (acl2-numberp a) (acl2-numberp b) (bind-free (bind-divisor a b) (x)) (case-split (not (equal x 0))) (case-split (acl2-numberp x))) (iff (equal a b) (equal (/ a x) (/ b x)))))
EXAMPLE 2: Pull integer summand out of floor. Note: This example
has an extended
bind-free hypothesis, which uses the term
(find-int-in-sum sum mfc state).
(defun fl (x) ;; This function is defined, and used, in the IHS books. (floor x 1)) (defun int-binding (term mfc state) ;; The call to mfc-ts returns the encoded type of term. ; ;; Thus, we are asking if term is known by type reasoning to ; ;; be an integer. ; (declare (xargs :stobjs (state) :mode :program)) (if (ts-subsetp (mfc-ts term mfc state) *ts-integer*) (list (cons 'int term)) nil)) (defun find-int-in-sum (sum mfc state) (declare (xargs :stobjs (state) :mode :program)) (if (and (nvariablep sum) (not (fquotep sum)) (eq (ffn-symb sum) 'binary-+)) (or (int-binding (fargn sum 1) mfc state) (find-int-in-sum (fargn sum 2) mfc state)) (int-binding sum mfc state))) ; Some additional work is required to prove the following. So for ; purposes of illustration, we wrap skip-proofs around the defthm. (skip-proofs (defthm cancel-fl-int ;; The use of case-split is probably not needed, since we should ;; know that int is an integer by the way we selected it. But this ;; is safer. (implies (and (acl2-numberp sum) (bind-free (find-int-in-sum sum mfc state) (int)) (case-split (integerp int))) (equal (fl sum) (+ int (fl (- sum int))))) :rule-classes ((:rewrite :match-free :all))) ) ; Arithmetic libraries will have this sort of lemma. (defthm hack (equal (+ (- x) x y) (fix y))) (in-theory (disable fl)) (thm (implies (and (integerp x) (acl2-numberp y)) (equal (fl (+ x y)) (+ x (fl y)))))
EXAMPLE 3: Simplify terms such as (equal (+ a (* a b)) 0)
(defun factors (product) ;; We return a list of all the factors of product. We do not ;; require that product actually be a product. (if (eq (fn-symb product) 'BINARY-*) (cons (fargn product 1) (factors (fargn product 2))) (list product))) (defun make-product (factors) ;; Factors is assumed to be a list of ACL2 terms. We return an ;; ACL2 term which is the product of all the ellements of the ;; list factors. (cond ((atom factors) ''1) ((null (cdr factors)) (car factors)) ((null (cddr factors)) (list 'BINARY-* (car factors) (cadr factors))) (t (list 'BINARY-* (car factors) (make-product (cdr factors)))))) (defun quotient (common-factors sum) ;; Common-factors is a list of ACL2 terms. Sum is an ACL2 term each ;; of whose addends have common-factors as factors. We return ;; (/ sum (make-product common-factors)). (if (eq (fn-symb sum) 'BINARY-+) (let ((first (make-product (set-difference-equal (factors (fargn sum 1)) common-factors)))) (list 'BINARY-+ first (quotient common-factors (fargn sum 2)))) (make-product (set-difference-equal (factors sum) common-factors)))) (defun intersection-equal (x y) (cond ((endp x) nil) ((member-equal (car x) y) (cons (car x) (intersection-equal (cdr x) y))) (t (intersection-equal (cdr x) y)))) (defun common-factors (factors sum) ;; Factors is a list of the factors common to all of the addends ;; examined so far. On entry, factors is a list of the factors in ;; the first addend of the original sum, and sum is the rest of the ;; addends. We sweep through sum, trying to find a set of factors ;; common to all the addends of sum. (declare (xargs :measure (acl2-count sum))) (cond ((null factors) nil) ((eq (fn-symb sum) 'BINARY-+) (common-factors (intersection-equal factors (factors (fargn sum 1))) (fargn sum 2))) (t (intersection-equal factors (factors sum))))) (defun simplify-terms-such-as-a+ab-rel-0-fn (sum) ;; If we can find a set of factors common to all the addends of sum, ;; we return an alist binding common to the product of these common ;; factors and binding quotient to (/ sum common). (if (eq (fn-symb sum) 'BINARY-+) (let ((common-factors (common-factors (factors (fargn sum 1)) (fargn sum 2)))) (if common-factors (let ((common (make-product common-factors)) (quotient (quotient common-factors sum))) (list (cons 'common common) (cons 'quotient quotient))) nil)) nil)) (defthm simplify-terms-such-as-a+ab-=-0 (implies (and (bind-free (simplify-terms-such-as-a+ab-rel-0-fn sum) (common quotient)) (case-split (acl2-numberp common)) (case-split (acl2-numberp quotient)) (case-split (equal sum (* common quotient)))) (equal (equal sum 0) (or (equal common 0) (equal quotient 0))))) (thm (equal (equal (+ u (* u v)) 0) (or (equal u 0) (equal v -1))))