This proof is quite interesting, because we needed to build some tools to achieve it :

- In order to prove that
`(palindromic l)`implies`(rev l)=l`, we had to prove an inversion theorem about the extraction of the last element of a list (lemma`remove_last_inv`) and a commutation lemma between`app`and`rev`. - 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.

- Finally, we proved two lemmas of regularity of
`app`Lemma app_left_reg : forall l l1 l2:list A, l ++ l1 = l ++ l2 -> l1 = l2. Lemma app_right_reg : forall l l1 l2:list A, l1 ++ l = l2 ++ l -> l1 = l2.

The first lemma is proved by a simple induction on`l`, the second one comes directly*via*properties of the`rev`function (taken from`PolyList`). A direct proof by induction both on`l1`and`l2`would have been too long.

Going home

Pierre Castéran