The Coq mailing list

[Cédric AUGER <Cedric.Auger AT lri.fr>]

Le Tue, 6 Dec 2011 10:35:35 +0100,
Gert Smolka 
<smolka AT ps.uni-saarland.de>
 a écrit :

> Consider the following definition of reflexive transitive closure:
> 
> Section Relation.
> Variable X : Type.
> Variable r : X -> X -> Prop.
> 
> Inductive star (x : X ) : X -> Prop:=
> | starR : star x x
> | starS x' y : r x x' -> star x' y -> star x y.

Just a hint, try not to mess with indices and parameters.

Here, you put 'x' as a parameter, whereas you use it as an index (see
the call "star x' y"), while you use y as an index where you could use
it as a parameter (all the calls are done with the same 'y' argument);
so that you could have put it a parameter by reversing the order of the
arguments.
-----------8<------------------------
Parameter X : Type.
Parameter r : X -> X -> Prop.
Inductive star (x : X ) : X -> Prop:=
 | starR : star x x
 | starS x' y : r x x' -> star x' y -> star x y.

Inductive star2 : X -> X -> Prop:=
 | starR2 x : star2 x x
 | starS2 x x' y : r x x' -> star2 x' y -> star2 x y.

Inductive star3 (y : X ) : X -> Prop:=
 | starR3 : star3 y y
 | starS3 x x' : r x x' -> star3 y x' -> star3 y x.

Notation "x '-*->' y" := (star3 y x) (at level 100).

Check star_ind.
(*
star_ind
     : forall P : X -> X -> Prop,
       (forall x : X, P x x) ->
       (forall x x' y : X, r x x' -> star x' y -> P x' y -> P x y) ->
       forall x x0 : X, star x x0 -> P x x0
*)
Check star2_ind.
(*
star2_ind
     : forall P : X -> X -> Prop,
       (forall x : X, P x x) ->
       (forall x x' y : X, r x x' -> star2 x' y -> P x' y -> P x y) ->
       forall x x0 : X, star2 x x0 -> P x x0
*)
Check star3_ind.
(*
star3_ind
     : forall (y : X) (P : X -> Prop),
       P y ->
       (forall x x' : X, r x x' -> (x' -*-> y) -> P x' -> P x) ->
       forall x : X, (x -*-> y) -> P x
*)
--------------------8<-------------------------------

> The induction scheme star_ind generated by Coq is suboptimal since it
> quantifies over both arguments x and y of star.  It is easy to prove
> an induction scheme quantifying only over x.
> 
> Lemma star_ind' (y : X) (p : X -> Prop) :
> p y ->
> ( forall x x', r x x' -> star x' y -> p x' -> p x) ->
> forall x, star x y -> p x.

I guess your "star_ind'" reminds you of my "star3_ind" ^^

> 
> Proof. intros A B x C. induction C ; eauto. Qed.
> 
> Unfortunately, I cannot use star_ind' with the induction tactic:
> 
> Goal forall x y z, star x y -> star y z -> star x z.
> 
> Proof. intros x y z A. revert z.
> induction A using star_ind'.
> 
> Error: Cannot recognize the conclusion of an induction scheme.
> 
> I have 2 questions:
> 
> 1) Why does the induction tactic reject star_ind'?

I din't know what is an induction scheme in Coq understandings,
but proving:
forall x y P, P y -> (forall x x', r x x' -> star x' y -> p x' -> p x)
-> star x y -> p x

instead of

forall y P, P y -> (forall x x', r x x' -> star x' y -> p x' -> p x) ->
forall x, star x y -> p x

works (the place of 'x' seems to be relvant)

> 2) Is there a good reason that Coq generates star_ind rather than
> star_ind'?

That is that if a parameter should be an index, it is turned into an
index (and I guess that all "rightfull" parameters following that
index are turned into indice as well, although I didn't check it), but
an index that could be a parameter is never turned into a parameter, to
fit the user specification.

Putting your argument 'y' implies swapping it with 'x' as parameters
MUST precede indice (it is reasonnable, since parameters cannot depend
on indice obviously).

My question would rather be: "Why is your definition of star accepted,
while you declared an index as a parameter?"

But I guess that the answer is that people don't want to understand and
explicitly give their parameters and indice; maybe that putting a
warning should be a good thing.

> 
> Thanks, Gert