The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 07/23/2013 02:31 PM, Daniel Schepler wrote:
> 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 another proof that is mostly automated.  More or less all you 
need is a lemma about decomposing a list into its last element and the rest.

Require Import List Omega.

Set Implicit Arguments.

Hint Extern 1 (_ <=_ ) => omega.

Inductive pal {X : Type} : list X -> Prop :=
   | pal_empty : pal nil
   | pal_single : forall (x : X), pal (x :: nil)
   | pal_app: forall (x : X) (l: list X), pal l -> pal (x :: l ++ x :: 
nil).

Hint Constructors pal.

Ltac t := simpl; repeat (autorewrite with list in *; simpl in *;
  repeat match goal with
           | [ H : ex _ |- _ ] => destruct H
           | [ H : _ :: _ = _ :: _ |- _ ] => injection H; clear H; 
intros; subst
         end;
  intuition (try congruence; try omega; eauto; try subst)).

Lemma app_nil : forall A (ls : list A),
  ls = nil ++ ls.
  t.
Qed.

Lemma app_cons : forall A (a : A) ls a',
  a :: ls ++ a' :: nil = (a :: ls) ++ a' :: nil.
  t.
Qed.

Hint Immediate app_nil app_cons.

Lemma has_last : forall A (ls : list A),
  ls = nil \/ exists ls' a, ls = ls' ++ a :: nil.
  induction ls; t.
Qed.

Lemma deapp : forall A (a : A) ls1 ls2,
  ls1 ++ a :: nil = ls2 ++ a :: nil
  -> ls1 = ls2.
  intros; do 2 (apply (f_equal (@rev _)) in H; t).
Qed.

Hint Immediate deapp.

Lemma pal_complete' : forall A n (l : list A), length l <= n
  -> l = rev l -> pal l.
  induction n; destruct l; t;
    specialize (has_last l); t.
Qed.

Theorem pal_complete : forall A (l : list A), l = rev l -> pal l.
  eauto using pal_complete'.
Qed.