helphome pageduck scriptspecificationfirst proof page

Inductive Properties of Lists, Part 1

Suppose we are given a spec for lists with a list reversing function, and that we want to prove the equation
(L1 : List) rev(rev(L1)) = L1 .
Then about the simplest non-trivial proof score we could give just suggests using induction on L1 with the basis { nil, cons }, which is exactly what appears in the Duck proof score for this goal, which is named <<RevRevThm>>.

Unfortunately, this proof attempt fails, but examining the result of its final reduction suggests a lemma that should be able to finish the proof. This lemma is given in the Duck proof score as the goal named <<RevAppLem>>, with the same minimal inductive proof command.

Unfortunately it also fails, but once again the nature of the failure suggests a lemma, which this time is the associative law for append, given in the Duck proof score as the goal named <<AppAssocThm>>, with once again the same minimal inductive proof command.

This proof attempt succeeds. Therefore we may hope that if these three goals are combined in just the opposite order, we will be able to prove our original goal. In fact, this works, as shown in our second proofweb for this goal.

The explanations associated to the first two proof pages of this proofweb show in detail how to infer the necessary lemmas from the corresponding proof failures.

To the Kumo demos homepage.
To the Tatami Project homepage.
To the UCSD Meaning and Computation Group homepage.

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