Coq

Question

假设我在 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)

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

Answer 1

在这种普遍情况下，这是不可能的。看下面：

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.

所以存在你的H成立的A、B、P、Q的赋值，但可以证明你的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, P a -> exists b : B, 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 类型可能更方便。

Coq - 向上下文添加选择功能

Coq - adding choice function to context

math

proof