The Coq mailing list

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

Dear Jean-Francois, Matthieu and Razvan,

many thanks for the explanations and hints.

First, I see now more clearly that the "fix" tactic plays also the
role of the general induction principle based on the transitive
closure of the direct-subterm relation.

Second, the Equations library looks very interesting and helpful.  I
should have a look at it.

Gyesik



2010/1/28 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
>
>