		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Logic-knowledge-taken-for-granted-q1-answer

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

The correct answer to Question 1 in logic-knowledge-taken-for-granted is Choice (iv).

The Induction Step of the inductive proof of

(implies (true-listp z)
         (equal (rev (rev z)) z))

for an induction on the linear list z is:

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

The second hypothesis above is the induction hypothesis. The conclusion above is the formula we are trying to prove. Each induction hypothesis is always an instance of the formula being proved, i.e., it is obtained from the formula being proved by uniformly replacing the variables in the formula with terms. Notice how the induction hypothesis above is the same as the induction conclusion, except that all the zs have been replaced by (cdr z).

If you thought the right answer was

Induction Step -- Choice (i): 
(implies (not (endp z)) 
         (implies (true-listp z) 
                  (equal (rev (rev z)) z)))

then perhaps you didn't understand that we're doing an inductive proof. Certainly if you prove the Base Case already discussed and you prove Choice (i) above, then you will have proved the goal conjecture, but you would have done it by simple case analysis: prove it when (endp z) and prove it when (not (endp z)). While logically valid, you probably can't prove Choice (i) directly because you have no induction hypothesis to work with.

If you thought the right answer was:

Induction Step -- Choice (ii): 
(implies (true-listp (cdr z)) 
         (equal (rev (rev (cdr z))) (cdr z)))

then perhaps you misunderstand the difference between the Induction Step and the Induction Hypothesis. The Induction Step is the ``other half'' of the main proof, balancing the Base Case. The Induction Hypothesis is just a hypothesis you get to use during the Induction Step. The question Q1 asked what is the Induction Step.

If you thought the right answer was:

Induction Step -- Choice (iii): 
(implies (and (not (endp z)) 
              (equal (rev (rev (cdr x))) (cdr x))) ; ``induction hyp'' 
         (implies (true-listp z) 
                  (equal (rev (rev z)) z)))

then you are making the most common mistake newcomers make to induction. You are giving yourself an ``induction hypothesis'' that is not an instance of the conjecture you're proving. This alleged induction hypothesis says that (rev (rev (cdr x))) is (cdr x), whereas the correct induction hypothesis says those two terms are equal if (true-listp (cdr x)). This alleged induction hypothesis is a stronger claim than we're trying to prove. It turns out that by making this mistake you can ``prove'' conjectures that are not always true! Remember: the induction hypothesis is always an instance of the conjecture you're proving, not just some piece of it. Of course, ACL2 ``knows'' this and will never make this mistake. But we remind you of it because there may be times when you intuit a different hypothesis and don't understand why ACL2 doesn't use it.

If this doesn't make sense, perhaps you should read about induction again.

When you understand why Choice (iv) is the correct answer, use your browser's Back Button to return to logic-knowledge-taken-for-granted and go to question Q2.