Why is following Coq rewrite not applying on right hand side of assumption?

Link:: https://stackoverflow.com/q/46016461

Display all goals and responses

Question

I have following Coq env.

n, m: nat
IHm: forall n : nat, n + n = m + m -> n = m
H: S (n + S n) = S (m + S m)
ll: forall k : nat, k + S k = S k + k

Doing rewrite ll in H, only changes the LHS S (n + S n) to S (S n + n) but not the RHS S (m + S m):

n, m: nat
IHm: forall n : nat, n + n = m + m -> n = m
H: S (S n + n) = S (m + S m)
ll: forall k : nat, k + S k = S k + k

ll should be applicable on all variables of type nat. What is wrong here?

A (ejgallego): rewrite H will only use one instantiation of H, you need to use the ! quantifier to force more rewrites to happen. Example:

Lemma ex n m : n = m -> n + 0 = m + 0.n, m: nat
n = m -> n + 0 = m + 0
Proof.n, m: nat
n = m -> n + 0 = m + 0 now rewrite <- !plus_n_O. Qed.

Answer

Expanding on Emilio's comment, rewrite H and rewrite H in H' will first find an instantiation for all (dependently) quantified variables of H, and then replace all occurrences [1] of that instantiated LHS with the RHS. I believe it finds the topmost/leftmost instantiation in the syntax tree. So, for example, if you do this:

Goal forall a b,
    (forall x, x + 0 = x) -> (a + 0) * (a + 0) * (b + 0) = a * a * b.forall a b : nat,
(forall x : nat, x + 0 = x) ->
(a + 0) * (a + 0) * (b + 0) = a * a * b
  intros a b H.a, b: nat
H: forall x : nat, x + 0 = x
(a + 0) * (a + 0) * (b + 0) = a * a * b
  rewrite H.a, b: nat
H: forall x : nat, x + 0 = x
a * a * (b + 0) = a * a * b

the rewrite H will choose to instantiate x with a, and the resulting goal will be a * a * (b + 0) = a * a * b. You can prefix the lemma with ! (as in rewrite !H) to mean "rewrite everywhere, picking as many instantiations as you can", or with ? (as in rewrite ?H) to mean try rewrite !H, i.e., you can pick multiple instantiations, and also don't fail if you can't find any.