On palindromes

Défine the inductive predicate palindrome associated to lists that can be read the same way in both directions.

Solution

Note

We added to the end of this file a proof that a list is palindromic (according to the inductive definition) if and only if it is equal to its own reverse (defined by the function rev in PolyList).

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.