在Coq中，如何定義一個像A = {x |的集合f（x）= 0}？

Question

我是使用Coq的新手。我想問一下，如果我想定義一組像 A = {x | f(x) = 0}， 我怎麼能做到這一點？ 我寫的東西，如：

Definition f0 := nat->nat. 

Definition A : Set := 
    forall x, f0 x -> 0. 

預期他們沒有工作。

非常感謝。

Answer 1

或多或少像你這樣寫道。首先，你必須有一些你想要應用這個定義的功能f0 : nat -> nat。你做了什麼在這裏

Definition f0 := nat -> nat. 

是名字從土黃的功能nat -> nat類型土黃f0。你可能想到的是這樣的：

Variable f0 : nat -> nat. 

聲明一個變量f0屬於類型nat -> nat。現在，我們可以適應您的原始描述勒柯克代碼：

Definition A : Set := {x : nat | f0 x = 0}. 

有兩件事情需要注意的這裏。首先，你可能想在以後將此定義爲特定功能f0 : nat -> nat，如前任功能pred : nat -> nat。在這種情況下，你應該附上你的代碼段：

Section Test. 
Variable f0 : nat -> nat. 
Definition A : Set := {x : nat | f0 x = 0}. 
End Test. 

的部分之外，A實際上是一個功能(nat -> nat) -> Set，這需要一個功能f0 : nat -> nat的類型{x : nat | f0 x = 0}。您可以像使用任何其他功能一樣使用A，例如

Check (A pred). 
(* A pred : set *) 

你必須記住的第二件事是，在勒柯克一個Set是不一樣的東西在傳統的數學一組。在數學中，集合{x | f(x) = 0}的元素也是自然數集的元素。但不是在Coq。在勒柯克，您需要申請一個明確的投影功能proj1_sig到{x : nat | f0 x = 0}元素轉換爲nat。