coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jean-Francois Monin <jean-francois.monin AT imag.fr>
- To: Gyesik Lee <gslee AT ropas.snu.ac.kr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] inductive types and well-foundness of the structural orderings
- Date: Thu, 28 Jan 2010 00:28:01 +0800
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:in-reply-to:user-agent; b=ti2jJp3vSjH/J5dhoK4pVb6v3PV86Mqy9SRyTkdBvvZpC3Z+jzNKstWcF0a21mwQzW TPwlf5w9d71m7REM/6aamTkKOwSrHAW1vqP0/vFSARgQzhs5Ku+ASUsw27JWLSacRtrw ZaW2q/KhRId35wh9sgG+ykVphXFwZT7GlSHnw=
Hi,
You don't need lt.
Theorem le_Pfact : forall x : nat, exists y, Pfact x y.
refine
(fix le_Pfact (x : nat) : exists y : _, Pfact x y :=
match x with
| 0 => _
| 1 => _
| S (S n) => _
end).
exists 1; constructor 1.
exists 1; constructor 2.
destruct (le_Pfact n) as (v, Hnv). exists (n * v); constructor 3.
assumption.
Qed.
Here is another solution using the undocumented "fix".
Theorem le_Pfact : forall x : nat, exists y, Pfact x y.
fix 1.
destruct x as [| x].
exists 1; constructor 1.
destruct x as [| n].
exists 1; constructor 2.
destruct (le_Pfact n) as (v, Hnv). exists (n * v); constructor 3.
assumption.
Qed.
Hope this helps,
JF
On Thu, Jan 28, 2010 at 12:57:28AM +0900, Gyesik Lee wrote:
> Hi,
>
> as in the following case, an induction principle provided by Coq is
> sometimes not strong enough:
>
> (A modified version of the example in Section 8.4.1.1 of CoqArt book.)
> ===================
> Open Scope nat_scope.
>
> Inductive Pfact : nat -> nat -> Prop :=
> | Pfact0 : Pfact 0 1
> | Pfact1 : Pfact 1 1
> | Pfact2 : forall n v : nat, Pfact n v -> Pfact (S (S n)) (n * v).
>
> Axiom lt_wf : well_founded lt.
>
> Theorem le_Pfact : forall x : nat, exists y, Pfact x y.
> induction x.
> (* then the induction hypothesis is not strong enough*)
> Abort.
>
> induction x using lt_wf.
> (* then the claim can be easily proved. *)
>
> ===================
>
> I am wondering if Coq provides a kind of mechanism producing the
> induction principle reflecting the well-foundedness of the canonically
> definable structural orderings on inductive types.
>
> Or is there a way to prove le_Pfact without using the well-foundedness
> of lt relation? I mean a "general" way, not specialized to this
> problem.
>
> Gyesik
>
>
--
Jean-Francois Monin
CNRS-LIAMA, Project FORMES & Universite de Grenoble 1
Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: +86 10 62 79 69 79 ext 605
Fax@LIAMA:
+86 10 6264 7458
- [Coq-Club] inductive types and well-foundness of the structural orderings, Gyesik Lee
- Re: [Coq-Club] inductive types and well-foundness of the structural orderings, Jean-Francois Monin
- Re: [Coq-Club] inductive types and well-foundness of the structural orderings, Matthieu Sozeau
Archive powered by MhonArc 2.6.16.