		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Logic-knowledge-taken-for-granted-q2-answer

The inductive step of the rev-rev proof — Answer to Question 2

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 Subgoal (ii), Subgoal (iii), Subgoal (iv), or combinations of those three. You must also prove Subgoal (i) or something like it!

The Inductive Step for the conjecture above is

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

Note that the Inductive Hypothesis is an implication:

(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 ``forgettable'' case.

In this case, the Induction Step simplifies to

Induction Step: 
(implies (and (not (endp z)) 
              (not (true-listp (cdr z)))) 
         (implies (true-listp z) 
                  (equal (rev (rev z)) z)))

By Promotion (see the list of tautologies in our discussion of propositional calculus) this is

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

Using the Contrapositive and rearranging the order of the hypotheses (see propositional calculus again), this is

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

Notice that Subgoal (i) implies Induction Step'':

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'))
--->
  q

It is then very common to prove that p implies p',

(i): 
(c & p) ---> p'

and then prove that q' implies q,

(ii): 
(c & p & q') ---> q

These correspond exactly to our choices Subgoal (i) and Subgoal (ii).

It is sometimes helpful to remember this diagram:

(c  &  (p'  --->  q')
        ^         |
        |         |
        |         v
 -->   (p   --->  q )

When you understand why Subgoals (i) and (ii) are sufficient, use your browser's Back Button to return to logic-knowledge-taken-for-granted and go to question Q3.