Coq equivalent of Lean's `nth_rewrite`

Question

Does Coq have an equivalent of Lean's nth_rewrite? rewrite ... at ... appears to specialize at its first unification site instead of using the argument to choose when to specialize.

---

This is a theorem from the text of Software Foundations Volume 1 (not an exercise, not a solution).

Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  (* We just need to swap (n + m) for (m + n)... seems                                                                                                                                       
     like add_comm should do the trick! *)
  rewrite add_comm.
  (* Doesn't work... Coq rewrites the wrong plus! :-( *)
Abort.

The text then describes proving a lemma and then using it to get Coq to perform the correct rewrite.

However, I know from the some random problems in the natural numbers game that Lean has an nth_rewrite tactic.

This question and its answer suggest a path forward, using rewrite ... at ....

I tried to do that and failed.

So, here's a self-contained proof of the whole thing.

From Coq Require Import Lia.

(* We don't care about this lemma. Prove it uninformatively. *)
Lemma add_comm : forall n m : nat, n + m = m + n.
Proof. lia. Qed.

Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  lia.
Qed.

And here is the exact problem that you get if you try to do it using just rewrite.

Given this:

From Coq Require Import Lia.

Lemma add_comm : forall n m : nat, n + m = m + n. Proof. lia. Qed.

Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  rewrite add_comm.

You get

1 goal (ID 9)
  
  n, m, p, q : nat
  ============================
  p + q + (n + m) = m + n + (p + q)

That is all well and good, let's try it with rewrite add_comm at 1.

Given the input below, the output is exactly the same.

From Coq Require Import Lia.

Lemma add_comm : forall n m : nat, n + m = m + n. Proof. lia. Qed.

Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  rewrite add_comm at 1.

However, rewrite add_com at 2. just fails.

From Coq Require Import Lia.

Lemma add_comm : forall n m : nat, n + m = m + n. Proof. lia. Qed.

Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  rewrite add_comm at 2.

Produces a tactic error:

Error: Invalid occurrence number: 2.

I know that there is more than one possible location that add_comm could apply in my goal.

Bubbler's answer on Stack Overflow says:

rewrite lemma at n instantiates the equality using the first occurrence, and then rewrites its nth occurrence.

This suggests to me that rewrite ... at ... is fundamentally less powerful than nth_rewrite. The "target selection" happens too late in the process and I can't select the nth unification site instead. (It does raise an interesting question, though, of how good of a match something needs to be in Lean land to be a potential rewrite site.)

Is there a Coq tactic, built in or custom, that can target the nth unification site for a rewrite in the way that Lean's nth_rewrite does?

Answer 1

(This answer is based on a comment by Pierre Courtieu to try setoid_rewrite)

The equivalent of nth_rewrite in Lean is indeed setoid_rewrite ... at ... in Coq, which is actually mentioned in Bubbler's answer from Stack Overflow.

I guess for some reason I thought that tactic was setoid-specific (with a setoid being a type equipped with an equivalence relation). But upon further reflection I guess a type like nat is indeed a trivial setoid.

From Coq Require Import Lia.

Lemma add_comm : forall n m : nat, n + m = m + n. Proof. lia. Qed.

Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  setoid_rewrite add_comm at 2.
  reflexivity.
Qed.

This proof goes through without issues.