Proving that a reversible list is a palindrome in Coq

Question

Here is my inductive definition of palindromes:

Inductive pal { X : Type } : list X -> Prop :=
  | pal0 : pal []
  | pal1 : forall ( x : X ), pal [x]
  | pal2 : forall ( x : X ) ( l : list X ), pal l -> pal ( x :: l ++ [x] ).

And the theorem I want to prove, from Software Foundations:

Theorem rev_eq_pal : forall ( X : Type ) ( l : list X ),
  l = rev l -> pal l.

My informal outlines of the proof are as follows:

Suppose l0 is an arbitrary list such that l0 = rev l0. Then one of the following three cases must hold. l0 has:

(a) zero elements, in which case it is a palindrome by definition.

(b) one element, in which case it is also a palindrome by definition.

(c) two elements or more, in which case l0 = x :: l1 ++ [x] for some element x and some list l1 such that l1 = rev l1.

Now, since l1 = rev l1, one of the following three cases must hold...

The recursive case analysis will terminate for any finite list l0 because the length of the list analyzed decreases by 2 through each iteration. If it terminates for any list ln, all of its outer lists up to l0 are also palindromes, since a list constructed by appending two identical elements at either end of a palindrome is also a palindrome.

I think the reasoning is sound, but I'm not sure how to formalize it. Can it be turned into a proof in Coq? Some explanations of how the tactics used work would be especially helpful.

Answer 1

This is a nice example where "direct" induction does not work well at all because you don't directly make the recursive call on the tail, but on part of the tail. In such cases, I usually advice to state your lemma with the length of the list, not on the list itself. You can then specialize it. That would be something like:

Lemma rev_eq_pal_length: forall (X: Type) (n: nat) (l: list X), length l <= n -> l = rev l -> pal l.
Proof.
(* by induction on [n], not [l] *)
Qed.

Theorem rev_eq_pal: forall (X: Type) (l: list X), l = rev l -> pal l.
Proof.
(* apply the previous lemma with n = length l *)
Qed.

I can help you in more detail if necessary, just leave a comment.

Good luck !

V.

EDIT: just to help you, I needed the following lemmas to make this proof, you might need them too.

Lemma tool : forall (X:Type) (l l': list X) (a b: X),                                                                                                         
            a :: l = l' ++ b :: nil -> (a = b /\ l = nil) \/ exists k, l = k ++ b :: nil.

Lemma tool2 : forall (X:Type) (l1 l2 : list X) (a b: X),                                                                                                         
     l1 ++ a :: nil = l2 ++ b :: nil -> a = b /\ l1 = l2.