在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 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 2

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

Error: Tactic failure: Setoid library not loaded.

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

Require Import Setoid.

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

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不会在绑定器(例如lambda)下重写，因为如果它重写了，你就可以从fun x => x + 0重写到fun x => x，这在普通的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.