## Stream: Coq users

### Topic: [beginner] Why doesn't rewrite work here?

#### Julin S (Jun 09 2021 at 05:02):

Hi. I was doing the following

``````Theorem plus3_assoc :
forall (n1 n2 n3: nat),
plus (plus n1 n2) n3 = plus n1 (plus n2 n3).
Proof.
induction n1.
- reflexivity.
- simpl.
rewrite -> IHn1.
(* reflexivity. *)
Qed.
``````

But the `rewrite` usage gives error saying:

"Found no subterm matching "n1 + (?M166 + ?M167)" in the current goal"

IHn1 was:

``````forall n2 n3 : nat, n1 + n2 + n3 = n1 + (n2 + n3)
``````

And Goal was:

``````forall n2 n3 : nat, S (n1 + n2 + n3) = S (n1 + (n2 + n3))
``````

I guess I'm understanding something wrong. Can someone please correct me?

#### Olivier Laurent (Jun 09 2021 at 06:01):

It is probably just because `rewrite` does not work under the binders `forall`. So if you do `intros n2 n3` just before the `rewrite -> IHn1`, it will work as you expect.

#### Olivier Laurent (Jun 09 2021 at 06:03):

An alternative solution is to use `setoid_rewrite` which rewrites under binders:

``````From Coq Require Import Setoid.

Theorem plus3_assoc :
forall (n1 n2 n3: nat),
plus (plus n1 n2) n3 = plus n1 (plus n2 n3).
Proof.
induction n1.
- reflexivity.
- simpl.
setoid_rewrite -> IHn1.
reflexivity.
Qed.
``````

#### Julin S (Jun 09 2021 at 07:18):

Thanks! That made it work. The proof finishes now.

Last updated: Jan 27 2023 at 01:03 UTC