summaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/BigN
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Natural/BigN')
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v20
-rw-r--r--theories/Numbers/Natural/BigN/NMake.v150
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml24
-rw-r--r--theories/Numbers/Natural/BigN/Nbasic.v5
4 files changed, 124 insertions, 75 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 89b65617..f7f4347b 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -28,23 +28,13 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
Delimit Scope bigN_scope with bigN.
-Module BigN <: NType <: OrderedTypeFull <: TotalOrder.
- Include NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope].
- Bind Scope bigN_scope with t t'.
- Include NTypeIsNAxioms
- <+ NProp [no inline]
+Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
+ NMake.Make Int31Cyclic
+ <+ NTypeIsNAxioms
+ <+ NBasicProp [no inline] <+ NExtraProp [no inline]
<+ HasEqBool2Dec [no inline]
<+ MinMaxLogicalProperties [no inline]
<+ MinMaxDecProperties [no inline].
-End BigN.
-
-(** Nota concerning scopes : for the first Include, we cannot bind
- the scope bigN_scope to a type that doesn't exists yet.
- We hence need to explicitely declare the scope substitution.
- For the next Include, the abstract type t (in scope abstract_scope)
- gets substituted to concrete BigN.t (in scope bigN_scope),
- and the corresponding argument scope are fixed automatically.
-*)
(** Notations about [BigN] *)
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index d280a04b..bdcdd5ca 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -146,7 +146,7 @@ Module Make (W0:CyclicType) <: NType.
Theorem spec_add: forall x y, [add x y] = [x] + [y].
Proof.
intros x y. rewrite add_fold. apply spec_same_level; clear x y.
- intros n x y. simpl.
+ intros n x y. cbv beta iota zeta.
generalize (ZnZ.spec_add_c x y); case ZnZ.add_c; intros z H.
rewrite spec_mk_t. assumption.
rewrite spec_mk_t_S. unfold interp_carry in H.
@@ -242,8 +242,8 @@ Module Make (W0:CyclicType) <: NType.
Definition comparen_m n :
forall m, word (dom_t n) (S m) -> dom_t n -> comparison :=
let op := dom_op n in
- let zero := @ZnZ.zero _ op in
- let compare := @ZnZ.compare _ op in
+ let zero := ZnZ.zero (Ops:=op) in
+ let compare := ZnZ.compare (Ops:=op) in
let compare0 := compare zero in
fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m).
@@ -273,7 +273,7 @@ Module Make (W0:CyclicType) <: NType.
Local Notation compare_folded :=
(iter_sym _
- (fun n => @ZnZ.compare _ (dom_op n))
+ (fun n => ZnZ.compare (Ops:=dom_op n))
comparen_m
comparenm
CompOpp).
@@ -358,13 +358,13 @@ Module Make (W0:CyclicType) <: NType.
Definition wn_mul n : forall m, word (dom_t n) (S m) -> dom_t n -> t :=
let op := dom_op n in
- let zero := @ZnZ.zero _ op in
- let succ := @ZnZ.succ _ op in
- let add_c := @ZnZ.add_c _ op in
- let mul_c := @ZnZ.mul_c _ op in
+ let zero := ZnZ.zero in
+ let succ := ZnZ.succ (Ops:=op) in
+ let add_c := ZnZ.add_c (Ops:=op) in
+ let mul_c := ZnZ.mul_c (Ops:=op) in
let ww := @ZnZ.WW _ op in
let ow := @ZnZ.OW _ op in
- let eq0 := @ZnZ.eq0 _ op in
+ let eq0 := ZnZ.eq0 in
let mul_add := @DoubleMul.w_mul_add _ zero succ add_c mul_c in
let mul_add_n1 := @DoubleMul.double_mul_add_n1 _ zero ww ow mul_add in
fun m x y =>
@@ -464,18 +464,18 @@ Module Make (W0:CyclicType) <: NType.
Definition wn_divn1 n :=
let op := dom_op n in
let zd := ZnZ.zdigits op in
- let zero := @ZnZ.zero _ op in
- let ww := @ZnZ.WW _ op in
- let head0 := @ZnZ.head0 _ op in
- let add_mul_div := @ZnZ.add_mul_div _ op in
- let div21 := @ZnZ.div21 _ op in
- let compare := @ZnZ.compare _ op in
- let sub := @ZnZ.sub _ op in
+ let zero := ZnZ.zero in
+ let ww := ZnZ.WW in
+ let head0 := ZnZ.head0 in
+ let add_mul_div := ZnZ.add_mul_div in
+ let div21 := ZnZ.div21 in
+ let compare := ZnZ.compare in
+ let sub := ZnZ.sub in
let ddivn1 :=
DoubleDivn1.double_divn1 zd zero ww head0 add_mul_div div21 compare sub in
fun m x y => let (u,v) := ddivn1 (S m) x y in (mk_t_w' n m u, mk_t n v).
- Let div_gtnm n m wx wy :=
+ Definition div_gtnm n m wx wy :=
let mn := Max.max n m in
let d := diff n m in
let op := make_op mn in
@@ -522,7 +522,7 @@ Module Make (W0:CyclicType) <: NType.
case (ZnZ.spec_to_Z y); auto.
Qed.
- Let spec_divn1 n :=
+ Definition spec_divn1 n :=
DoubleDivn1.spec_double_divn1
(ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
ZnZ.WW ZnZ.head0
@@ -633,17 +633,17 @@ Module Make (W0:CyclicType) <: NType.
Definition wn_modn1 n :=
let op := dom_op n in
let zd := ZnZ.zdigits op in
- let zero := @ZnZ.zero _ op in
- let head0 := @ZnZ.head0 _ op in
- let add_mul_div := @ZnZ.add_mul_div _ op in
- let div21 := @ZnZ.div21 _ op in
- let compare := @ZnZ.compare _ op in
- let sub := @ZnZ.sub _ op in
+ let zero := ZnZ.zero in
+ let head0 := ZnZ.head0 in
+ let add_mul_div := ZnZ.add_mul_div in
+ let div21 := ZnZ.div21 in
+ let compare := ZnZ.compare in
+ let sub := ZnZ.sub in
let dmodn1 :=
DoubleDivn1.double_modn1 zd zero head0 add_mul_div div21 compare sub in
fun m x y => reduce n (dmodn1 (S m) x y).
- Let mod_gtnm n m wx wy :=
+ Definition mod_gtnm n m wx wy :=
let mn := Max.max n m in
let d := diff n m in
let op := make_op mn in
@@ -671,7 +671,7 @@ Module Make (W0:CyclicType) <: NType.
reflexivity.
Qed.
- Let spec_modn1 n :=
+ Definition spec_modn1 n :=
DoubleDivn1.spec_double_modn1
(ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
ZnZ.WW ZnZ.head0
@@ -1617,40 +1617,90 @@ Module Make (W0:CyclicType) <: NType.
rewrite spec_shiftr, spec_1. apply Z.div2_spec.
Qed.
- (** TODO : provide efficient versions instead of just converting
- from/to N (see with Laurent) *)
+ Local Notation lorn := (fun n =>
+ let op := dom_op n in
+ let lor := ZnZ.lor in
+ fun x y => reduce n (lor x y)).
+
+ Definition lor : t -> t -> t := Eval red_t in same_level lorn.
- Definition lor x y := of_N (N.lor (to_N x) (to_N y)).
- Definition land x y := of_N (N.land (to_N x) (to_N y)).
- Definition ldiff x y := of_N (N.ldiff (to_N x) (to_N y)).
- Definition lxor x y := of_N (N.lxor (to_N x) (to_N y)).
+ Lemma lor_fold : lor = same_level lorn.
+ Proof. red_t; reflexivity. Qed.
- Lemma spec_land: forall x y, [land x y] = Z.land [x] [y].
+ Theorem spec_lor x y : [lor x y] = Z.lor [x] [y].
Proof.
- intros x y. unfold land. rewrite spec_of_N. unfold to_N.
- generalize (spec_pos x), (spec_pos y).
- destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+ rewrite lor_fold. apply spec_same_level; clear x y.
+ intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_lor.
Qed.
- Lemma spec_lor: forall x y, [lor x y] = Z.lor [x] [y].
+ Local Notation landn := (fun n =>
+ let op := dom_op n in
+ let land := ZnZ.land in
+ fun x y => reduce n (land x y)).
+
+ Definition land : t -> t -> t := Eval red_t in same_level landn.
+
+ Lemma land_fold : land = same_level landn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_land x y : [land x y] = Z.land [x] [y].
Proof.
- intros x y. unfold lor. rewrite spec_of_N. unfold to_N.
- generalize (spec_pos x), (spec_pos y).
- destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+ rewrite land_fold. apply spec_same_level; clear x y.
+ intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_land.
Qed.
- Lemma spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y].
+ Local Notation lxorn := (fun n =>
+ let op := dom_op n in
+ let lxor := ZnZ.lxor in
+ fun x y => reduce n (lxor x y)).
+
+ Definition lxor : t -> t -> t := Eval red_t in same_level lxorn.
+
+ Lemma lxor_fold : lxor = same_level lxorn.
+ Proof. red_t; reflexivity. Qed.
+
+ Theorem spec_lxor x y : [lxor x y] = Z.lxor [x] [y].
Proof.
- intros x y. unfold ldiff. rewrite spec_of_N. unfold to_N.
- generalize (spec_pos x), (spec_pos y).
- destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+ rewrite lxor_fold. apply spec_same_level; clear x y.
+ intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_lxor.
Qed.
- Lemma spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y].
- Proof.
- intros x y. unfold lxor. rewrite spec_of_N. unfold to_N.
- generalize (spec_pos x), (spec_pos y).
- destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
+ Local Notation ldiffn := (fun n =>
+ let op := dom_op n in
+ let lxor := ZnZ.lxor in
+ let land := ZnZ.land in
+ let m1 := ZnZ.minus_one in
+ fun x y => reduce n (land x (lxor y m1))).
+
+ Definition ldiff : t -> t -> t := Eval red_t in same_level ldiffn.
+
+ Lemma ldiff_fold : ldiff = same_level ldiffn.
+ Proof. red_t; reflexivity. Qed.
+
+ Lemma ldiff_alt x y p :
+ 0 <= x < 2^p -> 0 <= y < 2^p ->
+ Z.ldiff x y = Z.land x (Z.lxor y (2^p - 1)).
+ Proof.
+ intros (Hx,Hx') (Hy,Hy').
+ destruct p as [|p|p].
+ - simpl in *; replace x with 0; replace y with 0; auto with zarith.
+ - rewrite <- Z.shiftl_1_l. change (_ - 1) with (Z.ones (Z.pos p)).
+ rewrite <- Z.ldiff_ones_l_low; trivial.
+ rewrite !Z.ldiff_land, Z.land_assoc. f_equal.
+ rewrite Z.land_ones; try easy.
+ symmetry. apply Z.mod_small; now split.
+ Z.le_elim Hy.
+ + now apply Z.log2_lt_pow2.
+ + now subst.
+ - simpl in *; omega.
+ Qed.
+
+ Theorem spec_ldiff x y : [ldiff x y] = Z.ldiff [x] [y].
+ Proof.
+ rewrite ldiff_fold. apply spec_same_level; clear x y.
+ intros n x y. simpl. rewrite spec_reduce.
+ rewrite ZnZ.spec_land, ZnZ.spec_lxor, ZnZ.spec_m1.
+ symmetry. apply ldiff_alt; apply ZnZ.spec_to_Z.
Qed.
End Make.
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 9e4e88c5..6de77e0a 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -138,8 +138,6 @@ pr
pr "";
pr " Definition t := t'.";
pr "";
- pr " Bind Scope abstract_scope with t t'.";
- pr "";
pr " (** * A generic toolbox for building and deconstructing [t] *)";
pr "";
@@ -234,7 +232,7 @@ pr
| S n1 => mk_zn2z_ops (nmake_op ww ww_op n1)
end.
- Let eval n m := ZnZ.to_Z (Ops:=nmake_op _ (dom_op n) m).
+ Definition eval n m := ZnZ.to_Z (Ops:=nmake_op _ (dom_op n) m).
Theorem nmake_op_S: forall ww (w_op: ZnZ.Ops ww) x,
nmake_op _ w_op (S x) = mk_zn2z_ops (nmake_op _ w_op x).
@@ -326,8 +324,13 @@ pr "
Lemma spec_zeron : forall n, ZnZ.to_Z (zeron n) = 0%%Z.
Proof.
- do_size (destruct n; [exact ZnZ.spec_0|]).
- destruct n; auto. simpl. rewrite make_op_S. exact ZnZ.spec_0.
+ do_size (destruct n;
+ [match goal with
+ |- @eq Z (_ (zeron ?n)) _ =>
+ apply (ZnZ.spec_0 (Specs:=dom_spec n))
+ end|]).
+ destruct n; auto. simpl. rewrite make_op_S. fold word.
+ apply (ZnZ.spec_0 (Specs:=wn_spec (SizePlus 0))).
Qed.
(** * Digits *)
@@ -533,7 +536,7 @@ pr "
for i = 0 to size-1 do
let pattern = (iter_str (size+1-i) "(S ") ^ "_" ^ (iter_str (size+1-i) ")") in
pr
-" Let mk_t_%iw m := Eval cbv beta zeta iota delta [ mk_t plus ] in
+" Definition mk_t_%iw m := Eval cbv beta zeta iota delta [ mk_t plus ] in
match m return word w%i (S m) -> t with
| %s as p => mk_t_w %i (S p)
| p => mk_t (%i+p)
@@ -542,7 +545,7 @@ pr
done;
pr
-" Let mk_t_w' n : forall m, word (dom_t n) (S m) -> t :=
+" Definition mk_t_w' n : forall m, word (dom_t n) (S m) -> t :=
match n return (forall m, word (dom_t n) (S m) -> t) with";
for i = 0 to size-1 do pr " | %i => mk_t_%iw" i i done;
pr
@@ -958,6 +961,11 @@ pr " end.";
pr "";
pr " Ltac unfold_red := unfold reduce, %s." (iter_name 1 size "reduce_" ",");
+pr "";
+for i = 0 to size do
+pr " Declare Equivalent Keys reduce reduce_%i." i;
+done;
+pr " Declare Equivalent Keys reduce_n reduce_%i." (size + 1);
pr "
Ltac solve_red :=
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index e545508d..8fe9ea92 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -320,6 +320,7 @@ Section CompareRec.
Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n :=
(spec_double_to_Z wm_base wm_to_Z wm_to_Z_pos).
+ Declare Equivalent Keys compare0_mn compare0_m.
Lemma spec_compare0_mn: forall n x,
compare0_mn n x = (0 ?= double_to_Z n x).
@@ -371,7 +372,7 @@ Section CompareRec.
intros n (H0, H); split; auto.
apply Z.lt_le_trans with (1:= H).
unfold double_wB, DoubleBase.double_wB; simpl.
- rewrite Pshiftl_nat_S, base_xO.
+ rewrite base_xO.
set (u := base (Pos.shiftl_nat wm_base n)).
assert (0 < u).
unfold u, base; auto with zarith.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 08:14:03 +0000