The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Hi,
you can have a look at Pierre's webpage on this subject:

http://www.labri.fr/perso/casteran/CoqArt/inductive-prop-chap/palindrome.html

Best,
V.

2013/7/23 fengsheng 
<fsheng1990 AT 163.com>:
> 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?