Cannot rewrite goal with assertion?

user_5688082 0
Viewed 64

I am not sure I understand why in some cases rewriting H works, and in some it doesnt. Here for example:

Theorem add_assoc2 : forall n m: nat, n + m = m + n.
Proof. intros. rewrite add_comm. reflexivity. Qed.

Theorem plus_4: forall n m p q: nat,
  n + (n * p) + m + (m * p) = n + m + (n * p) + (m * p).
Proof.
  intros.
  assert (H: n * p + m = m + n * p).
  {  rewrite <- add_assoc2. reflexivity. }
  rewrite H.

Gives:

1 goal
n, m, p, q : nat
H : n * p + m = m + n * p
______________________________________(1/1)
n + n * p + m + m * p = n + m + n * p + m * p

But Coq complains: Found no subterm matching "n * p + m" in the current goal. Why?

I clearly see one, on the left side. When using induction, rewriting with IHn doesn't pose any problem, even if there are some other terms in front of rewriteable expression.

coq
1 Answers

You can "see" a subterm n * p + m, but this is misleading: Coq doesn't show you the implicit parentheses around all the + expressions.

Use

Set Printing Parentheses.

to make them visible. Your proof state is really:

  n, m, p, q : nat
  H : ((n * p) + m) = (m + (n * p))
  ============================
  (((n + (n * p)) + m) + (m * p)) = (((n + m) + (n * p)) + (m * p))

Coq was right that there is no subterm that matches H's left hand side expression ((n * p) + m). You need to rewrite using some associativity lemmas to shift the parentheses around.

Also, add_assoc2 is not a good name for a lemma forall n m: nat, n + m = m + n. This is a commutativity property, not associativity.

user_43917430
Related