coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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?
- [Coq-Club] The Proof of palindrome, fengsheng, 07/23/2013
- Re: [Coq-Club] The Proof of palindrome, Vincent Siles, 07/23/2013
- Re: [Coq-Club] The Proof of palindrome, Daniel Schepler, 07/23/2013
- Re: [Coq-Club] The Proof of palindrome, Adam Chlipala, 07/24/2013
Archive powered by MHonArc 2.6.18.