The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Jul 22, 2013 at 11:32 PM, fengsheng 
<fsheng1990 AT 163.com>
 wrote:
> Hello everyone:
>   I met a question of palindrome,the following is my definition of 
> palindrome:
>   Inductive pal {X : Type} : (list X) -> Prop :=
>   | pal_empty :  pal []
>   | pal_single : forall (x : X), pal [x]
>   | pal_app: forall (x : X) (l: list X), pal l -> pal (x::(snoc l x)).
>
>   Now, I want to prove:
>   THeorem forall l, l = rev l -> pal l.
>   But I counld not work it out.
>   Counld you give me a proof of the theorem?

Here's my first cut at such a proof.  Probably not as efficient as it
could be, but it should give the basic idea.

Require Import List.

Inductive palindrome {A:Type} : list A -> Prop :=
| palindrome_empty : palindrome nil
| palindrome_single (x:A) : palindrome (x :: nil)
| palindrome_extend : forall (x:A) (l:list A),
  palindrome l -> palindrome (x :: l ++ x :: nil).

Lemma palindrome_rev_eq : forall (A:Type) (l:list A),
  palindrome l -> rev l = l.
Proof.
induction 1; try reflexivity.
repeat (progress simpl || rewrite rev_app_distr).
f_equal.
f_equal.
trivial.
Qed.

Lemma app_end_eq : forall (A:Type) (l1 l2:list A) (x y:A),
  x :: l1 = l2 ++ y :: nil ->
  (x = y /\ l1 = nil /\ l2 = nil) \/
  (exists l':list A, l1 = l' ++ y :: nil /\ l2 = x :: l').
Proof.
induction l1; intros.
+ left.
  destruct l2; simpl in H.
  - injection H; repeat split; trivial.
  - injection H; intros.
    destruct l2; discriminate H0.

+ right.
  destruct l2; simpl in H.
  - discriminate H; intros.
  - injection H; intros; subst a0.
    clear H.
    destruct (IHl1 _ _ _ H0) as [ [? [? ?]] | [l' [? ?]] ]; subst.
    * exists nil; split; trivial.
    * exists (a :: l'); split; trivial.
Qed.

Require Import Arith.

Lemma rev_eq_palindrome : forall (A:Type) (l:list A),
  rev l = l -> palindrome l.
Proof.
intros.
(* Proceed by "strong induction" on length l. *)
remember (length l) as n.
revert l H Heqn; induction (lt_wf n).

destruct l; try constructor.
simpl; intros.
destruct (app_end_eq _ _ _ _ _ (eq_sym H1)) as
  [ [? [? ?]] | [l' [? ?]] ].
+ subst l; constructor.
+ subst l; constructor.
  apply H0 with (y := length l'); trivial.
  - rewrite app_length in Heqn; simpl in Heqn.
    rewrite plus_comm in Heqn; simpl in Heqn.
    subst x; auto with arith.
  - rewrite rev_unit in H3.
    injection H3; trivial.
Qed.
-- 
Daniel Schepler