The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Gert Smolka wrote:
> 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 will give yet another response that doesn't directly answer your 
questions. :)

I agree that this induction principle is more convenient than the 
automatically generated one.  I don't know why [induction] doesn't like 
your principle, but it is easy to implement a tactic that is just about 
as convenient as [induction]:

  Ltac star_ind H :=
    match type of H with
      | star ?x _ => pattern x; eapply star_ind'; try eexact H
    end.

Then your theorem follows directly:

  Hint Constructors star.

  Goal forall x y z, star x y -> star y z -> star x z.
    intros x y z A; revert z; star_ind A; eauto.
  Qed.