The Coq mailing list

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

Thanks Cédric, you answered my first question.  

Let me phrase the second question more clearly now.  Consider

Section Relation.
Variable X : Type.
Variable r : X -> X -> Prop.

Inductive star : X -> X -> Prop:=
| starR x : star x x
| starS x x' y : r x x' -> star x' y -> star x y.

Goal forall x y z, star x y -> star y z -> star x z.

Proof. intros x y z A B.
induction A. assumption. eauto using star. Qed.

If you look at the goal after assumption is executed, you see

B : star y z
IHA : star y z -> star x' z

If one looks at star_ind, it is clear why IHA has the unnecessary assumption. 
 There is however a simpler but still fully general induction scheme for star 
avoiding the unnecessary assumption in the inductive hypothesis.

Lemma star_ind' (x y : X) (p : X -> Prop) :
p y ->
( forall x x', r x x' -> star x' y -> p x' -> p x) ->
star x y -> p x.

Proof. intros A B C. induction C ; eauto. Qed.

Goal forall x y z, star x y -> star y z -> star x z.

Proof. intros x y z A B.
induction A using star_ind'. assumption. eauto using star. Qed.

This time, if you look at the goal after assumption is executed, you see

B : star y z
IHA : star x' z

So, my question is, why doesn't Coq generate the simplified induction scheme 
star_ind'?  It seems to me that determining the "real" indices (in this case 
just x) is feasible and having less redundant inductive hypotheses is 
desirable.

Gert