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定义了关系的传递性:

Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z.

简单地使用证明策略apply transitivity显然会失败.如何将传递性引理应用于上述目标？

Answer 1

该transitivity策略需要一个参数,就是要引入平等中期.第一次调用intros(这几乎总是在证明中做的第一件事)在环境中很好地得到假设.然后你可以说transitivity (g x),你有两个直接的假设应用.

intros.
transitivity (g x); auto.

您还可以让Coq猜测要使用哪个中间术语.这并不总是有效,因为有时候Coq会找到一个最终不能解决的候选人,但是这个案例很简单并且可以立即使用.transitivity适用的引理是eq_trans; 用于eapply eq_trans保留子项open(?).第一个eauto选择一个适用于证明的第一个分支的子项,这里它也适用于证明的第二个分支.

intros.
eapply eq_trans.
eauto.
eauto.

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

eauto using eq_trans.

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