5

如何rewrite在 ltac 中调用以仅重写一次出现？我认为 coq 的文档中提到了一些内容，rewrite at但我无法在实践中实际使用它，也没有示例。

这是我正在尝试做的一个例子：

Definition f (a b: nat): nat.
Admitted.

Theorem theorem1: forall a b: nat, f a b = 4.
Admitted.

Theorem theorem2: forall (a b: nat), (f a b) + (f a b) = 8.
Proof.
intros a b.
(*
my goal here is f a b + f a b = 8
I want to only rewrite the first f a b
The following tactic call doesn't work
*)
rewrite -> theorem1 at 1.
4

3 回答 3

6

当我按照您的建议尝试时rewrite -> theorem1 at 1.，我收到以下错误消息：

Error: Tactic failure: Setoid library not loaded.

因此，作为一种反应，我重新启动了您的脚本，包括一开始的以下命令。

Require Import Setoid.

现在，它可以工作了（我正在使用 coq 8.6 进行测试）。

于 2017-08-01T06:22:54.323 回答
4

您正在使用该rewrite at策略的变体，正如手册所指定的，它始终通过 setoid 重写来执行（请参阅https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic121）。

更好地控制重写规则的另一种可能性是断言所需重写的一般形式（这里可以通过 证明theorem1），然后使用新假设执行集中重写。

这无需借助任何库即可工作：

intros a b.
assert (H: f a b + f a b = 4 + f a b) by (rewrite theorem1; reflexivity).
rewrite H.
于 2017-08-01T17:55:21.147 回答
2

有几种选择，@Yves 指出了其中一种。

另一种选择是使用pattern策略：

pattern (f a b) at 1.
rewrite theorem1.

这里的诀窍实际上是pattern (f a b) at 1.转动目标

f a b + f a b = 8

进入

(fun n : nat => n + f a b = 8) (f a b)

基本上，它扩展了你的目标，在f a b. 此外，通常rewrite不会在活页夹（例如 lambdas）下重写，因为如果这样做了，你就可以从 let's say fun x => x + 0to 去fun x => x，这在 vanilla Coq 中是不相等的。

然后rewrite theorem1.将参数重写(f a b)为4并简化一点（它会减少 beta），因此您获得4 + f a b = 8.

旁注：您也可以replace像这样使用策略：

replace (f a b + f a b) with (4 + f a b) by now rewrite theorem1.
于 2017-08-02T12:41:37.660 回答