From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- theories/Numbers/Natural/BigN/BigN.v | 20 +--- theories/Numbers/Natural/BigN/NMake.v | 150 +++++++++++++++++++---------- theories/Numbers/Natural/BigN/NMake_gen.ml | 24 +++-- theories/Numbers/Natural/BigN/Nbasic.v | 5 +- 4 files changed, 124 insertions(+), 75 deletions(-) (limited to 'theories/Numbers/Natural/BigN') 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 *) -(* 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 *) -(* 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 *) -(*