The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

[setoid_rewrite <-compose_assoc at 2] works in Vadim's example.  The way 
that setoid_rewrite matches patterns is different from the way that 
rewrite matches patterns.  I think that setoid_rewrite's method is more 
intuitive.

-- Jonathan


On 08/16/2016 05:53 PM, Laurent Thery wrote:
> 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).