Theorem prover ACL2 –handout– Some primitive (built-in) functions (cons x y) constructs the ordered pair x, y (car x) left component of x, if x is a pair; nil otherwise (cdr x) right component of x, if x is a pair; nil otherwise (consp x) t if x is a pair; nil otherwise (if x y z) z if x is nil; y otherwise (equal x y) t if x is y; nil otherwise Some primitive (built-in) axioms 1. t = nil 2. x = nil → (if x y z) = y 3. x = nil → (if x y z) = z 4. (equal x y) = nil ∨ (equal x y) = t 5. x = y ↔ (equal x y) = t 6. (consp x) = nil ∨ (consp x) = t 7. (consp (cons x y)) = t 8. (consp nil) = (consp t) = (consp ’ok) = (consp 0) = (consp 1) = . . . = nil 9. (car (cons x y)) = x 10. (cdr (cons x y)) = y 11. (consp x) = t → (cons (car x) (cdr x)) = x Function definition (defun f (a1 a2 . . . an) β) creates the function f with arguments a1, a2, . . . , an and body β (Built-in) Lisp definitions of standard logic connectives (defun not (p) (if p nil t)) (defun and (p q) (if p q nil)) (defun or (p q) (if p p q)) (defun implies (p q) (if p (if q t nil) t)) (defun iff (p q) (and (implies p q) (implies qp))) Examples of recursive function definitions dup - duplicates each element in a list app - concatenates two lists (defun dup (x) (if (consp x) (cons (car x) (cons (car x) (dup (cdr x)))) nil)) (defun app (x y) (if (consp x) (cons (car x) (app (cdr x) y)) y)) A simple proof (defun treecopy (x) (if (consp x) (cons (treecopy (car x)) (treecopy (cdr x))) x)) Theorem: (equal (treecopy x) x)). Proof: Name the formula above *1. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (treecopy x). This suggestion was produced using the induction rule treecopy. If we let (ϕ x) denote *1 above then the induction scheme we’ll use is (and (implies (not (consp x)) (ϕ x)) (implies (and (consp x) (ϕ (car x)) (ϕ (cdr x))) (ϕ x))). This induction is justified by the same argument used to admit treecopy. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 (implies (not (consp x)) (equal (treecopy x) x)). But simplification reduces this to t, using the definition treecopy and primitive type reasoning. Subgoal *1/1 (implies (and (consp x) (equal (treecopy (car x)) (car x)) (equal (treecopy (cdr x)) (cdr x))) (equal (treecopy x) x)). But simplification reduces this to t, using the definition treecopy, primitive type reasoning and the rewrite rule cons-car-cdr. That completes the proof of *1. Q.E.D. Simplification of Subgoal *1/1 (treecopy x) = (if (consp x) ; treecopy definition (cons (treecopy (car x)) (treecopy (cdr x))) x) = (if t ; hypothesis 1 (cons (treecopy (car x)) (treecopy (cdr x))) x) = (cons (treecopy (car x)) ; axioms 1 and 2 (treecopy (cdr x))) = (cons (car x) ; hypothesis 2 (treecopy (cdr x))) = (cons (car x) ; hypothesis 3 (cdr x)) = x ; axiom 11 and hypothesis 1 For more information visit http://www.cs.utexas.edu/moore/acl2/