The Coq mailing list

[Gyesik Lee <leegys AT gmail.com>]

I don't try to answer your question, but want to ask back why Coq should choose your simplified version of induction.

I am saying without having done any deep consideration, but probably there are cases where the simplified version is not comfortable to be used.

The question is now about the mechanism of producing induction principles.

Gyesik

2011/12/6 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