Inductive Properties of Lists, Part 1

page 3

1 2 3 x

Inductive Properties of Lists, Part 1
Associativity of Append

We want to prove
( L1 L2 L3 : List ) append(append(L1 , L2) , L3) = append(L1 , append(L2 , L3)) .
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, l3 : List .
We show append(append(nil , l2) , l3) = append(nil , append(l2 , l3)) 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 L3 : List ) append(append(l0 , L2) , L3) = append(l0 , append(L2 , L3)) .
Quantifier elimination introduces the new constant(s) n0 : Nat .
Quantifier elimination introduces the new constant(s) l2, l3 : List .
We show append(append(cons(n0 , l0) , l2) , l3) = append(cons(n0 , l0) , append(l2 , l3)) by reduction.

And thus the main goal is proved.

Explanation

Since this proof attempt succeeds, our quest for a proof of the original goal would appear to be finished. This impression is confirmed by our second proof website for this goal, where trying to prove the three results in the reverse order of that in which they were discovered does in fact prove the original goal.

Left Up Down Right

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