The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

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