coq - 将重写策略应用于子表达式

Question

如何应用仅针对子表达式的rewrite ->？例如，考虑这个定理:

Parameter add : nat -> nat -> nat.
Axiom comm : forall a b, add a b = add b a.

Theorem t1 : forall a b : nat,
(add (add a b) (add a (add a b))) =
(add (add a b) (add a (add b a))).

直观上，它只需要交换一个 (add a b) 子表达式，但如果我执行 rewrite -> (comm a b)，它会重写所有出现的情况。如何定位特定的子表达式？

Answer 1

在这种情况下，ssreflect 匹配工具通常比“at”更方便[我敢说子术语重写通常是人们转向 ssreflect 重写的原因] 。特别是:

• rewrite {pos}[pat]lemma 将选择模式 pat 的出现 pos 进行重写，
• pat 可以是 contextual pattern这可以让您提高脚本的稳健性。