2

如何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)，它会重写所有出现的情况。如何定位特定的子表达式？

4

2 回答 2

3

在这种情况下，ssreflect 匹配工具通常比“ at”更方便[我敢说子项重写通常是人们切换到 ssreflect 重写的原因]。尤其是：

  • rewrite {pos}[pat]lemma将选择要重写pos的模式的出现，pat
  • pat可以是一种上下文模式，可以让您提高脚本的健壮性。
于 2019-04-22T11:36:23.447 回答
2

您可以rewrite使用后缀. 出现次数从 1 开始按从左到右的顺序编号。您可以通过用空格分隔它们的索引来重写多次出现。你需要. 后缀也可用于其他一些针对术语出现的策略，包括许多执行转换的策略（、、等）、、等。at NRequire Import Setoidatchangeunfoldfoldsetdestruct

intros.
rewrite -> (comm a b) at 2.
rewrite -> (comm _ _).
reflexivity.

还有其他可能的方法，特别是如果您只需要应用等式。该congruence策略可以自己找到要重写的内容并应用对称性和传递性，但是您需要通过将所有等价添加到上下文（以普遍量化的等价形式）来启动它，它不会查询提示数据库。

assert (Comm := comm).
congruence.

为了获得更多的自动化，Hint Rewrite创建一个该策略autorewrite将尝试应用的定理数据库。对于更高级的自动化，请查看使用 setoids进行的广义重写，我对此不太熟悉，无法详细说明。

于 2019-04-21T21:55:49.233 回答