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 находит кандидата, который не работает в конце, но этот случай достаточно прост и работает немедленно. Лемма о том, что transitivity применяется это eq_trans; использование eapply eq_trans оставить субтерм открытым (?). Первый eauto выбирает подтерм, который работает для первой ветви доказательства, и здесь он также работает во второй ветви доказательства.

intros.
eapply eq_trans.
eauto.
eauto.

Это может быть сокращено как intros; eapply eq_trans; eauto, Это может быть сокращено до

eauto using eq_trans.

eq_trans отсутствует в базе данных по умолчанию, так как часто приводит к неудачной ветке.

Answer 2

Хорошо, я был на неправильном пути. Вот доказательство леммы:

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.