Library nat_base
Natural Numbers
This definition introduces a new type nat
It also introduces two constructors for this type.
O that is just a natural number
and S that is a function that given natural number returns
another natural number - the successor
Now to do something interesting we need some operations on
nat. Let us start with addition. To define m + n we proceed
by doing case analysis on m. We have two cases corresponding
to the two constructors of type nat. If m is 0 then the
result is simply n. Otherwise m is a successor of some
number p and S p + n equals S (p + n). This is expressed
in Rocq with the following recursive definition
Fixpoint plus (m n : nat) {struct m} : nat :=
match m with
| O => n
| S p => S (plus p n)
end.
Print plus.
match m with
| O => n
| S p => S (plus p n)
end.
Print plus.
For such recursive definition to be accepted by Rocq it must be
terminating, i.e. it is not allowed that the sequence of
recursive calls can go on forever. To ensure this Rocq uses a
very simple criterion - one of the arguments must be structuraly
decreasing along the recursive call. The annotation {struct m}
in the above definition is used to indicated that m is the
decreasing argument. Indeed in the second case the first argument
to plus equals S p and is replaced by p in the recursive
call
Let us check the type of plus
We can also see its full definition
Print plus.
Now let us prove a simple lemma stating that O is a neutral
element for addition.