aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Cyclic
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Cyclic')
-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
5 files changed, 219 insertions, 9 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.
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 09:45:57 +0000