# Coq equivalent of Lean's nth_rewrite

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! *)
(* 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.

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.


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.


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.


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?

• Unchecked answer: try setoid_rewrite. Commented Jun 14 at 5:57

(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.
reflexivity.
Qed.


This proof goes through without issues.