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 - namely
the one that unwinds the recursion in 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, namely, the size of x is
decreasing according to a certain well-founded relation. When applied to the goal at hand the above
induction scheme produces the following two nontautological subgoals.
Subgoal *1/2
(implies (not (consp x))
(equal (treecopy x) x)).
But simplification reduces this to t, using the definition of treecopy and the primitive axioms.
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 of treecopy, and the primitive axioms.
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/