|
|
|---|
|
|
|
|---|
Recursion and Induction: Structural Induction
Problem 39.
Given the definition
(defun f (x)
(if (consp x)
(f (cdr x))
t))
can you prove the theorem (equal (f x) t) using the logical machinery we have described so far?
ACL2 supports inductive proofs. Its Induction Principle is quite general and involves the notion of the ordinals and well-foundedness. We use a much simpler principle for now.
A substitution σ is a car/cdr substitution on v if the binding (image) of v under σ is a car/cdr nest around v. The other bindings of σ are unrestricted. For example, σ = {x ← (car x), y ← (cons (cdr x) y)} is a car/cdr substitution on x.
Principle of Structural Induction: Let ψ be the term representing a conjecture. ψ may be proved by selecting an “induction” variable x, selecting a set of car/cdr substitutions on x σ_1, … , σ_n, and by proving the following subgoals:
Base Case:
(implies (not (consp x))
ψ)
and
Induction Step:
(implies (and (consp x) ; test
ψ/σ_1 ; induction hypothesis 1
.
.
.
ψ/σ_n) ; induction hypothesis n
ψ) ; induction conclusion
Here is an example Induction Step.
(implies (and (consp x)
ψ/{x ← (car x), y ← (app x y)}
ψ/{x ← (cdr (cdr x)), y ← (cons x y)}
ψ/{x ← (cdr (cdr x)), y ← y})
ψ)
Let us use structural induction to prove a theorem about tree-copy. Recall the definition.
(defun tree-copy (x)
(if (consp x)
(cons (tree-copy (car x))
(tree-copy (cdr x)))
x))
Theorem (equal (tree-copy x) x).
Proof.
Name the formula above *1.
We prove *1 by induction. One induction scheme is suggested by this conjecture – namely the one that unwinds the recursion in tree-copy.
If we let ψ denote *1 above then the induction scheme we'll use is
(and (implies (not (consp x))
ψ)
(implies (and (consp x)
ψ/{x ← (car x)}
ψ/{x ← (cdr x)})
ψ)).
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 (tree-copy x) x)).
But simplification reduces this to t, using the definition of tree-copy and the primitive axioms.
Subgoal *1/1
(implies (and (consp x) ; hyp 1
(equal (tree-copy (car x)) (car x)) ; hyp 2
(equal (tree-copy (cdr x)) (cdr x))) ; hyp 3
(equal (tree-copy x) x)).
But simplification reduces this to t, using the definition of tree-copy and the primitive axioms.
That completes the proof of *1.
Q.E.D.
Let us look more closely at the reduction of Subgoal *1/1. Consider the left-hand side of the concluding equality. Here is how it reduces to the right-hand side under the hypotheses.
(tree-copy x)
= {def tree-copy}
(if (consp x)
(cons (tree-copy (car x))
(tree-copy (cdr x)))
x)
= {hyp 1 and Axiom 6}
(if t
(cons (tree-copy (car x))
(tree-copy (cdr x)))
x)
= {Axioms 2 and 1}
(cons (tree-copy (car x))
(tree-copy (cdr x)))
= {hyp 2}
(cons (car x)
(tree-copy (cdr x)))
= {hyp 3}
(cons (car x)
(cdr x))
= {Axioms 11 and 6 and hyp 1}
x
This proof is of a very routine nature: induct so as to unwind some particular function appearing in the conjecture and then use the axioms and definitions to simplify each case to t.
The problems below refer to function symbols defined in previous exercises. Try to prove them for the definitions you wrote. But if you cannot, then use the definitions we use in our solutions. For each conjecture below that is not a theorem, show a counterexample and then try to write the theorem “suggested” by the conjecture. For example, add a hypothesis that restricts some variable so that the conjecture holds; you may even need to introduce new concepts.
Warning: Proving implications by induction is a little tricky. Suppose you're trying to prove (implies (p x) (q x)) by induction and you choose the substitution that replaces x by (cdr x). So the Induction Step will be
Induction Step.
(implies (and (consp x)
(implies (p (cdr x)) (q (cdr x))))
(implies (p x) (q x))).
By propositional calculus, this is the same as
(implies (and (consp x)
(implies (p (cdr x)) (q (cdr x)))
(p x))
(q x)).
Many students act like the induction hypothesis is that (q (cdr x)) is true and use that to show (q x) is true. But the induction hypothesis is actually (implies (p (cdr x)) (q (cdr x))). It tells us that (q (cdr x)) is true if (p (cdr x)) is true! So it often happens that you will use the (p x) hypothesis to prove (p (cdr x)) is true. Only then can you use (q (cdr x)) to work on (q x).
Problem 40.
Prove
(equal (app (app a b) c) (app a (app b c))).
Problem 41.
Prove
(equal (app a nil) a)
Problem 42.
Prove
(equal (mapnil (app a b)) (app (mapnil a) (mapnil b)))
Problem 43.
Prove
(equal (rev (mapnil x)) (mapnil (rev x)))
Problem 44.
Prove
(equal (rev (rev x)) x)
Problem 45.
Prove
(equal (swap-tree (swap-tree x)) x)
Problem 46.
Prove
(equal (mem e (app a b)) (or (mem e a) (mem e b)))
Problem 47.
Prove
(equal (mem e (int a b)) (and (mem e a) (mem e b)))
Problem 48.
Prove
(sub a a)
Problem 49.
Prove
(implies (and (sub a b)
(sub b c))
(sub a c))
Problem 50.
Prove
(sub (app a a) a)
Problem 51.
Define
(defun mapnil1 (x a)
(if (consp x)
(mapnil1 (cdr x) (cons nil a))
a))
Formalize and then prove the remark “On lists of nils, mapnil1 is commutative.”
Problem 52.
Define (perm x y) so that it returns t if lists x and
y are permutations of each other; otherwise it returns nil.
Problem 53.
Prove
(perm x x)
Problem 54.
Prove
(implies (perm x y) (perm y x)).
Problem 55.
Prove
(implies (and (perm x y)
(perm y z))
(perm x z))
For several of the problems below it is necessary to have a total ordering relation. Let <<= be a non-strict total order, i.e., a Boolean function that enjoys the following properties:
(and (<<= x x) ; Reflexive
(implies (and (<<= x y) ; Anti-symmetric
(<<= y x))
(equal x y))
(implies (and (<<= x y) ; Transitive
(<<= y z))
(<<= x z))
(or (<<= x y) ; Total
(<<= y x)))
Actually, there is such a function in ACL2 and it is called lexorder. But we use the more suggestive name “<<=” here. On the integers, <<= is just <=, but it orders all ACL2 objects.
Problem 56.
Define (ordered x) so that it returns t or nil according to
whether each pair of adjacent elements of x are in the relation
<<=. For example, (ordered '(1 3 3 7 12)) would
evauluate to t and
(ordered '(1 3 7 3 12)) would evaluate to nil.
Problem 57.
Define (isort x) to take an arbitrary list and return an
ordered permutation of it.
Problem 58.
Prove
(ordered (isort x)).
Problem 59.
Prove
(perm (isort x) x).
Problem 60.
Prove
(equal (isort (rev (isort x)))
(isort x)).
We thank Pete Manolios for suggesting this problem.
Problem 61.
Define
(defun rev1 (x a)
(if (consp x)
(rev1 (cdr x) (cons (car x) a))
a))
Prove
(equal (rev1 x nil) (rev x))
Problem 62.
Prove
(equal (mapnil1 x nil) (mapnil x))
Problem 63.
Prove
(not (equal x (cons x y)))
Problem 64.
Define
(defun mcflatten (x a)
(if (consp x)
(mcflatten (car x)
(mcflatten (cdr x) a))
(cons x a)))
Prove
(equal (mcflatten x nil) (flatten x))
Next: