勒柯克：应用及物与替代

我要证明这个引理在勒柯克：勒柯克：应用及物与替代

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明显失败。我如何将这个传递性引理应用于上面的目标？

来源

2014-04-02 SvenK

的transitivity战术需要一个参数，就是要引入平等中期。首先拨打电话intros（这几乎总是首先要做的证据），以便在环境中有很好的假设。那么你可以说transitivity (g x)，你留下了两个立即申请的假设。

intros. 
transitivity (g x); auto.

您还可以让Coq猜测使用哪个中间项。这并不总是奏效，因为Coq有时会发现一个候选人最终无法解决问题，但这种情况很简单，并且可以立即生效。 transitivity适用的引理是eq_trans;使用eapply eq_trans使子项开放（?）。第一个eauto选择一个适用于证明的第一个分支的子项，这里它也适用于证明的第二个分支。

intros. 
eapply eq_trans. 
eauto. 
eauto.

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

eauto using eq_trans.

eq_trans是不是在默认的提示数据库，因为它往往会导致下一个不成功的分支。

来源

2014-04-02 14:37:11 Gilles

好吧，我是在错误的轨道上。这里是引理的证明：

Lemma fun_trans : forall (a b:Type) (f g h:a->b), 
    (forall (x:a), f x = g x) -> 
    (forall (x:a), g x = h x) -> 
    (forall (x:a), f x = h x). 
Proof. 
    intros a b f g h f_g g_h x. 
    rewrite f_g. 
    rewrite g_h. 
    trivial. 
Qed.

来源

2014-04-02 13:41:22 SvenK

勒柯克：应用及物与替代

回答

相关问题