The proof of the converse was quite harder, since palindromes are
built by adding items at both ends of a list, and the lisp-like definition
of lists considers only insertion at the beginning (constructor cons).
The way we proceeded was to prove first an induction principle for lists,
considering insertions at both ends :
Lemma list_new_ind :
forall P:list A -> Prop,
P nil ->
(forall a:A, P (a :: nil)) ->
(forall (a b:A) (l:list A), P l -> P (a :: l ++ b :: nil)) ->
forall l:list A, P l.
The proof of this induction principle uses the "Fibonacci induction scheme" :
Lemma fib_ind :
forall P:nat -> Prop,
P 0 ->
P 1 ->
(forall n:nat, P n -> P (S n) -> P (S (S n))) ->
forall n:nat, P n.