|
We are given a spec for lists with a list reversing function, and we want
to prove the equation
(In our previous attempt to do this, we found that we needed a lemma relating rev with append, and then in our attempt to prove that lemma, we found that we also needed another lemma, asserting the associativity of append. This proofweb proves all three results, by tackling them in the reverse order of that in which they were uncovered, that is, starting with the associativity of append, then using that to prove the lemma relating reverse and append, and finally using that lemma to prove the goal stated above. All three proofs are simple inductions on the basis consisting of the list constructors, and there is nothing remarkable here except the now invisible fact that the correct proof was constructed from the failed proof attempts of the previous proofweb for this goal. |
|
To the Kumo
demos homepage. To the Tatami Project homepage. To the UCSD Meaning and Computation Group homepage. |
L1
: List) rev(rev(L1)) = L1 .