Coq：根据唯一性和存在性定理定义函数

Question

为了尽可能地隔离这个问题，假设我如下开始一个 Coq 会话。

Parameter A : Type.
Parameter B : Type.
Parameter P : A -> B -> Prop.

Axiom existence : forall a : A, exists b : B, P a b.
Axiom uniqueness : forall a : A, forall b b' : B, P a b -> P a b' -> b = b'.

从这里开始，我想将函数 f : A -> B 定义为 P a (f a) 始终为真的唯一函数。

我该怎么做？ 可以我这样做吗？显然我应该从类似的东西开始

Definition f : A -> B.
  intro a.
  assert (E := existence a).
  assert (U := uniqueness a).

...但是我如何根据这些假设实际编写函数？

Answer 1

我认为在您当前的设置下这是不可能的。

问题是你可以从existence定理中提取b，但这只能存在于Prop中。

所以，我相信您要么必须将A 和B 移动到Prop，或者将existence 和uniqueness 移动到Set。

这将导致以下任一情况：

---

Parameter A : Prop.
Parameter B : Prop.
Parameter P : A -> B -> Prop.

Axiom existence : forall a : A, exists b : B, P a b.
Axiom uniqueness : forall a : A, forall b b' : B, P a b -> P a b' -> b = b'.

Definition f : A -> B.
  intro a. destruct (existence a) as [b _]. exact b.
Defined.

---

Parameter A : Set.
Parameter B : Set.
Parameter P : A -> B -> Prop.

Axiom existence : forall a : A, { b : B | P a b }.
Axiom uniqueness : forall a : A, forall b b' : B, P a b -> P a b' -> b = b'.

Definition f : A -> B.
  intro a. destruct (existence a) as [b _]. exact b.
Defined.

---

很可能这些都不是您真正想要的。在这种情况下，我需要更多详细信息才能提供帮助。可能是你愿意做一些在直觉主义环境下不可能的事情。

PS：我不是专家。