aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-08-11 13:33:26 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-08-11 13:33:26 +0000
commit5c825f263698433ed4e8db8ccd0c14394520535a (patch)
treea9855a96d5e780166652b93376fea2483f9863c4 /theories/Numbers
parentc02c86626e36c908ec76854f8eda2d5278141d12 (diff)
fast bitwise operations (lor,land,lxor) on int31 and BigN
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/Cyclic/Abstract/CyclicAxioms.v11
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v106
-rw-r--r--theories/Numbers/Cyclic/Int31/Cyclic31.v55
-rw-r--r--theories/Numbers/Cyclic/Int31/Int31.v11
-rw-r--r--theories/Numbers/Cyclic/ZModulo/ZModulo.v45
-rw-r--r--theories/Numbers/Natural/BigN/NMake.v96
6 files changed, 292 insertions, 32 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 9a8a7691c..39e086c31 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -88,7 +88,11 @@ Module ZnZ.
is_even : t -> bool;
(* square root *)
sqrt2 : t -> t -> t * carry t;
- sqrt : t -> t }.
+ sqrt : t -> t;
+ (* bitwise operations *)
+ lor : t -> t -> t;
+ land : t -> t -> t;
+ lxor : t -> t -> t }.
Section Specs.
Context {t : Type}{ops : Ops t}.
@@ -199,7 +203,10 @@ Module ZnZ.
[||WW x y||] = [|s|] ^ 2 + [+|r|] /\
[+|r|] <= 2 * [|s|];
spec_sqrt : forall x,
- [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2
+ [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2;
+ spec_lor : forall x y, [|lor x y|] = Z.lor [|x|] [|y|];
+ spec_land : forall x y, [|land x y|] = Z.land [|x|] [|y|];
+ spec_lxor : forall x y, [|lxor x y|] = Z.lxor [|x|] [|y|]
}.
End Specs.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 35fe948ea..94d3e97a5 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -283,6 +283,27 @@ Section Z_2nZ.
Eval lazy beta delta [ww_gcd] in
ww_gcd compare w_0 w_eq0 w_gcd_gt _ww_digits gcd_gt_fix gcd_cont.
+ Definition lor (x y : zn2z t) :=
+ match x, y with
+ | W0, _ => y
+ | _, W0 => x
+ | WW hx lx, WW hy ly => WW (ZnZ.lor hx hy) (ZnZ.lor lx ly)
+ end.
+
+ Definition land (x y : zn2z t) :=
+ match x, y with
+ | W0, _ => W0
+ | _, W0 => W0
+ | WW hx lx, WW hy ly => WW (ZnZ.land hx hy) (ZnZ.land lx ly)
+ end.
+
+ Definition lxor (x y : zn2z t) :=
+ match x, y with
+ | W0, _ => y
+ | _, W0 => x
+ | WW hx lx, WW hy ly => WW (ZnZ.lxor hx hy) (ZnZ.lxor lx ly)
+ end.
+
(* ** Record of operators on 2 words *)
Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) | 1 :=
@@ -303,7 +324,10 @@ Section Z_2nZ.
pos_mod
is_even
sqrt2
- sqrt.
+ sqrt
+ lor
+ land
+ lxor.
Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) | 2 :=
ZnZ.MkOps _ww_digits _ww_zdigits
@@ -323,7 +347,10 @@ Section Z_2nZ.
pos_mod
is_even
sqrt2
- sqrt.
+ sqrt
+ lor
+ land
+ lxor.
(* Proof *)
Context {specs : ZnZ.Specs ops}.
@@ -787,6 +814,81 @@ refine
exact ZnZ.spec_sqrt2.
Qed.
+ Let wB_pos : 0 < wB.
+ Proof.
+ unfold wB, base; apply Z.pow_pos_nonneg; auto with zarith.
+ Qed.
+
+ Let ww_testbit_high n x y : Z.pos w_digits <= n ->
+ Z.testbit [|WW x y|] n =
+ Z.testbit (ZnZ.to_Z x) (n - Z.pos w_digits).
+ Proof.
+ intros Hn.
+ assert (E : ZnZ.to_Z x = [|WW x y|] / wB).
+ { simpl.
+ rewrite Z.div_add_l; auto with zarith.
+ now rewrite Z.div_small, Z.add_0_r. }
+ rewrite E.
+ unfold wB, base. rewrite Z.div_pow2_bits.
+ - f_equal; auto with zarith.
+ - easy.
+ - auto with zarith.
+ Qed.
+
+ Let ww_testbit_low n x y : 0 <= n < Z.pos w_digits ->
+ Z.testbit [|WW x y|] n = Z.testbit (ZnZ.to_Z y) n.
+ Proof.
+ intros (Hn,Hn').
+ assert (E : ZnZ.to_Z y = [|WW x y|] mod wB).
+ { simpl; symmetry.
+ rewrite Z.add_comm, Z.mod_add; auto with zarith.
+ apply Z.mod_small; auto with zarith. }
+ rewrite E.
+ unfold wB, base. symmetry. apply Z.mod_pow2_bits_low; auto.
+ Qed.
+
+ Let spec_lor x y : [|lor x y|] = Z.lor [|x|] [|y|].
+ Proof.
+ destruct x as [ |hx lx]. trivial.
+ destruct y as [ |hy ly]. now rewrite Z.lor_comm.
+ change ([|WW (ZnZ.lor hx hy) (ZnZ.lor lx ly)|] =
+ Z.lor [|WW hx lx|] [|WW hy ly|]).
+ apply Z.bits_inj'; intros n Hn.
+ rewrite Z.lor_spec.
+ destruct (Z.le_gt_cases (Z.pos w_digits) n) as [LE|GT].
+ - now rewrite !ww_testbit_high, ZnZ.spec_lor, Z.lor_spec.
+ - rewrite !ww_testbit_low; auto.
+ now rewrite ZnZ.spec_lor, Z.lor_spec.
+ Qed.
+
+ Let spec_land x y : [|land x y|] = Z.land [|x|] [|y|].
+ Proof.
+ destruct x as [ |hx lx]. trivial.
+ destruct y as [ |hy ly]. now rewrite Z.land_comm.
+ change ([|WW (ZnZ.land hx hy) (ZnZ.land lx ly)|] =
+ Z.land [|WW hx lx|] [|WW hy ly|]).
+ apply Z.bits_inj'; intros n Hn.
+ rewrite Z.land_spec.
+ destruct (Z.le_gt_cases (Z.pos w_digits) n) as [LE|GT].
+ - now rewrite !ww_testbit_high, ZnZ.spec_land, Z.land_spec.
+ - rewrite !ww_testbit_low; auto.
+ now rewrite ZnZ.spec_land, Z.land_spec.
+ Qed.
+
+ Let spec_lxor x y : [|lxor x y|] = Z.lxor [|x|] [|y|].
+ Proof.
+ destruct x as [ |hx lx]. trivial.
+ destruct y as [ |hy ly]. now rewrite Z.lxor_comm.
+ change ([|WW (ZnZ.lxor hx hy) (ZnZ.lxor lx ly)|] =
+ Z.lxor [|WW hx lx|] [|WW hy ly|]).
+ apply Z.bits_inj'; intros n Hn.
+ rewrite Z.lxor_spec.
+ destruct (Z.le_gt_cases (Z.pos w_digits) n) as [LE|GT].
+ - now rewrite !ww_testbit_high, ZnZ.spec_lxor, Z.lxor_spec.
+ - rewrite !ww_testbit_low; auto.
+ now rewrite ZnZ.spec_lxor, Z.lxor_spec.
+ Qed.
+
Global Instance mk_zn2z_specs : ZnZ.Specs mk_zn2z_ops.
Proof.
apply ZnZ.MkSpecs; auto.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 385217d05..0284af7aa 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1158,7 +1158,10 @@ Instance int31_ops : ZnZ.Ops int31 :=
fun i => let (_,r) := i/2 in
match r ?= 0 with Eq => true | _ => false end;
sqrt2 := sqrt312;
- sqrt := sqrt31
+ sqrt := sqrt31;
+ lor := lor31;
+ land := land31;
+ lxor := lxor31
}.
Section Int31_Specs.
@@ -2403,6 +2406,51 @@ Qed.
apply Zmod_unique with [|q|]; auto with zarith.
Qed.
+ (* Bitwise *)
+
+ Lemma log2_phi_bounded x : Z.log2 [|x|] < Z.of_nat size.
+ Proof.
+ destruct (phi_bounded x) as (H,H').
+ Z.le_elim H.
+ - now apply Z.log2_lt_pow2.
+ - now rewrite <- H.
+ Qed.
+
+ Lemma spec_lor x y : [| ZnZ.lor x y |] = Z.lor [|x|] [|y|].
+ Proof.
+ unfold ZnZ.lor; simpl. unfold lor31.
+ rewrite phi_phi_inv.
+ apply Z.mod_small; split; trivial.
+ - apply Z.lor_nonneg; split; apply phi_bounded.
+ - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy.
+ rewrite Z.log2_lor; try apply phi_bounded.
+ apply Z.max_lub_lt; apply log2_phi_bounded.
+ Qed.
+
+ Lemma spec_land x y : [| ZnZ.land x y |] = Z.land [|x|] [|y|].
+ Proof.
+ unfold ZnZ.land; simpl. unfold land31.
+ rewrite phi_phi_inv.
+ apply Z.mod_small; split; trivial.
+ - apply Z.land_nonneg; left; apply phi_bounded.
+ - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy.
+ eapply Z.le_lt_trans.
+ apply Z.log2_land; try apply phi_bounded.
+ apply Z.min_lt_iff; left; apply log2_phi_bounded.
+ Qed.
+
+ Lemma spec_lxor x y : [| ZnZ.lxor x y |] = Z.lxor [|x|] [|y|].
+ Proof.
+ unfold ZnZ.lxor; simpl. unfold lxor31.
+ rewrite phi_phi_inv.
+ apply Z.mod_small; split; trivial.
+ - apply Z.lxor_nonneg; split; intros; apply phi_bounded.
+ - apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by easy.
+ eapply Z.le_lt_trans.
+ apply Z.log2_lxor; try apply phi_bounded.
+ apply Z.max_lub_lt; apply log2_phi_bounded.
+ Qed.
+
Global Instance int31_specs : ZnZ.Specs int31_ops := {
spec_to_Z := phi_bounded;
spec_of_pos := positive_to_int31_spec;
@@ -2446,7 +2494,10 @@ Qed.
spec_pos_mod := spec_pos_mod;
spec_is_even := spec_is_even;
spec_sqrt2 := spec_sqrt2;
- spec_sqrt := spec_sqrt }.
+ spec_sqrt := spec_sqrt;
+ spec_lor := spec_lor;
+ spec_land := spec_land;
+ spec_lxor := spec_lxor }.
End Int31_Specs.
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index f414663a8..885cd0daf 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -335,6 +335,11 @@ Definition addmuldiv31 p i j :=
in
res.
+(** Bitwise operations *)
+
+Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)).
+Definition land31 n m := phi_inv (Z.land (phi n) (phi m)).
+Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)).
Register add31 as int31 plus in "coq_int31" by True.
Register add31c as int31 plusc in "coq_int31" by True.
@@ -348,6 +353,12 @@ Register div3121 as int31 div21 in "coq_int31" by True.
Register div31 as int31 div in "coq_int31" by True.
Register compare31 as int31 compare in "coq_int31" by True.
Register addmuldiv31 as int31 addmuldiv in "coq_int31" by True.
+Register lor31 as int31 lor in "coq_int31" by True.
+Register land31 as int31 land in "coq_int31" by True.
+Register lxor31 as int31 lxor in "coq_int31" by True.
+
+Definition lnot31 n := lxor31 Tn n.
+Definition ldiff31 n m := land31 n (lnot31 m).
Fixpoint euler (guard:nat) (i j:int31) {struct guard} :=
match guard with
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 9e3f4ef44..334836954 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -796,6 +796,40 @@ Section ZModulo.
exists 0; simpl; auto with zarith.
Qed.
+ Definition lor := Z.lor.
+ Definition land := Z.land.
+ Definition lxor := Z.lxor.
+
+ Lemma spec_lor x y : [|lor x y|] = Z.lor [|x|] [|y|].
+ Proof.
+ unfold lor, to_Z.
+ apply Z.bits_inj'; intros n Hn. rewrite Z.lor_spec.
+ unfold wB, base.
+ destruct (Z.le_gt_cases (Z.pos digits) n).
+ - rewrite !Z.mod_pow2_bits_high; auto with zarith.
+ - rewrite !Z.mod_pow2_bits_low, Z.lor_spec; auto with zarith.
+ Qed.
+
+ Lemma spec_land x y : [|land x y|] = Z.land [|x|] [|y|].
+ Proof.
+ unfold land, to_Z.
+ apply Z.bits_inj'; intros n Hn. rewrite Z.land_spec.
+ unfold wB, base.
+ destruct (Z.le_gt_cases (Z.pos digits) n).
+ - rewrite !Z.mod_pow2_bits_high; auto with zarith.
+ - rewrite !Z.mod_pow2_bits_low, Z.land_spec; auto with zarith.
+ Qed.
+
+ Lemma spec_lxor x y : [|lxor x y|] = Z.lxor [|x|] [|y|].
+ Proof.
+ unfold lxor, to_Z.
+ apply Z.bits_inj'; intros n Hn. rewrite Z.lxor_spec.
+ unfold wB, base.
+ destruct (Z.le_gt_cases (Z.pos digits) n).
+ - rewrite !Z.mod_pow2_bits_high; auto with zarith.
+ - rewrite !Z.mod_pow2_bits_low, Z.lxor_spec; auto with zarith.
+ Qed.
+
(** Let's now group everything in two records *)
Instance zmod_ops : ZnZ.Ops Z := ZnZ.MkOps
@@ -849,7 +883,10 @@ Section ZModulo.
(is_even : t -> bool)
(sqrt2 : t -> t -> t * carry t)
- (sqrt : t -> t).
+ (sqrt : t -> t)
+ (lor : t -> t -> t)
+ (land : t -> t -> t)
+ (lxor : t -> t -> t).
Instance zmod_specs : ZnZ.Specs zmod_ops := ZnZ.MkSpecs
spec_to_Z
@@ -906,7 +943,10 @@ Section ZModulo.
spec_is_even
spec_sqrt2
- spec_sqrt.
+ spec_sqrt
+ spec_lor
+ spec_land
+ spec_lxor.
End ZModulo.
@@ -922,4 +962,3 @@ Module ZModuloCyclicType (P:PositiveNotOne) <: CyclicType.
Instance ops : ZnZ.Ops t := zmod_ops P.p.
Instance specs : ZnZ.Specs ops := zmod_specs P.not_one.
End ZModuloCyclicType.
-
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 5012a1b93..3cfa55bef 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -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.