The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

  indeed the semantics of [rewrite l at n] is to first
find a complete match [l'] of [l] and rewrite the [n]th instance
of [l'] in the goal whereas [setoid_rewrite l at n] will
rewrite the [n]th instance of [l], even allowing multiple rewrites
at once:

Lemma foo (A: Type) (P: list A -> list A -> Prop) (x1 x2: A):
P (x1 :: nil) (x2 :: nil).
Proof. intros. setoid_rewrite <- List.app_nil_l at 1 2.

Goal is : P (nil ++ x1 :: nil) (nil ++ x2 :: nil)

The fact that [rewrite l] first finds a single instance is for
backward compatibility reasons. The semantics of the positions
is clear though, there are 4 subterms of type [list A] here, 
and they are found in left-to-right, top-down order. The only 
tricky point here is that occurrences of an instance which are inside
a strict subterm of a rewritten occurrence are not taken into account,
hence the [2] in the above invocation applies to the [x2 :: nil] subterm
and not to the [nil] inside [x1 :: nil] because [x1 :: nil] itself
was rewritten.

Hope this helps,
-- Matthieu

Le 9 févr. 2011 à 09:10, Damien Pous a écrit :

> I recently filed a bug report about a similar behaviour with setoid 
> relations:
> http://coq.inria.fr/bugs/show_bug.cgi?id=2474
> I didn't notice it was also problematic with plain Leibniz equality...
> 
> Another option here is to use "setoid_rewrite at" rather than "rewrite
> at" (although "rewrite at" seems to be already implemented with
> setoids!):
> 
> Require Import List.
> 
> Lemma foo (A: Type) (P: list A -> list A -> Prop) (x1 x2: A):
> P (x1 :: nil) (x2 :: nil).
> Proof.
> rewrite <- List.app_nil_l.
> Show Proof.                    (* eq_ind *)
> Restart.
> rewrite <- List.app_nil_l at 1.
> Show Proof.                    (* setoid things *)
> Restart.
> Fail rewrite <- List.app_nil_l at 2.
> setoid_rewrite <- List.app_nil_l at 2.
> Show Proof.                    (* setoid things *)
> Abort.
> 
> 
> 
> Damien