diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:26 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:26 +0000 |
commit | 07a5fbd1f2f8e84bc7409fe0e18e8803ae2bff68 (patch) | |
tree | 055e9c3db7716ce458ea47fd66d45979a442bc3e /theories/PArith/BinPos.v | |
parent | 157bee13827f9a616b6c82be4af110c8f2464c64 (diff) |
BinPosDef: a module with all code about positive, later Included in BinPos
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14101 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/PArith/BinPos.v')
-rw-r--r-- | theories/PArith/BinPos.v | 551 |
1 files changed, 8 insertions, 543 deletions
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 26754690a..67d193a6d 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -11,6 +11,8 @@ Require Export BinNums. Require Import Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders GenericMinMax Le Plus Wf_nat. +Require Export BinPosDef. + (**********************************************************************) (** * Binary positive numbers, operations and properties *) (**********************************************************************) @@ -20,17 +22,6 @@ Require Import Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid (** The type [positive] and its constructors [xI] and [xO] and [xH] are now defined in [BinNums.v] *) -(** Postfix notation for positive numbers, allowing to mimic - the position of bits in a big-endian representation. - For instance, we can write [1~1~0] instead of [(xO (xI xH))] - for the number 6 (which is 110 in binary notation). -*) - -Notation "p ~ 1" := (xI p) - (at level 7, left associativity, format "p '~' '1'") : positive_scope. -Notation "p ~ 0" := (xO p) - (at level 7, left associativity, format "p '~' '0'") : positive_scope. - Local Open Scope positive_scope. Local Unset Boolean Equality Schemes. Local Unset Case Analysis Schemes. @@ -43,543 +34,17 @@ Module Pos <: UsualDecidableTypeFull <: TotalOrder. -Definition t := positive. -Definition eq := @Logic.eq t. -Definition eq_equiv := @eq_equivalence t. -Include BackportEq. - -(** * Operations over positive numbers *) - -(** ** Successor *) - -Fixpoint succ x := - match x with - | p~1 => (succ p)~0 - | p~0 => p~1 - | 1 => 1~0 - end. - -(** ** Addition *) - -Fixpoint add x y := - match x, y with - | p~1, q~1 => (add_carry p q)~0 - | p~1, q~0 => (add p q)~1 - | p~1, 1 => (succ p)~0 - | p~0, q~1 => (add p q)~1 - | p~0, q~0 => (add p q)~0 - | p~0, 1 => p~1 - | 1, q~1 => (succ q)~0 - | 1, q~0 => q~1 - | 1, 1 => 1~0 - end - -with add_carry x y := - match x, y with - | p~1, q~1 => (add_carry p q)~1 - | p~1, q~0 => (add_carry p q)~0 - | p~1, 1 => (succ p)~1 - | p~0, q~1 => (add_carry p q)~0 - | p~0, q~0 => (add p q)~1 - | p~0, 1 => (succ p)~0 - | 1, q~1 => (succ q)~1 - | 1, q~0 => (succ q)~0 - | 1, 1 => 1~1 - end. - -Infix "+" := add : positive_scope. - -(** ** Operation [x -> 2*x-1] *) - -Fixpoint pred_double x := - match x with - | p~1 => p~0~1 - | p~0 => (pred_double p)~1 - | 1 => 1 - end. - -(** ** Predecessor *) - -Definition pred x := - match x with - | p~1 => p~0 - | p~0 => pred_double p - | 1 => 1 - end. - -(** ** The predecessor of a positive number can be seen as a [N] *) - -Definition pred_N x := - match x with - | p~1 => Npos (p~0) - | p~0 => Npos (pred_double p) - | 1 => N0 - end. - -(** ** An auxiliary type for subtraction *) - -Inductive mask : Set := -| IsNul : mask -| IsPos : positive -> mask -| IsNeg : mask. - -(** ** Operation [x -> 2*x+1] *) - -Definition succ_double_mask (x:mask) : mask := - match x with - | IsNul => IsPos 1 - | IsNeg => IsNeg - | IsPos p => IsPos p~1 - end. - -(** ** Operation [x -> 2*x] *) - -Definition double_mask (x:mask) : mask := - match x with - | IsNul => IsNul - | IsNeg => IsNeg - | IsPos p => IsPos p~0 - end. - -(** ** Operation [x -> 2*x-2] *) - -Definition double_pred_mask x : mask := - match x with - | p~1 => IsPos p~0~0 - | p~0 => IsPos (pred_double p)~0 - | 1 => IsNul - end. - -(** ** Predecessor with mask *) - -Definition pred_mask (p : mask) : mask := - match p with - | IsPos 1 => IsNul - | IsPos q => IsPos (pred q) - | IsNul => IsNeg - | IsNeg => IsNeg - end. - -(** ** Subtraction, result as a mask *) - -Fixpoint sub_mask (x y:positive) {struct y} : mask := - match x, y with - | p~1, q~1 => double_mask (sub_mask p q) - | p~1, q~0 => succ_double_mask (sub_mask p q) - | p~1, 1 => IsPos p~0 - | p~0, q~1 => succ_double_mask (sub_mask_carry p q) - | p~0, q~0 => double_mask (sub_mask p q) - | p~0, 1 => IsPos (pred_double p) - | 1, 1 => IsNul - | 1, _ => IsNeg - end - -with sub_mask_carry (x y:positive) {struct y} : mask := - match x, y with - | p~1, q~1 => succ_double_mask (sub_mask_carry p q) - | p~1, q~0 => double_mask (sub_mask p q) - | p~1, 1 => IsPos (pred_double p) - | p~0, q~1 => double_mask (sub_mask_carry p q) - | p~0, q~0 => succ_double_mask (sub_mask_carry p q) - | p~0, 1 => double_pred_mask p - | 1, _ => IsNeg - end. - -(** ** Subtraction, result as a positive, returning 1 if [x<=y] *) - -Definition sub x y := - match sub_mask x y with - | IsPos z => z - | _ => 1 - end. - -Infix "-" := sub : positive_scope. - -(** ** Multiplication *) - -Fixpoint mul x y := - match x with - | p~1 => y + (mul p y)~0 - | p~0 => (mul p y)~0 - | 1 => y - end. - -Infix "*" := mul : positive_scope. - -(** ** Iteration over a positive number *) - -Fixpoint iter (n:positive) {A} (f:A -> A) (x:A) : A := - match n with - | xH => f x - | xO n' => iter n' f (iter n' f x) - | xI n' => f (iter n' f (iter n' f x)) - end. - -(** ** Power *) - -Definition pow (x y:positive) := iter y (mul x) 1. - -Infix "^" := pow : positive_scope. - -(** ** Division by 2 rounded below but for 1 *) - -Definition div2 p := - match p with - | 1 => 1 - | p~0 => p - | p~1 => p - end. +(** * The definitions of operations are now in a separate file *) -(** Division by 2 rounded up *) - -Definition div2_up p := - match p with - | 1 => 1 - | p~0 => p - | p~1 => succ p - end. - -(** ** Number of digits in a positive number *) - -Fixpoint size_nat p : nat := - match p with - | 1 => S O - | p~1 => S (size_nat p) - | p~0 => S (size_nat p) - end. - -(** Same, with positive output *) - -Fixpoint size p := - match p with - | 1 => 1 - | p~1 => succ (size p) - | p~0 => succ (size p) - end. - -(** ** Comparison on binary positive numbers *) - -Fixpoint compare_cont (x y:positive) (r:comparison) {struct y} : comparison := - match x, y with - | p~1, q~1 => compare_cont p q r - | p~1, q~0 => compare_cont p q Gt - | p~1, 1 => Gt - | p~0, q~1 => compare_cont p q Lt - | p~0, q~0 => compare_cont p q r - | p~0, 1 => Gt - | 1, q~1 => Lt - | 1, q~0 => Lt - | 1, 1 => r - end. - -Definition compare x y := compare_cont x y Eq. - -Infix "?=" := compare (at level 70, no associativity) : positive_scope. - -Definition lt x y := (x ?= y) = Lt. -Definition gt x y := (x ?= y) = Gt. -Definition le x y := (x ?= y) <> Gt. -Definition ge x y := (x ?= y) <> Lt. - -Infix "<=" := le : positive_scope. -Infix "<" := lt : positive_scope. -Infix ">=" := ge : positive_scope. -Infix ">" := gt : positive_scope. - -Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope. -Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope. -Notation "x < y < z" := (x < y /\ y < z) : positive_scope. -Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope. - -Definition min p p' := - match p ?= p' with - | Lt | Eq => p - | Gt => p' - end. - -Definition max p p' := - match p ?= p' with - | Lt | Eq => p' - | Gt => p - end. - -(** ** Boolean equality and comparisons *) - -(** Nota: this [eqb] is not convertible with the generated [positive_beq], due - to a different guard argument. We keep this version for compatibility. *) - -Fixpoint eqb p q {struct q} := - match p, q with - | p~1, q~1 => eqb p q - | p~0, q~0 => eqb p q - | 1, 1 => true - | _, _ => 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) : positive_scope. -Infix "<=?" := leb (at level 70, no associativity) : positive_scope. -Infix "<?" := ltb (at level 70, no associativity) : positive_scope. - -(** ** A Square Root function for positive numbers *) - -(** We procede by blocks of two digits : if p is written qbb' - then sqrt(p) will be sqrt(q)~0 or sqrt(q)~1. - For deciding easily in which case we are, we store the remainder - (as a mask, since it can be null). - Instead of copy-pasting the following code four times, we - factorize as an auxiliary function, with f and g being either - xO or xI depending of the initial digits. - NB: (sub_mask (g (f 1)) 4) is a hack, morally it's g (f 0). -*) - -Definition sqrtrem_step (f g:positive->positive) p := - match p with - | (s, IsPos r) => - let s' := s~0~1 in - let r' := g (f r) in - if s' <=? r' then (s~1, sub_mask r' s') - else (s~0, IsPos r') - | (s,_) => (s~0, sub_mask (g (f 1)) 4) - end. - -Fixpoint sqrtrem p : positive * mask := - match p with - | 1 => (1,IsNul) - | 2 => (1,IsPos 1) - | 3 => (1,IsPos 2) - | p~0~0 => sqrtrem_step xO xO (sqrtrem p) - | p~0~1 => sqrtrem_step xO xI (sqrtrem p) - | p~1~0 => sqrtrem_step xI xO (sqrtrem p) - | p~1~1 => sqrtrem_step xI xI (sqrtrem p) - end. - -Definition sqrt p := fst (sqrtrem p). - - -(** ** Greatest Common Divisor *) - -Definition divide p q := exists r, p*r = q. -Notation "( p | q )" := (divide p q) (at level 0) : positive_scope. - -(** Instead of the Euclid algorithm, we use here the Stein binary - algorithm, which is faster for this representation. This algorithm - is almost structural, but in the last cases we do some recursive - calls on subtraction, hence the need for a counter. -*) - -Fixpoint gcdn (n : nat) (a b : positive) : positive := - match n with - | O => 1 - | S n => - match a,b with - | 1, _ => 1 - | _, 1 => 1 - | a~0, b~0 => (gcdn n a b)~0 - | _ , b~0 => gcdn n a b - | a~0, _ => gcdn n a b - | a'~1, b'~1 => - match a' ?= b' with - | Eq => a - | Lt => gcdn n (b'-a') a - | Gt => gcdn n (a'-b') b - end - end - end. - -(** We'll show later that we need at most (log2(a.b)) loops *) - -Definition gcd (a b : positive) := gcdn (size_nat a + size_nat b)%nat a b. - -(** Generalized Gcd, also computing the division of a and b by the gcd *) - -Fixpoint ggcdn (n : nat) (a b : positive) : (positive*(positive*positive)) := - match n with - | O => (1,(a,b)) - | S n => - match a,b with - | 1, _ => (1,(1,b)) - | _, 1 => (1,(a,1)) - | a~0, b~0 => - let (g,p) := ggcdn n a b in - (g~0,p) - | _, b~0 => - let '(g,(aa,bb)) := ggcdn n a b in - (g,(aa, bb~0)) - | a~0, _ => - let '(g,(aa,bb)) := ggcdn n a b in - (g,(aa~0, bb)) - | a'~1, b'~1 => - match a' ?= b' with - | Eq => (a,(1,1)) - | Lt => - let '(g,(ba,aa)) := ggcdn n (b'-a') a in - (g,(aa, aa + ba~0)) - | Gt => - let '(g,(ab,bb)) := ggcdn n (a'-b') b in - (g,(bb + ab~0, bb)) - end - end - end. - -Definition ggcd (a b: positive) := ggcdn (size_nat a + size_nat b)%nat a b. - -(** Local copies of the not-yet-available [N.double] and [N.succ_double] *) - -Definition Nsucc_double x := - match x with - | N0 => Npos 1 - | Npos p => Npos p~1 - end. - -Definition Ndouble n := - match n with - | N0 => N0 - | Npos p => Npos p~0 - end. - -(** Operation over bits. *) - -(** Logical [or] *) - -Fixpoint lor (p q : positive) : positive := - match p, q with - | 1, q~0 => q~1 - | 1, _ => q - | p~0, 1 => p~1 - | _, 1 => p - | p~0, q~0 => (lor p q)~0 - | p~0, q~1 => (lor p q)~1 - | p~1, q~0 => (lor p q)~1 - | p~1, q~1 => (lor p q)~1 - end. - -(** Logical [and] *) - -Fixpoint land (p q : positive) : N := - match p, q with - | 1, q~0 => N0 - | 1, _ => Npos 1 - | p~0, 1 => N0 - | _, 1 => Npos 1 - | p~0, q~0 => Ndouble (land p q) - | p~0, q~1 => Ndouble (land p q) - | p~1, q~0 => Ndouble (land p q) - | p~1, q~1 => Nsucc_double (land p q) - end. - -(** Logical [diff] *) - -Fixpoint ldiff (p q:positive) : N := - match p, q with - | 1, q~0 => Npos 1 - | 1, _ => N0 - | _~0, 1 => Npos p - | p~1, 1 => Npos (p~0) - | p~0, q~0 => Ndouble (ldiff p q) - | p~0, q~1 => Ndouble (ldiff p q) - | p~1, q~1 => Ndouble (ldiff p q) - | p~1, q~0 => Nsucc_double (ldiff p q) - end. - -(** [xor] *) - -Fixpoint lxor (p q:positive) : N := - match p, q with - | 1, 1 => N0 - | 1, q~0 => Npos (q~1) - | 1, q~1 => Npos (q~0) - | p~0, 1 => Npos (p~1) - | p~0, q~0 => Ndouble (lxor p q) - | p~0, q~1 => Nsucc_double (lxor p q) - | p~1, 1 => Npos (p~0) - | p~1, q~0 => Nsucc_double (lxor p q) - | p~1, q~1 => Ndouble (lxor p q) - end. - -(** Shifts. NB: right shift of 1 stays at 1. *) +Include BinPosDef.Pos. +(* TODO : fix the location of iter_nat *) Definition shiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p. - Definition shiftr_nat (p:positive)(n:nat) := iter_nat n _ div2 p. -Definition shiftl (p:positive)(n:N) := - match n with - | N0 => p - | Npos n => iter n xO p - end. - -Definition shiftr (p:positive)(n:N) := - match n with - | N0 => p - | Npos n => iter n div2 p - end. - -(** Checking whether a particular bit is set or not *) - -Fixpoint testbit_nat (p:positive) : nat -> bool := - match p with - | 1 => fun n => match n with - | O => true - | S _ => false - end - | p~0 => fun n => match n with - | O => false - | S n' => testbit_nat p n' - end - | p~1 => fun n => match n with - | O => true - | S n' => testbit_nat p n' - end - end. - -(** Same, but with index in N *) - -Fixpoint testbit (p:positive)(n:N) := - match p, n with - | p~0, N0 => false - | _, N0 => true - | 1, _ => false - | p~0, Npos n => testbit p (pred_N n) - | p~1, Npos n => testbit p (pred_N n) - end. - -(** ** From binary positive numbers to Peano natural numbers *) - -Definition iter_op {A}(op:A->A->A) := - fix iter (p:positive)(a:A) : A := - match p with - | 1 => a - | p~0 => iter p (op a a) - | p~1 => op a (iter p (op a a)) - end. - -Definition to_nat (x:positive) : nat := iter_op plus x (S O). - -(** ** From Peano natural numbers to binary positive numbers *) - -(** A version preserving positive numbers, and sending 0 to 1. *) - -Fixpoint of_nat (n:nat) : positive := - match n with - | O => 1 - | S O => 1 - | S x => succ (of_nat x) - end. - -(* Another version that converts [n] into [n+1] *) - -Fixpoint of_succ_nat (n:nat) : positive := - match n with - | O => 1 - | S x => succ (of_succ_nat x) - end. - +Definition eq := @Logic.eq t. +Definition eq_equiv := @eq_equivalence t. +Include BackportEq. (**********************************************************************) (** * Properties of operations over positive numbers *) |