Proof 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 unofficial outline of evidence is as follows:

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

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

(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 be fulfilled ...

A recursive case analysis will end for any finite list l0 , because the length of the analyzed list is reduced by 2 after each iteration. If it ends for any list ln , all its external lists up to l0 are also palindromes, since a list constructed by adding two identical elements at both ends of the palindrome is also a palindrome.

I think the reasoning sounds, but I'm not sure how to formalize it. Can this be turned into evidence in Coq? Some explanations of how tactics were used were especially helpful.

Answer 1

This is a good example where “direct” induction does not work at all, because you are not making a direct recursive call on the tail, but on part of the tail. In such cases, I usually advise you to indicate your lemma with the length of the list, not the list itself. Then you can specialize in this. It will 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: in order to help you, I needed the following lemmas; to make this proof, you may need them too.

 Lemma tool : forall (X:Type) (l l': list X) (ab: 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) (ab: X), l1 ++ a :: nil = l2 ++ b :: nil -> a = b /\ l1 = l2. 

Answer 2

You can also get your principle of induction from a valid induction form.

 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 the hypothesis 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 does not have an induction hypothesis, 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).