The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

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