Major Section: TUTORIAL5-MISCELLANEOUS-EXAMPLES
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. ;
;;;;;;;;;;;;;;;;;;;;;;;
; Define a ``fold'' function that iteratively applies ac-fn over a list.
(defun ac-fn-list (x)
(if (atom x)
(ac-fn-root)
(ac-fn (car x)
(ac-fn-list (cdr x)))))
; Recognize lists all of whose elements are in the intended domain.
(defun ac-fn-domain-list (x)
(if (atom x)
t
(and (ac-fn-domain (car x))
(ac-fn-domain-list (cdr x)))))
; Define a list reverse function.
(defun rev (x)
(if (atom x)
nil
(append (rev (cdr x))
(list (car x)))))
; The following is needed for proving ac-fn-list-append, which is
; needed for proving ac-fn-list-rev.
(defthm ac-fn-list-closed
(ac-fn-domain (ac-fn-list x)))
; Needed for proving ac-fn-list-rev:
(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)))))
; Needed for proving ac-fn-list-rev:
(defthm ac-fn-domain-list-rev
(equal (ac-fn-domain-list (rev x))
(ac-fn-domain-list x)))
; The following is a good idea because without it, the proof attempt
; for ac-fn-list-rev (see just below) fails with the term (HIDE
; (AC-FN-LIST NIL)). It is often a good idea to disable
; executable-counterparts of functions that call constrained
; functions.
(in-theory (disable (:executable-counterpart ac-fn-list)))
(defthm ac-fn-list-rev
(implies (ac-fn-domain-list x)
(equal (ac-fn-list (rev x))
(ac-fn-list x))))
; Our goal now is to apply functional instantiation to ac-fn-list-rev
; in order to prove the corresponding theorem, times-list-rev, based
; on * instead of ac-fn.
(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)))))
; The following relies on the following built-in rules for * (whose
; statements correspond directly to their names): commutativity-of-*,
; associativity-of-*, and unicity-of-1.
(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 *)
(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))))))
