CODEWITHSUNDEEP
coq
Tianyu Sun
Tianyu Sun

Reputation: 11

In Coq, how to define a set like 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.

They are not working as expected.

Thanks a lot.

Upvotes: 1

Views: 197

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

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.

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.

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}.

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.

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

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.

Upvotes: 5

Related Questions