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

Question

I have following Coq env.

    1 subgoals
m : nat
IHm : forall n : nat, n + n = m + m -> n = m
n : nat
H : S (n + S n) = S (m + S m)
ll := 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). ll should be applicable on all variables of type nat. What is wrong here?

Answer 1

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* 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.
  intros a b H.
  rewrite H.

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.

*There's actually a bit more nuance, which is that the replacement is done in a single pass with rewrite H and in multiple passes with rewrite ?H and rewrite !H. This only shows up when the first replacement(s) expose other replacement locations that weren't previously available. This shows up, for example, if you rewrite with a + 0 = a in the goal (a + 0) + 0 = a; rewrite H leaves the goal a + 0 = 0.