Doubly Reverse List

We want to prove

L1:List (rev(rev(L1)) = L1) .
We use induction on List to prove this goal. For this, we use the induction scheme based on signature {nil,cons} for List . Induction requires that we do the following:
  • Base case : prove assertion for L1 = nil .
  • Induction case : prove assertion for L1 = cons(M,L) assume it for L1 = L .
    • Introduce the lemma L1,L2:List (rev(append(L1,L2)) = append(rev(L2), rev(L1))) .
    • Change hypothesis L1,L2:List (rev(append(L1,L2)) = append(rev(L2), rev(L1))) to rewritng rule.
    • Quantifier elimination introduces new constants m :Nat and l :List .
    • Implication elimination assumes rev(rev(l)) = l .
    • Change hypothesis rev(rev(l)) = l to rewritng rule.
    • Show rev(rev(cons(m,l))) = cons(m,l) by reduction.


This page was generated
by Kumo on Mon Jun 01 16:26:05 PDT 1998