page 2 1 2 3 x

Inductive Properties of Lists, Part 1
Reverse Append Lemma

 We want to prove ( L1  L2  : List  ) rev(append(L1 , L2)) = append(rev(L2) , rev(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: Base case: prove the assertion for L1 = nil . Quantifier elimination introduces the new constant(s) l2 : List  . We show rev(append(nil , l2)) = append(rev(l2) , rev(nil)) by reduction. 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 ( L2  : List  ) rev(append(l0 , L2)) = append(rev(L2) , rev(l0)) . Quantifier elimination introduces the new constant(s) n0 : Nat  . Quantifier elimination introduces the new constant(s) l2 : List  . We try to show rev(append(cons(n0 , l0) , l2)) = append(rev(l2) , rev(cons(n0 , l0))) by reduction. But reduction gives the following normal forms:     append(append(rev(l2) , rev(l0)) , cons(n0 , nil))     append(rev(l2) , append(rev(l0) , cons(n0 , nil))) . Therefore the subgoal may be false, or may require one or more new lemmas. And thus the main goal is not proved.

 Explanation It is obvious that equality of the two terms resulting from reduction is an instance of the associative law for append, which therefore seems to be the appropriate lemma for completing this proof. The next proof page of this proofweb attempts this, and in fact, succeeds.

 Left    Up    Down    Right

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