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

**Principle of Structural Induction:**
Let ` ψ` be the term representing a conjecture.

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) ={deftree-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 `nil`s, `mapnil1`
is commutative.”

**Problem 52. ** Define

**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

**Problem 57. ** Define

**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: