### LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-Q1-ANSWER

the inductive step of the `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 `z`

s 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.