The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

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.

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.

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'?

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

Thanks, Gert