Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] inductive types and well-foundness of the structural orderings

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] inductive types and well-foundness of the structural orderings


chronological Thread 
  • 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



Archive powered by MhonArc 2.6.16.

Top of Page