通過coq中的屬性定義

Question

我無法正式確定以下形式的定義：定義一個整數，使某些屬性成立。

比方說，我正式的屬性的定義：

Definition IsGood (x : Z) : Prop := ... 

現在我需要形式的定義：

Definition Good : Z := ... 

假設我證明，用該財產的整數存在，是獨一無二的：

Lemma Lemma_GoodExistsUnique : exists! (x : Z), IsGood x. 

有定義Good一個簡單的方法使用IsGood和Lemma_GoodExistsUnique？

由於該屬性是在整數上定義的，所以似乎不需要額外的公理。無論如何，我不知道如何添加類似於選擇公理的東西可以幫助定義。

另外，我在正式定義下面的表格時遇到了問題（我懷疑這與上面描述的問題有關，但請指出是否不是這種情況）：對於每個x，存在y，並且這些y是不同的x。等，例如，如何界定是否有使用IsGoodN明顯好整數：

Definition ThereAreNGoodIntegers (N : Z) (IsGood : Z -> Prop) := ...? 

在現實世界中的數學，定義一樣，出現現在每一次，所以這不應該是難以形式化，如果Coq旨在適用於實際數學。

Answer 1

你的第一個問題的簡短答案是：總的來說，這是不可能的，但在你的特定情況下，是的。

在Coq理論中，命題（即Prop）及其證明具有非常特殊的地位。特別是，通常不可能寫出選擇操作符來提取存在證據的證人。這樣做是爲了使理論與某些公理和原理相一致，例如證明無關性，即證明給定命題的所有證明都彼此相等。如果你想能夠做到這一點，你需要添加這個選擇算子作爲你的理論的一個額外的公理，如standard library。

但是，在某些特定情況下，它可能從提取一個證明出來的抽象存在證明而沒有任何額外的公理。特別是，當有問題的財產是可確定的時，可以對可數類型（例如Z）這樣做。例如，您可以使用Ssreflect庫中的choiceType接口來獲取您想要的內容（查找xchoose函數）。

這就是說，我通常會建議與做這種風格的事情，因爲它會導致不必要的複雜性。直接定義Good，而不訴諸存在證明可能更容易，然後單獨證明Good具有所需的屬性。

Definition Good : Z := (* ... *) 
Definition IsGood (z : Z) : Prop := (* ... *) 

Lemma GoodIsGood : IsGood Good. 
Proof. (* ... *) Qed. 

Lemma GoodUnique : forall z : Z, IsGood z -> z = Good. 

如果你絕對要定義Good與存在的證據，你也可以改變的Lemma_GoodExistsUnique證明在Type而不是Prop使用結締組織，因爲它允許您直接使用proj1_sig函數提取證人：

Lemma Lemma_GoodExistsUnique : {z : Z | Good z /\ forall z', Good z' -> z' = z}. 
Proof. (* ... *) Qed. 

至於你的第二個問題，是的，它與第一點有點相關。再次，我建議您寫下一個函數y_from_x與類型Z -> Z，它將計算y給出x，然後分別證明此函數以特定方式關聯輸入和輸出。然後，通過證明y_from_x是內射的，你可以說y對於不同的x s是不同的。

另一方面，我不確定你的最後一個例子與第二個問題有什麼關係。如果我理解你想要正確地做什麼，你可以寫類似

Definition ThereAreNGoodIntegers (N : Z) (IsGood : Z -> Prop) := 
    exists zs : list Z, 
    Z.of_nat (length zs) = N 
    /\ NoDup zs 
    /\ Forall IsGood zs. 

這裏，Z.of_nat : nat -> Z是土黃爲整數規範注射，NoDup是謂詞斷言列表不包含重複的元素，和Forall是一個高階謂詞，聲明給定謂詞（在本例中爲IsGood）包含列表的所有元素。

作爲最後一點，我建議不要使用Z來處理只能涉及自然數的事情。在你的例子中，你用一個整數來談論一個集合的基數，這個數字總是一個自然數。