Why can't I perform rewrite tactic here?

I have already a theorem

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.

and I want to prove its "reverse form". So I have

Theorem plus_n_n_injective : forall n m,
     n + n = m + m ->
     n = m.
Proof.
  intros n. induction n as [| n' IHn'].
  - intros [] eq. reflexivity. discriminate.
  - intros m eq.

And then the goal is

1 goal
n' : nat
IHn' : forall m : nat, n' + n' = m + m -> n' = m
m : nat
eq : S n' + S n' = m + m
______________________________________(1/1)
S n' = m

So IMO, I want to rewrite the goal to S n' + S n' = m + m by plus_id_example. However, it fails with

rewrite <- plus_id_example

I don't know why.

Maybe it is because we can only rewrite like a = b. However, replacing it to apply plus_id_example does not work. And I don't know how to apply ... with ... with multiple replacement to take.

The only way is like

    pose proof plus_id_example as pp.
    specialize pp with (n := S n').
    specialize pp with (m := m).

My question is is there any way to do this with apply with or rewrite?

Meanwhile, I want to rewrite the goal to match eq, is there a way to do so?

Solution

When you send the command

rewrite <- plus_id_example.

The system analyzes the statements of plus_id_example and detects whether its conclusion is an equality (it is), and then it computes the pattern in the right hand side of this equality, here this pattern is:

(x + x)

where x can be replaced by any value (because the m in plus_id_example is universally quantified.

Then it looks in the conclusion of the goal for an instance of this pattern.

Here the conclusion of the goal is

S n' = m

So, there is no place where this rewrite can be applied, and the command fails. This is the reason why you can't perform this precise rewrite command.

Anyway, the theorem plus_id_example is in fact not useful to prove the theorem plus_n_n_injective, you should think of another proof plan.