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: Oct 04 2023 at 23:01 UTC