The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

I'm sorry, I won't reply to the main question of the email, but I'm
still going to ask another one:

On Tue, Dec 6, 2011 at 10:35 AM, Gert Smolka 
<smolka AT ps.uni-saarland.de>
 wrote:
> 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.

How is it "sub-optimal", since you are able to prove your own
"induction scheme" with it. It seems to me that since star_ind implies
your star_ind', it is more optimal than star_ind'!

Do you have an example of lemma that you think you'll be able to prove
with star_ind' and not with star_ind?

Goal forall x y z, star x y -> star y z -> star x z.
Proof.
  intros * H *.
  induction H; eauto using starS.
Qed.


Cheers,
Alexandre

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