The Coq mailing list

[Razvan Voicu <razvan AT comp.nus.edu.sg>]

Hi Gyesik and Matthieu,

Consider the following proof for your goal:

Theorem le_Pfact: forall x:nat, exists y, Pfact x y.
Proof.
fix circ 1.
intro.
destruct x.
exists 1.
constructor.
destruct x.
 exists 1.
 constructor.
 pose proof (circ x) as H.
 destruct H. (* existential var becomes x0 *)
 exists (x * x0).
 constructor.
 assumption.
Save.

I find the above style of inductive proof much easier. Of course, the 
hypothesis "circ" must be applied in a well-founded way. However, 
there's no need to have an adequate induction principle readily 
available (or even bother to know what that induction principle should be).

Hope this helps,

Razvan

Matthieu Sozeau wrote:
> Le 27 janv. 10 à 10:57, Gyesik Lee a écrit :
>
> > Hi,
>
> Hi Gyesik,
>
> > 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.
>
> My soon-to-be-released Equations [1] plugin has ML code to generate this
> order on any non-impredicative, computational inductive family (ie. most
> datatypes). You can derive both the subterm relation (actually the
> transitive closure of the direct subterm relation) and its 
> wellfoundedness
> proof and a [Below] predicate that can be used to recurse and get a tuple
> of all the possible recursive calls in the context. You don't need to 
> worry
> about guardness checks anymore if you use any of these, but you have to
> provide proofs that recursive arguments decrease in the first case or
> find your way in a tuple in the second case. This is partially 
> automatable
> though.
>
> <<
>
> Require Import Equations.
>
> 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).
>
> Derive Subterm for nat.
>
> Theorem le_Pfact : forall x : nat, exists y, Pfact x y.
> apply FixWf; intros.
> destruct x. econstructor; constructor.
> destruct x. econstructor. constructor.
>   destruct (H x). solve_rec.
>   exists (x * x0). constructor; auto.
> Qed.
>
> Derive Below for nat.
>
> Definition rec_nat (P : nat -> Type) (step : Π n, Below_nat P n -> P 
> n) n : P n :=
>   step n (below_nat P step n).
>
> Theorem le_Pfact' : forall x : nat, exists y, Pfact x y.
> induction x using rec_nat.
> destruct x. econstructor; constructor.
> destruct x. econstructor. constructor.
>   simpl in X. destruct_conjs.
>   exists (x * e0). constructor; auto.
> Qed.
>
> >>
>
> [1] http://mattam.org/research/coq/equations.en.html
>
> -- Matthieu