|
Suppose we are given a spec for lists with a list reversing function, and that we
want to prove the equation
(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
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 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. |
L1
: List) rev(rev(L1)) = L1 .