Peano number implementation in Coq

Question

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. What I do not get is when our defined nat data type is used in pred definition how does O represent 0? And how does S n' patter match gives us predecessor of n.

Answer 1

The Peano numbers

nat represents the natural numbers via the unary numeral system. The inhabitants (values) of the nat type are O, S O, S (S O), S (S (S O)), ..., S (S (S (S ... O)...).

We interpret the symbol O as the natural number zero. And S represents a single "tick" in unary representation, i.e. we interpret S as a constructor (it has nothing to do with object-oriented programming) which takes a natural number and yields the next natural number.

The predecessor function

pred is actually is not a very well-behaved function in a sense.

First of all, there is no predecessor of zero when we are talking about the natural numbers. But all functions in Coq must return a value, so if we want to keep the type of pred (which is nat -> nat) we must do something about pred O. It feels natural to just return O and get it over with. This gives us the first branch of the pattern-mathing expression (O => O).

Next, what do we return when we call pred on the number representing 1? Let's recall that we write 1 in Coq as S O. This is easy -- pred (S O) should return O. Now let's try 2: pred (S (S O)) should return S O. You see the pattern here? If we have a bunch of S's in front of an O, we strip one S off -- simple as that. The second branch of the pattern-matching expression (S n' => n') does exactly this: it takes a (non-zero) number of the form S n' and turns it into n' (not changing the original, of course).

Let me give an example. Let's calculate the predecessor of the number 3 step-by-step:

pred (S (S (S O)))

Unfold the definition of pred, substitute S (S (S O)) for n:

match S (S (S O)) with
| O => O
| S n' => n'
end

S (S (S O)) has form S n' (it starts with S), so we take the 2nd branch, binding n' to S (S O). How do we check that we didn't make a mistake here? If we substitute the definition of n' into S n' we should get back the original n: S n' = S (S (S O)) = n.

Now, we just return n':

S (S O)

As expected, we got 2 as the result!

Notations

There is a distinction between 0, 0, and O. The first zero (0) is a meta-level numeral for the natural number zero (it's how we designate zero in our metalanguage, e.g. English in this case). 0 is a notation for O, in other words 0 is syntactic sugar for O. As the Coq reference manual says (§1.2.4):

Numerals have no definite semantics in the calculus. They are mere notations that can be bound to objects through the notation mechanism (see Chapter 12 for details). Initially, numerals are bound to Peano’s representation of natural numbers (see 3.1.3).

It's easy to illustrate:

Check 0.                     (* 0 : nat *)
Check 5.                     (* 5 : nat *)
Unset Printing Notations.    (* Print terms as is, no syntactic sugar *)
Check 0.                     (* O : nat *)
Check 5.                     (* S (S (S (S (S O)))) : nat *)

You can overload numerals, here is an example with integers:

Set Printing Notations.
Require Import Coq.ZArith.ZArith.
Open Scope Z.
Check 0.                            (* 0 : Z *)
Check 5.                            (* 5 : Z *) 
Unset Printing Notations.
Check 0.                            (* Z0 : Z *)
Check 5.                            (* Zpos (xI (xO xH)) : Z *)

Upshot: the same notation can be tied to different terms. Coq defines some default notations, e.g. for such ubiquitous things as numbers.

If you wanted to define your own type to represent the natural numbers (my_nat) with possibly different names for O and S (like stop and tick), you'd have to write a plugin to map Coq numerals onto the terms of my_nat (see here).