The Coq mailing list

[<michael.soegtrop AT intel.com>]

Dear Coq users,

can someone explain to me how "rewrite at" works? Please have a look at this
simple example:

Require Import NPeano.

Theorem Test1 : forall a b c d:nat, a+b = c+d -> b+a = d+c.
Proof.
  intros.
  rewrite Plus.plus_comm at 2.                     Doesn't work
  rewrite Plus.plus_comm with (m:=c).         Does work

I was expecting that rewrite at 2 swaps d+c, but I get an error. rewrite at 1
works as expected. Also "rewrite with" works for the second term.

From the description in the reference manual I was assuming that rewrite at 2
should swap d+c in the above term. I also tried larger numbers (not knowing
how terms are counted), but everything I tried except for 1 doesn't work with
rewrite at.

Best regards,

Michael