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.
rewrite usage gives error saying:
"Found no subterm matching "n1 + (?M166 + ?M167)" in the current goal"
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: Jan 27 2023 at 01:03 UTC