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?
The
transitivity
tactic requires an argument, which is the intermediate term that you want to introduce into the equality. First callintros
(that's almost always the first thing to do in a proof) to have the hypotheses nicely in the environment. Then you can saytransitivity (g x)
and you're left with two immediate applications of an assumption.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 iseq_trans
; useeapply eq_trans
to leave a subterm open (?
). The firsteauto
chooses a subterm that works for the first branch of the proof, and here it also works in the second branch of the proof.This can be abbreviated as
intros; eapply eq_trans; eauto
. It can even be abbreviated further toeq_trans
isn't in the default hint database because it often leads down an unsuccessful branch.