diff options
Diffstat (limited to 'theories/NArith/BinNat.v')
-rw-r--r-- | theories/NArith/BinNat.v | 359 |
1 files changed, 13 insertions, 346 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index b1d62d776..7d9f4d64f 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -9,6 +9,7 @@ Require Export BinNums. Require Import BinPos RelationClasses Morphisms Setoid Equalities GenericMinMax Wf_nat Bool NAxioms NProperties. +Require BinNatDef. (**********************************************************************) (** * Binary natural numbers, operations and properties *) @@ -17,7 +18,7 @@ Require Import BinPos RelationClasses Morphisms Setoid (** The type [N] and its constructors [N0] and [Npos] are now defined in [BinNums.v] *) -(** Every definitions and early properties about binary natural numbers +(** Every definitions and properties about binary natural numbers are placed in a module [N] for qualification purpose. *) Local Open Scope N_scope. @@ -31,98 +32,18 @@ Module N <: UsualDecidableTypeFull <: TotalOrder. -Definition t := N. -Definition eq := @Logic.eq t. -Definition eq_equiv := @eq_equivalence t. - -(** Operation [x -> 2*x+1] *) - -Definition succ_double x := - match x with - | 0 => Npos 1 - | Npos p => Npos p~1 - end. - -(** Operation [x -> 2*x] *) - -Definition double n := - match n with - | 0 => 0 - | Npos p => Npos p~0 - end. - -(** Successor *) - -Definition succ n := - match n with - | 0 => 1 - | Npos p => Npos (Pos.succ p) - end. - -(** Predecessor *) - -Definition pred n := - match n with - | 0 => 0 - | Npos p => Pos.pred_N p - end. - -(** The successor of a N can be seen as a positive *) - -Definition succ_pos (n : N) : positive := - match n with - | N0 => 1%positive - | Npos p => Pos.succ p - end. - -(** Addition *) - -Definition add n m := - match n, m with - | 0, _ => m - | _, 0 => n - | Npos p, Npos q => Npos (p + q) - end. - -Infix "+" := add : N_scope. +(** Definitions of operations, now in a separate file *) -(** Subtraction *) +Include BinNatDef.N. -Definition sub n m := -match n, m with -| 0, _ => 0 -| n, 0 => n -| Npos n', Npos m' => - match Pos.sub_mask n' m' with - | IsPos p => Npos p - | _ => 0 - end -end. - -Infix "-" := sub : N_scope. - -(** Multiplication *) - -Definition mul n m := - match n, m with - | 0, _ => 0 - | _, 0 => 0 - | Npos p, Npos q => Npos (p * q) - end. - -Infix "*" := mul : N_scope. - -(** Order *) +(* TODO : fix the location of iter_nat *) +Definition shiftl_nat (a:N)(n:nat) := iter_nat n _ double a. +Definition shiftr_nat (a:N)(n:nat) := iter_nat n _ div2 a. -Definition compare n m := - match n, m with - | 0, 0 => Eq - | 0, Npos m' => Lt - | Npos n', 0 => Gt - | Npos n', Npos m' => (n' ?= m')%positive - end. +(** Logical predicates *) -Infix "?=" := compare (at level 70, no associativity) : N_scope. +Definition eq := @Logic.eq t. +Definition eq_equiv := @eq_equivalence t. Definition lt x y := (x ?= y) = Lt. Definition gt x y := (x ?= y) = Gt. @@ -139,258 +60,11 @@ Notation "x <= y < z" := (x <= y /\ y < z) : N_scope. Notation "x < y < z" := (x < y /\ y < z) : N_scope. Notation "x < y <= z" := (x < y /\ y <= z) : N_scope. -(** Boolean equality and comparison *) - -(** Nota: this [eqb] is not convertible with the generated [N_beq], - since the underlying [Pos.eqb] differs from [positive_beq] - (cf BinIntDef). *) - -Fixpoint eqb n m := - match n, m with - | 0, 0 => true - | Npos p, Npos q => Pos.eqb p q - | _, _ => false - end. - -Definition leb x y := - match x ?= y with Gt => false | _ => true end. - -Definition ltb x y := - match x ?= y with Lt => true | _ => false end. - -Infix "=?" := eqb (at level 70, no associativity) : N_scope. -Infix "<=?" := leb (at level 70, no associativity) : N_scope. -Infix "<?" := ltb (at level 70, no associativity) : N_scope. - -(** Min and max *) - -Definition min n n' := match n ?= n' with - | Lt | Eq => n - | Gt => n' - end. - -Definition max n n' := match n ?= n' with - | Lt | Eq => n' - | Gt => n - end. - -(** Dividing by 2 *) - -Definition div2 n := - match n with - | 0 => 0 - | Npos 1 => 0 - | Npos (p~0) => Npos p - | Npos (p~1) => Npos p - end. - -(** Parity *) - -Definition even n := - match n with - | 0 => true - | Npos (xO _) => true - | _ => false - end. - -Definition odd n := negb (even n). - -(** Power *) - -Definition pow n p := - match p, n with - | 0, _ => Npos 1 - | _, 0 => 0 - | Npos p, Npos q => Npos (q^p) - end. - -Infix "^" := pow : N_scope. - -(** Base-2 logarithm *) - -Definition log2 n := - match n with - | 0 => 0 - | Npos 1 => 0 - | Npos (p~0) => Npos (Pos.size p) - | Npos (p~1) => Npos (Pos.size p) - end. - -(** How many digits in a number ? - Number 0 is said to have no digits at all. -*) - -Definition size n := - match n with - | 0 => 0 - | Npos p => Npos (Pos.size p) - end. - -Definition size_nat n := - match n with - | 0 => O - | Npos p => Pos.size_nat p - end. - -(** Euclidean division *) - -Fixpoint pos_div_eucl (a:positive)(b:N) : N * N := - match a with - | xH => - match b with 1 => (1,0) | _ => (0,1) end - | xO a' => - let (q, r) := pos_div_eucl a' b in - let r' := double r in - if b <=? r' then (succ_double q, r' - b) - else (double q, r') - | xI a' => - let (q, r) := pos_div_eucl a' b in - let r' := succ_double r in - if b <=? r' then (succ_double q, r' - b) - else (double q, r') - end. - -Definition div_eucl (a b:N) : N * N := - match a, b with - | 0, _ => (0, 0) - | _, 0 => (0, a) - | Npos na, _ => pos_div_eucl na b - end. - -Definition div a b := fst (div_eucl a b). -Definition modulo a b := snd (div_eucl a b). - -Infix "/" := div : N_scope. -Infix "mod" := modulo (at level 40, no associativity) : N_scope. - -(** Greatest common divisor *) - Definition divide p q := exists r, p*r = q. - Notation "( p | q )" := (divide p q) (at level 0) : N_scope. -Definition gcd a b := - match a, b with - | 0, _ => b - | _, 0 => a - | Npos p, Npos q => Npos (Pos.gcd p q) - end. - -(** Generalized Gcd, also computing rests of [a] and [b] after - division by gcd. *) - -Definition ggcd a b := - match a, b with - | 0, _ => (b,(0,1)) - | _, 0 => (a,(1,0)) - | Npos p, Npos q => - let '(g,(aa,bb)) := Pos.ggcd p q in - (Npos g, (Npos aa, Npos bb)) - end. - -(** Square root *) - -Definition sqrtrem n := - match n with - | 0 => (0, 0) - | Npos p => - match Pos.sqrtrem p with - | (s, IsPos r) => (Npos s, Npos r) - | (s, _) => (Npos s, 0) - end - end. - -Definition sqrt n := - match n with - | 0 => 0 - | Npos p => Npos (Pos.sqrt p) - end. - -(** Operation over bits of a [N] number. *) - -(** Logical [or] *) - -Definition lor n m := - match n, m with - | 0, _ => m - | _, 0 => n - | Npos p, Npos q => Npos (Pos.lor p q) - end. - -(** Logical [and] *) - -Definition land n m := - match n, m with - | 0, _ => 0 - | _, 0 => 0 - | Npos p, Npos q => Pos.land p q - end. - -(** Logical [diff] *) - -Fixpoint ldiff n m := - match n, m with - | 0, _ => 0 - | _, 0 => n - | Npos p, Npos q => Pos.ldiff p q - end. - -(** [xor] *) - -Definition lxor n m := - match n, m with - | 0, _ => m - | _, 0 => n - | Npos p, Npos q => Pos.lxor p q - end. - -(** Shifts *) - -Definition shiftl_nat (a:N)(n:nat) := iter_nat n _ double a. - -Definition shiftr_nat (a:N)(n:nat) := iter_nat n _ div2 a. - -Definition shiftl a n := - match a with - | 0 => 0 - | Npos a => Npos (Pos.shiftl a n) - end. - -Definition shiftr a n := - match n with - | 0 => a - | Npos p => Pos.iter p div2 a - end. - -(** Checking whether a particular bit is set or not *) - -Definition testbit_nat (a:N) := - match a with - | 0 => fun _ => false - | Npos p => Pos.testbit_nat p - end. - -(** Same, but with index in N *) - -Definition testbit a n := - match a with - | 0 => false - | Npos p => Pos.testbit p n - end. - -(** Translation from [N] to [nat] and back. *) - -Definition to_nat (a:N) := - match a with - | N0 => O - | Npos p => Pos.to_nat p - end. - -Definition of_nat (n:nat) := - match n with - | O => 0 - | S n' => Npos (Pos.of_succ_nat n') - end. +Definition Even n := exists m, n = 2*m. +Definition Odd n := exists m, n = 2*m+1. (** Decidability of equality. *) @@ -863,9 +537,6 @@ Qed. (** Specification of parity functions *) -Definition Even n := exists m, n = 2*m. -Definition Odd n := exists m, n = 2*m+1. - Lemma even_spec n : even n = true <-> Even n. Proof. destruct n. @@ -1220,11 +891,7 @@ Proof. apply pos_ldiff_spec. Qed. -(** Some constants *) - -Definition zero := 0. -Definition one := 1. -Definition two := 2. +(** Specification of constants *) Lemma one_succ : 1 = succ 0. Proof. reflexivity. Qed. |