The Coq mailing list

[Gregory Malecha <gregory AT bedrocksystems.com>]

Hello --

My intuition, which may be incorrect, about rewrite at is that it performs unification to find possible rewrites and replaces them. If you don't have an "at", then it rewrites all occurences of the *first* match. If you say, "at" then it will only rewrite one occurence and it will pick the occurance by skipping the first n-1 matches (though the numbers can seem quite arbitrary).

While I haven't used it, I believe that ssreflect has a much nicer mechanism for picking particular instantiations based on what is matched rather than by position number, and I believe that this matches has been integrated into Coq-proper at this point, so I would suggest using it.

On Thu, Aug 15, 2019 at 1:26 PM David Holland <dholland-coq AT netbsd.org> wrote:

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

--

gregory malecha

gregory AT bedrocksystems.com

director of formal methods