Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] The Proof of palindrome


Chronological Thread 
  • From: Daniel Schepler <dschepler AT gmail.com>
  • To: fengsheng <fsheng1990 AT 163.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] The Proof of palindrome
  • Date: Tue, 23 Jul 2013 11:31:02 -0700

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



Archive powered by MHonArc 2.6.18.

Top of Page