Cannot rewrite goal with assertion?

Question

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

Require Import PeanoNat.

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

Theorem plus_4 : forall n m p q : nat,
    n + (n * p) + m + (m * p) = n + m + (n * p) + (m * p).
forall n m p : nat,
nat -> n + n * p + m + m * p = n + m + n * p + m * p
Proof.
forall n m p : nat,
nat -> n + n * p + m + m * p = n + m + n * p + m * p
  intros.
n, m, p, q: nat
n + n * p + m + m * p = n + m + n * p + m * p
  assert (H : n * p + m = m + n * p).
n, m, p, q: nat
n * p + m = m + n * p
n, m, p, q: nat
H: n * p + m = m + n * p
n + n * p + m + m * p = n + m + n * p + m * p
  {
n, m, p, q: nat
n * p + m = m + n * p rewrite <- add_assoc2.
n, m, p, q: nat
m + n * p = m + n * p reflexivity. }
n, m, p, q: nat
H: n * p + m = m + n * p
n + n * p + m + m * p = n + m + n * p + m * p
  rewrite H.
Found no subterm matching "n * p + m" in the current goal.
n, m, p, q: nat
H: n * p + m = m + n * p
n + n * p + m + m * p = n + m + n * p + m * p

Gives:

1 subgoal

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

But Coq complains:

The command has indeed failed with message:
Found no subterm matching "n * p + m" in the current goal.

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.

Answer

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:

1 subgoal

  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.