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。

所以，我相信你要麼必須在Prop移動A和B，或在Set移動existence和uniqueness。

這將導致以下任一：

---

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：我不是專家。