关于 Coq 中的 refine 策略

Question

考虑以下行（在 Coq 中）：

Variable A : Type.
Variable  f g : A -> A.
Axiom Hfg : forall x, f x = g x.
Variable a b : A.
Axiom t : g a = g b.
Goal f a = g b.

战术refine (eq_trans (Hfg _) t)解决了目标。也就是说，Coq 能够在没有帮助的情况下用 a 替换空洞。但是战术refine (eq_trans (Hfg a) _)用目标g a = g b代替了上面的目标。

但是，Coq 无法单独找到 t。策略同上 refine (eq_trans (Hfg _) _)。

Coq 能够猜出第一个洞而不是第二个洞是否有特殊原因？

Answer 1

（我不是 100% 确定我在这里写的是什么，但是）Coq 从来没有 'guess' 任何东西，但它可以从更复杂的信息中推断出信息。您的一般方案是要求 Coq 使用相等的传递性来解决您的目标。因此，Coq 需要两个相等的语句才能成功。

在第一种情况下，您为 Coq 提供了解决目标所需的一切，即 t : g a = g b 和 Hfg _ : f _ = g _。由于 eq_trans 迫使 _ 成为 a，因此没有什么可以证明的了。

在第二种情况下，你只喂 coq Hfg a : f a = g a 所以它错过了 g a = g b 来解决目标。是的，它在上下文中，但除非您明确要求，否则 Coq 不会使用自动化。

Answer 2

您的目标需要两个公理 Hfg 和 t。 Coq 只会在证明中使用明确给出的公理或在提示数据库中找到公理。所以你的证明需要同时出现Hfg和t。

refine (eq_trans (Hfg _) t) 包含两个公理。 Hfg 的参数由术语的类型强加：

eq_trans 具有 ?1 = ?2 -> ?2 = ?3 -> ?1 = ?3 形式的类型，将 t 的类型与 ?2 = ?3 统一产生 ?2 := g a 和 ?3 := g b .
Hfg _ 具有 f ?4 = g ?4 形式的类型，将其与 ?1 = ?2 统一产生 ?4 := a 和 ?1 := f a.

Coq 能够进行这种类型推断，因此该术语是完全类型化的并完成了证明。

相比之下，对于 refine (eq_trans (Hfg a) _)，Coq 应用它给出的东西，发现证明中有一个漏洞：它需要 g a = g b 的证明。这是一个公理，但 Coq 不会自动应用它：它让您选择决定是使用这个证明还是使用该事实的其他证明。

证明此目标的自然方法是使用 rewrite tactic.

Goal f a = g b.
rewrite Hfg.
rewrite t.
reflexivity.
Qed.

您可以通过使用 Hint Rewrite then applying autorewrite 声明公理让 Coq 找到合适的等式来应用。请注意，autorewrite 盲目地应用等式，它不受目标的影响。

Hint Rewrite Hfg t : my_equalities.
Goal f a = g b.
autorewrite with my_equalities.
reflexivity.
Qed.

或者，您可以应用 congruence tactic，它负责链接多个等式。您需要先将公理纳入假设。

Goal f a = g b.
generalize Hfg t; intros.
congruence.
Qed.

About the refine tactic in Coq