Coq: apply transitivity with substitution

Question

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?

Gymno

Answer 1

The transitivity tactic requires an argument, which is the intermediate term that you want to introduce into the equality. First call intros (that's almost always the first thing to do in a proof) to have the hypotheses nicely in the environment. Then you can say transitivity (g x) and you're left with two immediate applications of an assumption.

intros.
transitivity (g x); auto.

You can also make Coq guess which intermediate term to use. This doesn't always work, because sometimes Coq finds a candidate that doesn't work out in the end, but this case is simple enough and works immediately. The lemma that transitivity applies is eq_trans; use eapply eq_trans to leave a subterm open (?). The first eauto chooses a subterm that works for the first branch of the proof, and here it also works in the second branch of the proof.

intros.
eapply eq_trans.
eauto.
eauto.

This can be abbreviated as intros; eapply eq_trans; eauto. It can even be abbreviated further to

eauto using eq_trans.

eq_trans isn't in the default hint database because it often leads down an unsuccessful branch.

Botzow

Answer 2

Ok, I was on the wrong track. Here is the proof of the lemma:

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.

Gymno