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
.
Show
rev(rev(nil)) = nil
by reduction.
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