The Coq mailing list

[David P Á <david AT picon.email>]

On 24/05/2017 6:50, nikhil kaushik wrote:
> How does O becomes 0 when we use it in definition of

This definition is of the Peano naturals. Peano axioms say: there is a
constant (0) which is a natural number. This corresponds to the
constructor O which takes no arguments. Then, for every natural, one can
construct a natural S(n) where S is the successor. This is the 2nd
constructor which takes a nat argument.

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

O doesn't represent natural numbers, O is a constructor for a natural.
It constructs 0.

> 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' pattern
> match gives us predecessor of n.

pred gives you the predecessor of a number. Because Coq wants totality
here, pred must be defined for all n, including 0. Unfortunately this
requires us to say that the predecessor of 0 is 0 (since -1 is not in
nat). So hence:

| O => O

matches O and produces O. (pred O) -> O.

And when the natual is of the form S n' the match gives us n'. So say
you have:
S(S(S(O))), which is 3.
You go through the match. Constructors are disjoint so S something can't
match O, so you go to the next one, S n'. So n' becomes the thing inside
the first S, S(S(O)), and the return of the match is that n', which is
2, predecessor of 3.

HTH,
--David.