Coq - 向上下文添加选择函数

如何解决Coq - 向上下文添加选择函数

假设我在 Coq 证明中，并且当前上下文包括形式的假设

H : forall a : A,P a -> exists b : B,Q a b

哪里

A B:Type
P : A -> Prop
Q : A -> B -> Prop

然后，我想在上下文中添加两个新术语：

f : A -> B
H' : forall a : A,P a -> Q a (f a)

我该怎么做？我很高兴添加非构造公理来实现这一点。

解决方法

在一般情况下，这是不可能的。请看以下内容：

Definition A : Type := True.
Definition B : Type := False.
Definition P : A -> Prop := (fun a : A => False).
Definition Q : A -> B -> Prop := (fun (a : A) (b : B) => True).

Example H_is_trivial: forall a : A,P a -> exists b : B,Q a b.
Proof.
  intros a HP.
  destruct HP.
Qed.

Example f_cannot_exist: (exists f : A -> B,forall a : A,P a -> Q a (f a)) -> False.
Proof.
  intros.
  destruct H as [f H].
  apply f.
  exact I.
Qed.

所以存在 A、B、P 和 Q 的赋值，其中你的 H 成立，但可以证明你的 f 不存在。

对于细化问题，你可以定义一个simga类型{a | P a} 并用选择公理证明：

Require Import ClassicalChoice.

Section Test.
Variable A B : Type.
Variable P : A -> Prop.
Variable Q : A -> B -> Prop.
Variable H : forall a : A,Q a b.

Definition AP := { a : A | P a }.
Definition QAP (a : AP) (b : B) := Q (proj1_sig a) b.

Lemma f_exists: exists f : AP -> B,(forall ap : AP,QAP ap (f ap)).
  apply choice.
  intros ap.
  specialize (H (proj1_sig ap) (proj2_sig ap)).
  destruct H as [b HQ].
  exists b. exact HQ.
Qed.

再次拆开 sigma 类型并解决您的直接问题应该不难，但无论如何 sigma 类型可能更方便。