coq - 将包含 y 的公式转换为包含 f(x) 的公式的定理的 Coq 证明

Question

我想证明:

forall (T : Type) (U : Type) (P : T -> U -> Prop),
  (forall (x : T), exists (y : U), P x y)
    -> (exists (f : T -> U), forall (x : T), P x (f x))

用简单的英语来说，我想做的是表达将 y 转换为 f(x) 的能力。例如，将 y = x + 1 更改为 f(x) = x + 1。

用反向蕴涵箭头证明目标(将 f(x) 变成 y)需要 4 行。但是，为了实现这个目标，我想不出在 intros 之后可以做什么。

我什至不确定这在 Coq 中是否可行。如果没有，是否有更好的方式来表达我想做的事情？

Answer 1

你的结果是选择公理的一种形式，没有额外的公理就无法在 Coq 中证明。问题在于，为了构造 f，您需要从 exists y, P x y 的证明中提取元素 y : U。 Coq 在设计上禁止这样做，以确保证明没有计算意义。

绕过此限制的一种方法是用计算相关的对应项替换通常的存在项。然后我们得到 Bob Harper 所说的选择定理:

Goal forall (T : Type) (U : Type) (P : T -> U -> Prop),
  (forall (x : T), { y : U | P x y })
    -> (exists (f : T -> U), forall (x : T), P x (f x)).
Proof.
intros T U P H.
exists (fun x => proj1_sig (H x)).
intros x.
now apply proj2_sig.
Qed.