a small proof demonstrating functional instantiation

The example below demonstrates the use of functional instantiation, that is, the use of a generic result in proving a result about specific functions. In this example we constrain a function to be associative and commutative, with an identity or ``root,'' on a given domain. Next, we define a corresponding function that applies the constrained associative-commutative function to successive elements of a list. We then prove that the latter function gives the same value when we first reverse the elements of the list. Finally, we use functional instantiation to derive the corresponding result for the function that multiplies successive elements of a list.

The details of the proof (such as the in-theory event and particulars of the lemmas) are not the point here. Rather, the point is to demonstrate the interaction of encapsulate events and :functional-instance lemma-instances. Of course, if you are interested in details then you may find it helpful to run these events through ACL2.

Also see constraint for more about :functional-instance and see lemma-instance for general information about the use of previously-proved lemmas.

(in-package "ACL2")

(encapsulate (((ac-fn * *) => *) ((ac-fn-domain *) => *) ((ac-fn-root) => *)) (local (defun ac-fn (x y) (+ x y))) (local (defun ac-fn-root () 0)) (local (defun ac-fn-domain (x) (acl2-numberp x))) (defthm ac-fn-comm (equal (ac-fn x y) (ac-fn y x))) (defthm ac-fn-assoc (equal (ac-fn (ac-fn x y) z) (ac-fn x (ac-fn y z)))) (defthm ac-fn-id (implies (ac-fn-domain x) (equal (ac-fn (ac-fn-root) x) x))) (defthm ac-fn-closed (and (ac-fn-domain (ac-fn x y)) (ac-fn-domain (ac-fn-root)))))

; End of encapsulate.

(defun ac-fn-list (x) (if (atom x) (ac-fn-root) (ac-fn (car x) (ac-fn-list (cdr x)))))

(in-theory (disable (ac-fn-list)))

(defun ac-fn-domain-list (x) (if (atom x) t (and (ac-fn-domain (car x)) (ac-fn-domain-list (cdr x)))))

(defun rev (x) (if (atom x) nil (append (rev (cdr x)) (list (car x)))))

(defthm ac-fn-list-closed (ac-fn-domain (ac-fn-list x)))

(defthm ac-fn-list-append (implies (and (ac-fn-domain-list x) (ac-fn-domain-list y)) (equal (ac-fn-list (append x y)) (ac-fn (ac-fn-list x) (ac-fn-list y)))))

(defthm ac-fn-domain-list-rev (equal (ac-fn-domain-list (rev x)) (ac-fn-domain-list x)))

(defthm ac-fn-list-rev (implies (ac-fn-domain-list x) (equal (ac-fn-list (rev x)) (ac-fn-list x))))

(defun times-list (x) (if (atom x) 1 (* (car x) (times-list (cdr x)))))

(defun acl2-number-listp (x) (if (atom x) t (and (acl2-numberp (car x)) (acl2-number-listp (cdr x)))))

(defthm times-list-rev (implies (acl2-number-listp x) (equal (times-list (rev x)) (times-list x))) :hints (("Goal" :use ((:functional-instance ac-fn-list-rev ;; Instantiate the generic functions: (ac-fn (lambda (x y) (* x y))) (ac-fn-root (lambda () 1)) (ac-fn-domain acl2-numberp) ;; Instantiate the other relevant functions: (ac-fn-list times-list) (ac-fn-domain-list acl2-number-listp))))))