The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

Hi Nikhil,

you got it a bit wrong. 0 does not represent natural numbers. It represent the number zero. Coq uses the Peano definition of natural number (or recursive definition) :
- a number is zero
- or a number is the follower (successor) of another number.

This gives us :
0 = 0
Sucessor of 0 = S 0 = 1
Sucessor of 1 = S 1 = S (S 0) = 2
Sucessor of  2 = S 2 = S (S (S 0)) = 3

etc...

the pred function return the predecessor or the number "before". If you were to see it as a function it would be :

f : x ->
    0  if x = 0
    otherwise  x - 1

The predecessor of 3 is 2 or pred (S (S (S 0))) = S (S 0).

If you try this definition of pred, it won't compile : it is missing a case.

Definition pred (n : nat) : nat :=
  match n with
    | S n' => n'
  end.

the match in Coq checks the type of n, sees the induction principle and notice that you are missing the case where n = 0.

In the inductive definition of nat, S and 0 are what we call "constructors".

Hope this helps.

On 05/24/2017 06:50 AM, nikhil kaushik wrote:

I was going through the book Software foundations to learn Coq and I got stuck on Numbers. In this Type definition

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

How does O becomes 0 when we use it in definition of

Definition pred (n : nat) : nat :=
  match n with
    | O => O
    | S n' => n'
  end.

I only understood that O represents natural numbers and S takes a natural number and return another natural number so S is a function. What I do not get is when our defined nat data type is used in preddefinition how does O represent 0? And how does S n' pattern match gives us predecessor of n.

--

~Nikhil Kaushik

-- 
Kind regards,

Benoît Viguier
Software Engineer - PhD Student | Cryptography & Formal Methods
Radboud University | Mercator 1, room 03.17, Toernooiveld 212
6525 EC Nijmegen, the Netherlands | www.viguier.nl

--------------------------------------------------------------------------
This message (and any attachments) is intended solely for the addressee(s)
and may contain confidential information. If you are not the addressee, do
not copy this message (and any attachments), forward or share this message
with third parties. You are requested to notify the sender immediately and
delete this message.

Attachment: signature.asc
Description: OpenPGP digital signature