CODEWITHSUNDEEP
coq
user520415
user520415

Reputation:

How do you define an ordered pair in Coq?

I am a programmer, but an ultra-newbie to Coq, and have tried to figure out the tutorials without much success. My question is very simple: How does one define an ordered pair (of natural numbers) in Coq?

Here was my attempt:

Variable node1 : nat.
Variable node2 : nat.
Inductive edge : type := node1 -> node2.

(Note that "edge" is the name I am using for ordered pair.) The third line gives a syntax error, suggesting that I need a '.' in the sentence somewhere.

I don't know what to do. Any help would be great! (Also, is there a tutorial that helps teach very basic Coq concepts better than the ones that are easily seen given a Google search for "Coq Tutorial" ?)

Upvotes: 2

Views: 2131

Answers (1)

Kristopher Micinski
Kristopher Micinski

Reputation: 7672

You can do this simply enough by just using a Coq definition:

Definition ordered_pair := (nat * nat) % type.

This introduces ordered_pair as a synonym for (nat * nat) % type (note that the % type is required to get Coq to interpret * in the scope of types, rather than naturals). The real power is in the use of *:

Inductive prod (A B:Type) : Type :=
  pair : A -> B -> prod A B.

(From http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html)

You get all the necessary elimination principles, etc... from there.

Upvotes: 3

Related Questions