Proving that a reversible list is a palindrome in Coq

You could also derive your induction principle from a form of well-founded induction.

Notation " [ ] " := nil : list_scope.
Notation " [ x1 ; .. ; x2 ] " := (cons x1 .. (cons x2 nil) ..) : list_scope.
Open Scope list_scope.

Conjecture C1 : forall t1 f1 p1, (forall x1, (forall x2, f1 x2 < f1 x1 -> p1 x2) -> p1 x1) -> forall x1 : t1, p1 x1.
Conjecture C2 : forall t1 p1, p1 [] -> (forall x1 l1, p1 ([x1] ++ l1)) -> forall l1 : list t1, p1 l1.
Conjecture C3 : forall t1 p1, p1 [] -> (forall x1 l1, p1 (l1 ++ [x1])) -> forall l1 : list t1, p1 l1.
Conjecture C4 : forall t1 (x1 x2 : t1) l1, length l1 < length ([x1] ++ l1 ++ [x2]).

Theorem T1 : forall t1 p1,
  p1 [] ->
  (forall x1, p1 [x1]) ->
  (forall x1 x2 l1, p1 l1 -> p1 ([x1] ++ l1 ++ [x2])) ->
  forall l1 : list t1, p1 l1.
Proof.
intros t1 p1 h1 h2 h3.
induction l1 as [l1 h4] using (C1 (list t1) (@length t1)).
induction l1 as [| x1 l1] using C2.
eapply h1.
induction l1 as [| x2 l1] using C3.
simpl.
eapply h2.
eapply h3.
eapply h4.
eapply C4.
Qed.

You can prove conjecture C1 by first applying the hypothesis to the conclusion, then using structural induction on f1 x1, and then using some facts about <.

To prove C3, which has no induction hypothesis, you first use case analysis on is_empty l1, and then use the facts is_empty l1 = true -> l1 = [] and is_empty l1 = false -> l1 = delete_last l1 ++ [get_last l1] (get_last will need a default value).

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.