We want to prove
(  L1
L2
: List
)
rev(append(L1 , L2)) = append(rev(L2) , rev(L1)) .
We use induction on
L1
to prove this goal.
For this, we use the
induction
scheme based on the signature
{
nil, cons
}
for
List.
Induction requires that we do the following:
-
Base case: prove the assertion for
L1
=
nil
.
-
Induction case: assume the assertion for
L1
=
L0
,
and then prove it for
L1
=
cons(N0 , L0)
.
-
Quantifier
elimination introduces the new constant(s)
l0
:
List
.
-
Implication elimination
assumes
( L2
: List
)
rev(append(l0 , L2)) = append(rev(L2) , rev(l0))
.
-
Quantifier
elimination introduces the new constant(s)
n0
:
Nat
.
-
Quantifier
elimination introduces the new constant(s)
l2
:
List
.
-
We try to show
rev(append(cons(n0 , l0) , l2)) = append(rev(l2) , rev(cons(n0 , l0)))
by
reduction.
But reduction gives the following normal forms:
append(append(rev(l2) , rev(l0)) , cons(n0 , nil))
append(rev(l2) , append(rev(l0) , cons(n0 , nil))) .
Therefore the subgoal may be false,
or may require one or more new lemmas.
And thus the main goal is not proved.
|
1 2 3 x
