gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-02 19:51:32 24 4
gpt4 key购买 nike

我想在 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。

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

最佳答案

传递性策略需要一个参数,它是您要引入到等式中的中间项。首先调用 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 不在默认提示数据库中,因为它经常导致不成功的分支。

关于relation - Coq:通过替换应用传递性,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/22811700/

24 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com