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?

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.

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.
```

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

Last updated: Oct 04 2023 at 23:01 UTC