diff options
Diffstat (limited to 'theories/Numbers/Integer/BigZ')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 13 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 40 |
2 files changed, 46 insertions, 7 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index b2bf8703ea..72137eccf7 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -19,17 +19,14 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake. - [ZMake.Make BigN] provides the operations and basic specs w.r.t. ZArith - [ZTypeIsZAxioms] shows (mainly) that these operations implement the interface [ZAxioms] - - [ZPropSig] adds all generic properties derived from [ZAxioms] - - [ZDivPropFunct] provides generic properties of [div] and [mod] - ("Floor" variant) + - [ZProp] adds all generic properties derived from [ZAxioms] - [MinMax*Properties] provides properties of [min] and [max] *) Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder := - ZMake.Make BigN <+ ZTypeIsZAxioms - <+ !ZProp <+ !ZDivProp <+ HasEqBool2Dec + ZMake.Make BigN <+ ZTypeIsZAxioms <+ !ZProp <+ HasEqBool2Dec <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. (** Notations about [BigZ] *) @@ -67,6 +64,8 @@ Arguments Scope BigZ.log2 [bigZ_scope]. Arguments Scope BigZ.sqrt [bigZ_scope]. Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope]. Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope]. +Arguments Scope BigZ.quot [bigZ_scope bigZ_scope]. +Arguments Scope BigZ.remainder [bigZ_scope bigZ_scope]. Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope]. Arguments Scope BigZ.even [bigZ_scope]. Arguments Scope BigZ.odd [bigZ_scope]. @@ -92,7 +91,9 @@ Notation "x < y <= z" := (x<y /\ y<=z)%bigZ : bigZ_scope. Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope. Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope. Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. -Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigN_scope. +Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope. +Infix "rem" := BigZ.remainder (at level 40, no associativity) : bigZ_scope. +Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope. Local Open Scope bigZ_scope. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index b341b32095..f4baf32bc4 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -Require Import ZArith. +Require Import ZArith Zquot. Require Import BigNumPrelude. Require Import NSig. Require Import ZSig. @@ -453,6 +453,44 @@ Module Make (N:NType) <: ZType. intros q r q11 r1 H; injection H; auto. Qed. + Definition quot x y := + match x, y with + | Pos nx, Pos ny => Pos (N.div nx ny) + | Pos nx, Neg ny => Neg (N.div nx ny) + | Neg nx, Pos ny => Neg (N.div nx ny) + | Neg nx, Neg ny => Pos (N.div nx ny) + end. + + Definition remainder x y := + if eq_bool y zero then x + else + match x, y with + | Pos nx, Pos ny => Pos (N.modulo nx ny) + | Pos nx, Neg ny => Pos (N.modulo nx ny) + | Neg nx, Pos ny => Neg (N.modulo nx ny) + | Neg nx, Neg ny => Neg (N.modulo nx ny) + end. + + Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y). + Proof. + intros [x|x] [y|y]; simpl; symmetry; + rewrite N.spec_div, ?Zquot_opp_r, ?Zquot_opp_l, ?Zopp_involutive; + rewrite Zquot_Zdiv_pos; trivial using N.spec_pos. + Qed. + + Lemma spec_remainder : forall x y, + to_Z (remainder x y) = (to_Z x) rem (to_Z y). + Proof. + intros x y. unfold remainder. rewrite spec_eq_bool, spec_0. + assert (Hy := Zeq_bool_if (to_Z y) 0). destruct Zeq_bool. + now rewrite Hy, Zrem_0_r. + destruct x as [x|x], y as [y|y]; simpl in *; symmetry; + rewrite N.spec_modulo, ?Zrem_opp_r, ?Zrem_opp_l, ?Zopp_involutive; + try rewrite Z.eq_opp_l, Z.opp_0 in Hy; + rewrite Zrem_Zmod_pos; generalize (N.spec_pos x) (N.spec_pos y); + z_order. + Qed. + Definition gcd x y := match x, y with | Pos nx, Pos ny => Pos (N.gcd nx ny) |