5

I want to proof this lemma in 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

I know that Coq.Relations.Relation_Definitions defines transitivity for relations:

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

Simply using the proof tactic apply transitivity obviously fails. How can I apply the transitivity lemma to the goal above?

4

2 回答 2

6

该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-02T14:37:11.200 回答
1

好吧，我走错了路。下面是引理的证明：

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-02T13:41:22.517 回答