在Coq中，如何定义像A = {x | f（x）= 0}？ [英] In Coq, how to define a set like A = {x | f(x) = 0}?

问题描述

我是使用Coq的新手。我想问是否要定义一个像
A = {x | f（x）= 0} ，
我该怎么做？
我写类似的东西：

I am a newbie in using Coq. I want to ask if I want to define a set like A = {x | f(x) = 0}, how could I do that? I write something like:

Definition f0 := nat->nat. 

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

它们未按预期工作。

非常感谢。

推荐答案

与您写的差不多。首先，您必须具有一些功能 f0：nat-> nat 您要应用此定义的位置。您在这里做什么

More or less like you wrote. First, you have to have some function f0 : nat -> nat that you want to apply this definition to. What you did here

Definition f0 := nat -> nat.

被命名为 nat-> nat 的功能从自然到自然 f0 。您可能已经想到了这样的东西：

was to name the type nat -> nat of functions from naturals to naturals f0. You probably had in mind something like this:

Variable f0 : nat -> nat.

这声明了一个变量 f0 类型 nat-> nat 。现在，我们可以将您的原始描述调整为Coq代码：

This declares a variable f0 that belongs to the type nat -> nat. Now we can adapt your original description to Coq code:

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

这里有两件事要注意。首先，您可能想稍后将此定义应用于 specific 函数 f0：nat-> nat ，例如前置函数 pred：nat-> nat 。在这种情况下，您应该将代码放在以下部分中：

There are two things to be aware of here. First, you might want to apply this definition later to a particular function f0 : nat -> nat, such as the predecessor function pred : nat -> nat. In this case, you should enclose your code in a section:

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

在此部分之外， A 实际上是函数（nat-> nat）->设置，它需要一个函数 f0：nat-> nat 设置为 {x：nat | f0 x = 0} 。您可以像使用其他任何功能一样使用 A ，例如

Outside of the section, A is actually a function (nat -> nat) -> Set, that takes a function f0 : nat -> nat to the type {x : nat | f0 x = 0}. You can use A as you would use any other function, e.g.

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

您必须记住的第二件事是Coq中的 Set 与传统数学中的集合不同。在数学中，集合 {x | f（x）= 0} 也是自然数集的元素。但不在Coq中。在Coq中，您需要应用显式投影函数 proj1_sig 来转换 {x的元素： f0 x = 0} 到 nat 。

The second thing you must keep in mind is that a Set in Coq is not the same thing as a set in conventional mathematics. In math, an element of the set {x | f(x) = 0} is also an element of the set of natural numbers. But not in Coq. In Coq, you need to apply an explicit projection function proj1_sig to convert an element of {x : nat | f0 x = 0} to a nat.

这篇关于在Coq中，如何定义像A = {x | f（x）= 0}？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！