如何讀取ex_intro的定義？

Question

我讀Mike Nahas's introductory Coq tutorial，它說：

的參數爲 「ex_intro」 是：

• 謂語
• 證人
• 的所謂預測與證人證明

我看着the definition：

Inductive ex (A:Type) (P:A -> Prop) : Prop := 
    ex_intro : forall x:A, P x -> ex (A:=A) P. 

我在解析它時遇到了問題。表達式forall x:A, P x -> ex (A:=A) P的哪些部分對應於這三個論點（謂詞，見證和證明）？

Answer 1

要了解邁克的意思，這是更好地啓動勒柯克解釋和查詢的ex_intro類型：

Check ex_intro. 

之後，應看到：

ex_intro 
    : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists x, P x 

這是說ex_intro需要不只有3個，但4個參數：

• 這個類型你正在量化，A;
• 謂詞P : A -> Prop;
• 見證人x : A;和
• 的P x證明，聲稱x是一個有效的見證。

如果將所有這些內容組合在一起，就會得到exists x : A, P x的證明。例如，@ex_intro nat (fun n => n = 3) 3 eq_refl是exists n, n = 3的證明。

因此，實際的類型ex_intro和一個你定義閱讀之間的區別在於，前者包括所有在頭給出的參數 - 在這種情況下，A和P。

Answer 2

呀，這些感應類型定義可能會難以閱讀。

第一部分是：

Inductive ex (A:Type) (P:A -> Prop) : Prop := 

這是與類型本身相關聯。所以你看一個ex任何時候，就會有一個A和和P和ex將Prop類型。暫時跳過A，讓我們關注P這是謂詞。因此，如果我們以「存在自然數爲素數」爲例，P可能是is_prime，其中is_prime以nat（自然數）作爲參數，並且如果nat爲素數則可以存在證明。

在這個例子中，A將是nat。在本教程中，A未被提及，因爲Coq始終可以推斷它。給定謂詞，Coq可以通過查看謂詞參數的類型來獲得A的類型。

總而言之，在我們的例子中，類型將是ex nat is_prime。這說明存在一個非常重要的nat，但它沒有說明哪個nat。當我們構建一個ex nat is_prime時，我們需要說出哪一個 - 我們需要一個「證人」。這使我們在構造函數的定義：

ex_intro : forall x:A, P x -> ex (A:=A) P. 

構造名爲ex_intro。這裏棘手的是構造函數具有該類型的所有參數。因此，在我們找到ex_intro之後列出的那些之前，我們必須包含類型：A和P。

後這些參數來ex_intro後列出的：x，這是見證，P x，這是一個證明，斷言有效，對於證人。使用我們的示例，x可能是2，P x將是(is_prime 2)的證明。

構造函數需要指定它正在構造的類型ex的參數。這是箭頭後面發生的事情（->）。這些不需要與調用構造函數時使用的參數相匹配，但通常它們都可以。爲了實現這一點，參數A是而不是被推斷 - 它正在被明確地傳遞。 (A:=A)表示ex中的參數A應該等於調用構造函數中的A。同樣，ex的參數P正被設置爲P從調用構造函數。

因此，如果我們用(prime 2)類型有proof_that_2_is_prime，我們可以稱之爲ex_intro is_prime 2 proof_that_2_is_prime，它將有型ex nat is_prime。我們的證明是存在一個自然數是質數的證明。

---

直接回答你的問題：在表達forall x:A, P x -> ex (A:=A)，x:A是證人和P x是證人是真實的證明。該表達式不包含謂詞，因爲它是必須傳遞給構造函數ex_intro的類型參數的一部分。本教程的參數列表不包括A，因爲是由Coq推斷的。

我希望你明白爲什麼我認爲這個討論對我的教程太詳細了！感謝您的問題。