The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Hi
>   (* The following does not work. Error: Tactic failure: Nothing to
> rewrite. *)
>   try rewrite <- compose_assoc at 2.

Unfortunately the rewrite _ at n, rewrite the nth occurrence of the 
first pattern that is found

Here is an example:

Goal forall (x y : nat), (x + 0) + (y + 0) + (x + 0) = 0.
intros.
rewrite <- plus_n_O at 2.

If you want to select a particular occurrence, one way is to instantiate 
the theorem enough to make it applicable only where you want.

In your example

Lemma Foo
      {A:Type}
      (f0 f1 f2 f3 f4: A->A)
  :
    compose f1 (compose f2 (compose f3 f4))  =
    compose f1 (compose (compose f2 f3) f4).
Proof.
  intros.
rewrite <- (compose_assoc _ _ _ _  _ _ f2).

or

Lemma Foo
      {A:Type}
      (f0 f1 f2 f3 f4: A->A)
  :
    compose f1 (compose f2 (compose f3 f4))  =
    compose f1 (compose (compose f2 f3) f4).
Proof.
  intros.
   rewrite <- compose_assoc with (h := f2).