我是使用Coq的新手。我想問一下,如果我想定義一組像 A = {x | f(x) = 0}
, 我怎麼能做到這一點? 我寫的東西,如:在Coq中,如何定義一個像A = {x |的集合f(x)= 0}?
Definition f0 := nat->nat.
Definition A : Set :=
forall x, f0 x -> 0.
預期他們沒有工作。
非常感謝。
我是使用Coq的新手。我想問一下,如果我想定義一組像 A = {x | f(x) = 0}
, 我怎麼能做到這一點? 我寫的東西,如:在Coq中,如何定義一個像A = {x |的集合f(x)= 0}?
Definition f0 := nat->nat.
Definition A : Set :=
forall x, f0 x -> 0.
預期他們沒有工作。
非常感謝。
或多或少像你這樣寫道。首先,你必須有一些你想要應用這個定義的功能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
。
非常感謝,這是如此完美! :) –