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

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

Примените функцию к обеим сторонам равенства в 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)

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

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

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

apply_in_hypo fst H as new_H

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

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


coq coq-tactic
person potterman28wxcv    schedule 21.06.2018    source источник
comment
Это связанный вопрос.   -  person Anton Trunov    schedule 21.06.2018

Ответы (1)


arrow_upward
3
arrow_downward

Для этого вы можете использовать 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.
person Anton Trunov    schedule 21.06.2018
comment
Спасибо! Именно то, что я искал - person potterman28wxcv; 21.06.2018