Inductive Properties of Lists, Part 2

page 2

1 2 3 x

Inductive Properties of Lists, Part 2
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 use associativity of the operation append . Click here to see its proof.
We show rev(append(cons(n0 , l0) , l2)) = append(rev(l2) , rev(cons(n0 , l0))) by reduction.

And thus the main goal is proved.

Explanation

The most notable point about this proof is the now invisible fact that the need for it, as well as for the lemma that it uses (the associativity of append), were discovered from the failed proof attempts in our previous proofweb for the main goal, that reversing a list twice yields the original list.

It is also worth noting that when the associativity of append is used as a lemma, it is in the implicit form of the associativity attribute, rather than the explicit application of the associativity equation as a rewrite rule. The way that the associativity lemma is entered into the computational context can be seen in the BOBJ proof score for the present lemma; it has the form of an operator declaration,

op append : List List -> List [ assoc idr: nil ] .

which overwrites the previous declaration for append without the assoc attribute.

Left Up Down Right

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