`rev-rev`

proof -- Answer to Question 2
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

The correct answer to Question 2 in
logic-knowledge-taken-for-granted is *Subgoal (i)*
plus any one of the other other three. For your reference, the
four choices were:

Subgoal (i): (implies (and (not (endp z)) (true-listp z)) (true-listp (cdr z)))Subgoal (ii): (implies (and (not (endp z)) (true-listp z) (equal (rev (rev (cdr z))) (cdr z))) (equal (rev (rev z)) z))Subgoal (iii): (implies (and (not (endp z)) (equal (rev (rev (cdr z))) (cdr z))) (equal (rev (rev z)) z))Subgoal (iv): (implies (and (not (endp z)) (true-listp (cdr z)) (equal (rev (rev (cdr z))) (cdr z))) (equal (rev (rev z)) z))

In particular, it is wrong to think the Induction Step of the proof of

(implies (true-listp z) (equal (rev (rev z)) z))can be established by proving just

The Inductive Step for the conjecture above is

Note that the Inductive Hypothesis is an implication:Induction Step: (implies (and (not (endp z)) ;Induction Hypothesis: (implies (true-listp (cdr z)) (equal (rev (rev (cdr z))) (cdr z)))) ;Induction Conclusion: (implies (true-listp z) (equal (rev (rev z)) z)))

(implies (true-listp (cdr z)) (equal (rev (rev (cdr z))) (cdr z)))This hypothesis can be true two different ways. The ``normal'' way -- the way everybody remembers -- is that

`(true-listp (cdr z))`

is true and thus
`(equal (rev (rev (cdr z))) (cdr z))`

is true. But the way many people
forget is that `(true-listp (cdr z))`

is false. You must prove the
Induction Step even in this ``forgetable'' case.In this case, the Induction Step simplifies to

By Promotion (see the list of tautologies in our discussion of propositional calculus) this isInduction Step: (implies (and (not (endp z)) (not (true-listp (cdr z)))) (implies (true-listp z) (equal (rev (rev z)) z)))

Using the Contrapositive and rearranging the order of the hypotheses (see propositional calculus again), this isInduction Step': (implies (and (not (endp z)) (not (true-listp (cdr z))) (true-listp z)) (equal (rev (rev z)) z))

Notice thatInduction Step'': (implies (and (not (endp z)) (true-listp z) (not (equal (rev (rev z)) z))) (true-listp (cdr z)))

Subgoal (i): (implies (and (not (endp z)) (truelistp z)) (truelistp (cdr z)))

Every inductive proof of an implication raises a case like this.
If we denote the conjecture `(implies p q)`

as `p ---> q`

, then
the Induction Step will look like this:

( c & (p' ---> q')) ---> (p ---> q)where

`c`

is the test that determines the inductive step, (e.g., `(not (endp z))`

)
and `p'`

and `q'`

are inductive instances of `p`

and `q`

. Promotion produces
( c & p & (p' ---> q')) ---> qIt is then very common to prove that

`p`

implies `p'`

,
and then prove that(i): (c & p) ---> p'

`q'`

implies `q`

,
These correspond exactly to our choices(ii): (c & p & q') ---> q

It is sometimes helpful to remember this diagram:

(c & (p' ---> q') ^ | | | | v --> (p ---> q )When you understand why