logic - 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?

标签： logiccoqinduction

Answer 1

您可以使用以下方法精确说明您想要用于引理的参数：

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

但更常见的是像函数一样应用它：

rewrite (commute x (S y)).

如果指定的参数之一很明显，您可以避免在第一种情况下提及它，或者在第二种情况下添加下划线，这将给出：

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

和

rewrite (commute _ (S y)).