rev-rev proof -- Answer to Question 1
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
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 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.
