From 88cf0acb11ae2b4a7e0fb7df8289c15eb0748f19 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:28 +0000 Subject: BinNatDef containing all functions of BinNat, misc adaptations in BinPos git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14102 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/NArith/BinNat.v | 359 ++----------------------------------------- theories/NArith/BinNatDef.v | 361 ++++++++++++++++++++++++++++++++++++++++++++ theories/NArith/vo.itarget | 1 + 3 files changed, 375 insertions(+), 346 deletions(-) create mode 100644 theories/NArith/BinNatDef.v (limited to 'theories/NArith') 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 " 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. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v new file mode 100644 index 000000000..cb5cfe7f0 --- /dev/null +++ b/theories/NArith/BinNatDef.v @@ -0,0 +1,361 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 2*x+1] *) + +Definition succ_double x := + match x with + | 0 => 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. + +(** Subtraction *) + +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 *) + +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. + +Infix "?=" := compare (at level 70, no associativity) : 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 " 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 + | 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, _ => 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 + | 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 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 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 + | 0 => 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. + +End N. \ No newline at end of file diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget index 3e285772d..e76033f78 100644 --- a/theories/NArith/vo.itarget +++ b/theories/NArith/vo.itarget @@ -1,3 +1,4 @@ +BinNatDef.vo BinNat.vo NArith.vo Ndec.vo -- cgit v1.2.3