# Library Coq.Init.Nat

# Peano natural numbers, definitions of operations

Definition succ := S.

Definition pred n :=

match n with

| 0 => n

| S u => u

end.

Fixpoint add n m :=

match n with

| 0 => m

| S p => S (p + m)

end

where "n + m" := (add n m) : nat_scope.

Definition double n := n + n.

Fixpoint mul n m :=

match n with

| 0 => 0

| S p => m + p * m

end

where "n * m" := (mul n m) : nat_scope.

Truncated subtraction: n-m is 0 if n<=m

Fixpoint sub n m :=

match n, m with

| S k, S l => k - l

| _, _ => n

end

where "n - m" := (sub n m) : nat_scope.

Fixpoint eqb n m : bool :=

match n, m with

| 0, 0 => true

| 0, S _ => false

| S _, 0 => false

| S n', S m' => eqb n' m'

end.

Fixpoint leb n m : bool :=

match n, m with

| 0, _ => true

| _, 0 => false

| S n', S m' => leb n' m'

end.

Definition ltb n m := leb (S n) m.

Infix "=?" := eqb (at level 70) : nat_scope.

Infix "<=?" := leb (at level 70) : nat_scope.

Infix "<?" := ltb (at level 70) : nat_scope.

Fixpoint compare n m : comparison :=

match n, m with

| 0, 0 => Eq

| 0, S _ => Lt

| S _, 0 => Gt

| S n', S m' => compare n' m'

end.

Infix "?=" := compare (at level 70) : nat_scope.

Fixpoint max n m :=

match n, m with

| 0, _ => m

| S n', 0 => n

| S n', S m' => S (max n' m')

end.

Fixpoint min n m :=

match n, m with

| 0, _ => 0

| S n', 0 => 0

| S n', S m' => S (min n' m')

end.

Fixpoint even n : bool :=

match n with

| 0 => true

| 1 => false

| S (S n') => even n'

end.

Definition odd n := negb (even n).

Fixpoint pow n m :=

match m with

| 0 => 1

| S m => n * (n^m)

end

where "n ^ m" := (pow n m) : nat_scope.

## Euclidean division

Fixpoint divmod x y q u :=

match x with

| 0 => (q,u)

| S x' => match u with

| 0 => divmod x' y (S q) y

| S u' => divmod x' y q u'

end

end.

Definition div x y :=

match y with

| 0 => y

| S y' => fst (divmod x y' 0 y')

end.

Definition modulo x y :=

match y with

| 0 => y

| S y' => y' - snd (divmod x y' 0 y')

end.

Infix "/" := div : nat_scope.

Infix "mod" := modulo (at level 40, no associativity) : nat_scope.

## Greatest common divisor

## Square root

Fixpoint sqrt_iter k p q r :=

match k with

| O => p

| S k' => match r with

| O => sqrt_iter k' (S p) (S (S q)) (S (S q))

| S r' => sqrt_iter k' p q r'

end

end.

Definition sqrt n := sqrt_iter n 0 0 0.

## Log2

10 9 8 7 * 6 * 5 ... 4 3 * 2 * 1 * * 0 * * *

Fixpoint log2_iter k p q r :=

match k with

| O => p

| S k' => match r with

| O => log2_iter k' (S p) (S q) q

| S r' => log2_iter k' p (S q) r'

end

end.

Definition log2 n := log2_iter (pred n) 0 1 0.

Iterator on natural numbers

Bitwise operations
We provide here some bitwise operations for unary numbers.
Some might be really naive, they are just there for fullfiling
the same interface as other for natural representations. As
soon as binary representations such as NArith are available,
it is clearly better to convert to/from them and use their ops.

Fixpoint div2 n :=

match n with

| 0 => 0

| S 0 => 0

| S (S n') => S (div2 n')

end.

Fixpoint testbit a n : bool :=

match n with

| 0 => odd a

| S n => testbit (div2 a) n

end.

Definition shiftl a := nat_rect _ a (fun _ => double).

Definition shiftr a := nat_rect _ a (fun _ => div2).

Fixpoint bitwise (op:bool->bool->bool) n a b :=

match n with

| 0 => 0

| S n' =>

(if op (odd a) (odd b) then 1 else 0) +

2*(bitwise op n' (div2 a) (div2 b))

end.

Definition land a b := bitwise andb a a b.

Definition lor a b := bitwise orb (max a b) a b.

Definition ldiff a b := bitwise (fun b b' => andb b (negb b')) a a b.

Definition lxor a b := bitwise xorb (max a b) a b.