在 ltac 中重写单次出现

Question

如何在 ltac 中调用 rewrite 以仅重写一次？我认为 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_tactic121）。

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

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

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

Answer 3

有几种选择，@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）下重写，因为如果这样做了，你就可以从 fun x => x + 0 到 fun x => x，这是不相等的香草辅酶

然后 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.

在 ltac 中重写单次出现

rewrite single occurence in ltac

coq

coq-tactic

ltac