Inductive Properties of Lists, Part 2

page 3

1 2 3 x

Inductive Properties of Lists, Part 2
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:

Base case: prove the assertion for L1 = nil .

We show rev(rev(nil)) = 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

rev(rev(l0)) = l0 .
Quantifier elimination introduces the new constant(s) n0 : Nat .
We use associativity of the operation append . Click here to see its proof.
We introduce the lemma

( L1 L2 : List ) rev(append(L1 , L2)) = append(rev(L2) , rev(L1)).

Click here to see its proof.
We show rev(rev(cons(n0 , l0))) = cons(n0 , l0) by reduction.

And thus the main goal is proved.

Explanation

The main point of note about this proof is that the lemma that it uses was discovered from the failed direct attempt for the original goal in our previous proofweb for the same result.

Note that, as on the previous proofpage, the associativity lemma is used in an implicit way, as an attribute of append.

Left Up Down Right

This page was generated by Kumo on Tue Feb 13 19:34:15 PST 2001.