diff options
Diffstat (limited to 'theories/Numbers/Cyclic/ZModulo/ZModulo.v')
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 55 |
1 files changed, 47 insertions, 8 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 673e4b1c..b93b4eb3 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.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 *) @@ -38,10 +38,10 @@ Section ZModulo. Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). Notation "[+| c |]" := - (interp_carry 1 wB to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB to_Z c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB to_Z c) (at level 0, c at level 99). Notation "[|| x ||]" := (zn2z_to_Z wB to_Z x) (at level 0, x at level 99). @@ -466,8 +466,8 @@ Section ZModulo. generalize (Zgcd_is_gcd a b); inversion_clear 1. destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4. assert (H4:=Z.gcd_nonneg a b). - destruct (Z.eq_dec (Z.gcd a b) 0). - rewrite e; generalize (Zmax_spec a b); omega. + destruct (Z.eq_dec (Z.gcd a b) 0) as [->|Hneq]. + generalize (Zmax_spec a b); omega. assert (0 <= q). apply Z.mul_le_mono_pos_r with (Z.gcd a b); auto with zarith. destruct (Z.eq_dec q 0). @@ -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. - |