将函数应用于 Coq 假设中的等式两边

Question

我的问题与下面 link 中提出的问题非常相似，但基于假设而不是目标。

Apply a function to both sides of an equality in 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.

但我想尽可能避免显式编写断言。我想要一些像这样工作的策略或等效策略：

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.

可以使用 intro-patterns:

以更简洁的方式重写上面的代码片段

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

将函数应用于 Coq 假设中的等式两边

Apply a function to both sides of equality in a Coq hypothesis

coq

coq-tactic