Library Coq.Init.Nat
Require Import Notations Logic Datatypes.
Require Decimal Hexadecimal Number.
Local Open Scope nat_scope.
Peano natural numbers, definitions of operations
Local Notation "0" := O.
Local Notation "1" := (S O).
Local Notation "2" := (S (S O)).
Definition zero := 0.
Definition one := 1.
Definition two := 2.
Definition succ := S.
Definition pred n :=
match n with
| 0 => n
| S u => u
end.
Register pred as num.nat.pred.
Fixpoint add n m :=
match n with
| 0 => m
| S p => S (p + m)
end
where "n + m" := (add n m) : nat_scope.
Register add as num.nat.add.
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.
Register mul as num.nat.mul.
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.
Register sub as num.nat.sub.
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.
tail_addmul r n m is r + n * m.
Fixpoint tail_addmul r n m :=
match n with
| O => r
| S n => tail_addmul (tail_add m r) n m
end.
Definition tail_mul n m := tail_addmul 0 n m.
Local Notation ten := (S (S (S (S (S (S (S (S (S (S O)))))))))).
Fixpoint of_uint_acc (d:Decimal.uint)(acc:nat) :=
match d with
| Decimal.Nil => acc
| Decimal.D0 d => of_uint_acc d (tail_mul ten acc)
| Decimal.D1 d => of_uint_acc d (S (tail_mul ten acc))
| Decimal.D2 d => of_uint_acc d (S (S (tail_mul ten acc)))
| Decimal.D3 d => of_uint_acc d (S (S (S (tail_mul ten acc))))
| Decimal.D4 d => of_uint_acc d (S (S (S (S (tail_mul ten acc)))))
| Decimal.D5 d => of_uint_acc d (S (S (S (S (S (tail_mul ten acc))))))
| Decimal.D6 d => of_uint_acc d (S (S (S (S (S (S (tail_mul ten acc)))))))
| Decimal.D7 d => of_uint_acc d (S (S (S (S (S (S (S (tail_mul ten acc))))))))
| Decimal.D8 d => of_uint_acc d (S (S (S (S (S (S (S (S (tail_mul ten acc)))))))))
| Decimal.D9 d => of_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul ten acc))))))))))
end.
Definition of_uint (d:Decimal.uint) := of_uint_acc d O.
Local Notation sixteen := (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))).
Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:nat) :=
match d with
| Hexadecimal.Nil => acc
| Hexadecimal.D0 d => of_hex_uint_acc d (tail_mul sixteen acc)
| Hexadecimal.D1 d => of_hex_uint_acc d (S (tail_mul sixteen acc))
| Hexadecimal.D2 d => of_hex_uint_acc d (S (S (tail_mul sixteen acc)))
| Hexadecimal.D3 d => of_hex_uint_acc d (S (S (S (tail_mul sixteen acc))))
| Hexadecimal.D4 d => of_hex_uint_acc d (S (S (S (S (tail_mul sixteen acc)))))
| Hexadecimal.D5 d => of_hex_uint_acc d (S (S (S (S (S (tail_mul sixteen acc))))))
| Hexadecimal.D6 d => of_hex_uint_acc d (S (S (S (S (S (S (tail_mul sixteen acc)))))))
| Hexadecimal.D7 d => of_hex_uint_acc d (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))
| Hexadecimal.D8 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))
| Hexadecimal.D9 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))
| Hexadecimal.Da d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))
| Hexadecimal.Db d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))
| Hexadecimal.Dc d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))
| Hexadecimal.Dd d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))
| Hexadecimal.De d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))))
| Hexadecimal.Df d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))))
end.
Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O.
Definition of_num_uint (d:Number.uint) :=
match d with
| Number.UIntDecimal d => of_uint d
| Number.UIntHexadecimal d => of_hex_uint d
end.
Fixpoint to_little_uint n acc :=
match n with
| O => acc
| S n => to_little_uint n (Decimal.Little.succ acc)
end.
Definition to_uint n :=
Decimal.rev (to_little_uint n Decimal.zero).
Fixpoint to_little_hex_uint n acc :=
match n with
| O => acc
| S n => to_little_hex_uint n (Hexadecimal.Little.succ acc)
end.
Definition to_hex_uint n :=
Hexadecimal.rev (to_little_hex_uint n Hexadecimal.zero).
Definition to_num_uint n := Number.UIntDecimal (to_uint n).
Definition to_num_hex_uint n := Number.UIntHexadecimal (to_hex_uint n).
Definition of_int (d:Decimal.int) : option nat :=
match Decimal.norm d with
| Decimal.Pos u => Some (of_uint u)
| _ => None
end.
Definition of_hex_int (d:Hexadecimal.int) : option nat :=
match Hexadecimal.norm d with
| Hexadecimal.Pos u => Some (of_hex_uint u)
| _ => None
end.
Definition of_num_int (d:Number.int) : option nat :=
match d with
| Number.IntDecimal d => of_int d
| Number.IntHexadecimal d => of_hex_int d
end.
Definition to_int n := Decimal.Pos (to_uint n).
Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n).
Definition to_num_int n := Number.IntDecimal (to_int n).
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 => x
| 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 fulfilling
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.