The Coq mailing list

[David Holland <dholland-coq AT netbsd.org>]

On Sun, Aug 11, 2019 at 11:38:35AM +0800, Cao Qinxiang wrote:
 > Dear Coq clubbers,
 > 
 > I find that the behavior of "rewrite ... at ..." is quite strange. I am
 > wondering whether it is actually a feature or a bug. Here is a tiny 
 > example.
 >
 > [...]

I don't know officially, but, as strange as that behavior seems, I
think it's at least mostly what's intended. The understanding I have,
which may be incomplete, is that the idea of "at N" is to pick which
of several matches in the target term you want to operate on...
*after* the matches have been found by instantiating binders and so
on. So you can't use "at N" to tell it whether to operate on x or y or
z.

In your setting, one gets

Goal forall x y, foo x y y.
   intros.

   rewrite <- app_nil_l with (l := y).      (* foo x (nil ++ y) (nil ++ y) *)
   rewrite <- app_nil_l with (l := y) at 1. (* foo x (nil ++ y) y *)
   rewrite <- app_nil_l with (l := y) at 2. (* foo x y (nil ++ y) *)

and my understanding is that this is the control that "at N" is
supposed to give.

However, I apparently don't have the full picture because one also gets

   rewrite <- (@app_nil_l (list _)) at 1.   (* foo x (nil ++ y) y *)
   rewrite <- (@app_nil_l (list _)) at 2.   (* foo x y (nil ++ y) *)
   rewrite <- (@app_nil_l (list _)).        (* foo x y (nil ++ y) *)

I guess this matching works differently? Maybe someone else can shed
further light.

-- 
David A. Holland
dholland AT netbsd.org