The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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