coq - 关于 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 从不“猜测”任何东西，但它可以从更复杂的信息中推断出信息。您的一般方案是要求 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 不会使用自动化。