How to use the rewrite command in coq for inner subexpressions?

Question

I have a lemma telling that addition commutes:

Lemma commute: for all x y, add x y = add y x.

Now in my goal, I am trying to prove that:

add (add x (S y)) z = add x (S (add y z))

I would like to use my lemma to rewrite the inner add on the left

add x (S y) to add (S y) x.

However, the command rewrite commute instead rewrites the outer add:

add (add x (S y)) z to add z (add x (S y)).

Question: how to use commute for rewriting inner subexpressions?

Answer 1

You can precise which arguments you want for your lemma with :

rewrite commute with (x := x)(y :=(S y)).

But it is even more common to apply it like a function with :

rewrite (commute x (S y)).

If one of the specified arguments is obvious, you can avoid mentionning it in the first case, or put an underscore in the second, which would give here :

rewrite commute with (y :=(S y)).

and

rewrite (commute _ (S y)).