Примените функцию к обеим сторонам равенства в гипотезе Coq

Question

Вопрос, который у меня есть, очень похож на тот, который представлен в ссылке ниже, но по гипотезе вместо цели.

Применить функцию к обеим сторонам равенства в Coq?

Скажем, у меня есть следующее определение:

Definition make_couple (a:nat) (b:nat) := (a, b).

И следующую лемму для доказательства:

a, b : nat
H : (a, b) = make_couple a b
-------------------------------
(some goal to prove)

Я хотел бы сформулировать следующую гипотезу:

new_H : fst (a, b) = fst (make_couple a b)

Один из способов - написать явно assert, а затем использовать eapply f_equal:

assert (fst (a, b) = fst (make_couple a b)). eapply f_equal; eauto.

Но я бы хотел, по возможности, избежать явного утверждения утверждения. Я хотел бы иметь какую-то тактику или эквивалент, который бы работал так:

apply_in_hypo fst H as new_H

Есть ли в Coq что-нибудь, что могло бы приблизиться к этому?

Спасибо за ответы.

Answer 1

Ты можешь использовать f_equal Лемма, чтобы сделать это.

About f_equal.

f_equal : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y

Arguments A, B, x, y are implicit
Argument scopes are [type_scope type_scope function_scope _ _ _]
f_equal is transparent
Expands to: Constant Coq.Init.Logic.f_equal

Вот как вы можете применить это к гипотезе:

Goal forall a b : nat, (a, b) = (a, b) -> True.
  intros a b H.
  apply (f_equal fst) in H.

Приведенный выше фрагмент может быть переписан в более сжатой форме, используя интро-шаблоны:

  Restart.
  intros a b H%(f_equal fst).
Abort.