relation - Coq:通过替换应用传递性

Question

我想在 Coq 中证明这个引理:

a : Type
b : Type
f : a -> b
g : a -> b
h : a -> b
______________________________________(1/1)
(forall x : a, f x = g x) ->
(forall x : a, g x = h x) -> forall x : a, f x = h x

我知道 Coq.Relations.Relation_Definitions 定义了关系的传递性:

定义及物:Prop := forall x y z:A, R x y -> R y z -> R x z。

简单地使用证明策略应用传递性显然是失败的。如何将及物性引理应用于上述目标？

Answer 1

传递性策略需要一个参数，它是您要引入到等式中的中间项。首先调用 intros (这几乎总是证明中要做的第一件事)，以便在环境中很好地实现假设。然后你可以说传递性(g x)，然后你就剩下了一个假设的两个直接应用。

intros.
transitivity (g x); auto.

您还可以让 Coq 猜测要使用哪个中间项。这并不总是有效，因为有时 Coq 会找到一个最终不起作用的候选者，但这种情况很简单并且可以立即起作用。 传递性应用的引理是eq_trans；使用 eapply eq_trans 使子项保持打开状态 (?)。第一个 eauto 选择适用于证明的第一个分支的子项，在这里它也适用于证明的第二个分支。

intros.
eapply eq_trans.
eauto.
eauto.

这可以缩写为intros； eapply eq_trans； eauto。它甚至可以进一步缩写为

eauto using eq_trans.

eq_trans 不在默认提示数据库中，因为它经常导致不成功的分支。