在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.现在我们可以根据Coq代码调整您的原始描述:

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 *)

你必须记住的第二件事是,SetCoq中的a与传统数学中的集合不同.在数学中,集合{x | f(x) = 0}的元素也是自然数集的元素.但不是在Coq.在Coq中,您需要应用显式投影函数proj1_sig将元素转换{x : nat | f0 x = 0}为a nat.