helphome pageduck scriptspecificationfirst proof page

Inductive Properties of Lists, Part 2

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

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