coq - 重写 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.

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

Require Import Setoid.

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