重写 ltac 中的单次出现

Question

如何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.

Answer 1

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

Error: Tactic failure: Setoid library not loaded.

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

Require Import Setoid.

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

Answer 2

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

对重写规则进行更精细控制的另一种可能性是断言所需重写的一般形状（此处将通过 证明theorem1），然后使用新假设执行有针对性的重写。

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

intros a b.
assert (H: f a b + f a b = 4 + f a b) by (rewrite theorem1; reflexivity).
rewrite H.