The Coq mailing list

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

Certainly star_ind and star_ind' have the same proof power.  But since 
star_ind has the dependency on y, it will give you unnecessarily complex 
inductive hypotheses (since the assumptions depending on y will be included). 
 Gert

Am 06.12.2011 um 10:53 schrieb Alexandre Pilkiewicz:

> 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