Skip to Content.
Sympa Menu

coq-club - [Coq-Club] The Proof of palindrome

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] The Proof of palindrome


Chronological Thread 
  • From: "fengsheng" <fsheng1990 AT 163.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] The Proof of palindrome
  • Date: Tue, 23 Jul 2013 08:32:37 +0200 (CEST)

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?



Archive powered by MHonArc 2.6.18.

Top of Page