helphome pageduck scriptspecificationfirst proof pagepage 1 1 2 3 xpage 2

Inductive Properties of Lists, Part 1
The Doubly Reversed List Equation


We want to prove
( L1  : List  ) rev(rev(L1)) = L1 .
We use induction on L1 to prove this goal. For this, we use the induction scheme based on the signature { nil, cons } for List. Induction requires that we do the following:
  1. Base case: prove the assertion for L1 = nil .
  2. Induction case: assume the assertion for L1 = L0 , and then prove it for L1 = cons(N0 , L0) .
    • Quantifier elimination introduces the new constant(s) l0 : List  .
    • Implication elimination assumes rev(rev(l0)) = l0 .
    • Quantifier elimination introduces the new constant(s) n0 : Nat  .
    • We try to show rev(rev(cons(n0 , l0))) = cons(n0 , l0) by reduction.
      But reduction gives the following normal forms:
          rev(append(rev(l0) , cons(n0 , nil)))
          cons(n0 , l0) .
      Therefore the subgoal may be false, or may require one or more new lemmas.

And thus the main goal is not proved.

Explanation

First note that in the syntax of the list spec that we are given, the one element list [n0] appears as cons(n0, nil). If we write the two terms that we need to be equal in order to complete the proof as an equation using the simpler notation, with · as append, then we get
rev(rev(L1) · [n0]) = [n0] · L1 ,
To prove this, it would suffice, given the inductive hypothesis (which the proof page also conveniently displays for us) to know the following more symmetrical result,
rev(L1 · [n0]) = [n0] · rev(L1) .
Although we could prove and then use this, we might as well it generalize to
rev(L1 · L2) = rev(L2) · rev(L1) ,
which is itself an interesting result about reversing lists.

It is now reasonable to hope that proving the above first as a lemma will allow us to prove our original goal. That this is so is demonstrated in our second proofweb. The second proof page of the current proofweb shows a first attempt to prove the above lemma.


BOBJ proof scoreLeft    Up    Down    Right   
 

       This page was generated by Kumo on Mon Nov 20 10:18:44 PST 2000.