diff options
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 3 | ||||
| -rw-r--r-- | kernel/byterun/coq_instruct.h | 1 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 22 | ||||
| -rw-r--r-- | kernel/cbytecodes.ml | 6 | ||||
| -rw-r--r-- | kernel/cbytecodes.mli | 7 | ||||
| -rw-r--r-- | kernel/cemitcodes.ml | 3 | ||||
| -rw-r--r-- | kernel/environ.ml | 3 | ||||
| -rw-r--r-- | kernel/retroknowledge.ml | 3 | ||||
| -rw-r--r-- | kernel/retroknowledge.mli | 3 | ||||
| -rw-r--r-- | tactics/extraargs.ml4 | 4 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 11 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 106 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 55 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 11 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 45 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 96 |
16 files changed, 342 insertions, 37 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 5d3026605..9a59a773f 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -46,7 +46,8 @@ void init_arity () { arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]= arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]= arity[HEAD0INT31]=arity[TAIL0INT31]= - arity[COMPINT31]=arity[DECOMPINT31]=0; + arity[COMPINT31]=arity[DECOMPINT31]= + arity[ORINT31]=arity[ANDINT31]=arity[XORINT31]=0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index e224a1080..d1136b2dc 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -49,6 +49,7 @@ enum instructions { HEAD0INT31, TAIL0INT31, ISCONST, ARECONST, COMPINT31, DECOMPINT31, + ORINT31, ANDINT31, XORINT31, /* /spiwack */ STOP }; diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index aab08d890..216919ae3 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1373,7 +1373,29 @@ value coq_interprete Next; } + Instruct (ORINT31) { + /* returns the bitwise or */ + print_instr("ORINT31"); + accu = + value_of_uint32((uint32_of_value(accu)) | (uint32_of_value(*sp++))); + Next; + } + Instruct (ANDINT31) { + /* returns the bitwise and */ + print_instr("ANDINT31"); + accu = + value_of_uint32((uint32_of_value(accu)) & (uint32_of_value(*sp++))); + Next; + } + + Instruct (XORINT31) { + /* returns the bitwise xor */ + print_instr("XORINT31"); + accu = + value_of_uint32((uint32_of_value(accu)) ^ (uint32_of_value(*sp++))); + Next; + } /* /spiwack */ diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index c0119aa26..994242a8a 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -114,6 +114,9 @@ type instruction = | Kareconst of int*Label.t (* conditional jump *) | Kcompint31 (* dynamic compilation of int31 *) | Kdecompint31 (* dynamic decompilation of int31 *) + | Klorint31 (* bitwise operations: or and xor *) + | Klandint31 + | Klxorint31 (* /spiwack *) and bytecodes = instruction list @@ -220,6 +223,9 @@ let rec instruction ppf = function | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl | Kcompint31 -> fprintf ppf "\tcompint31" | Kdecompint31 -> fprintf ppf "\tdecompint" + | Klorint31 -> fprintf ppf "\tlorint31" + | Klandint31 -> fprintf ppf "\tlandint31" + | Klxorint31 -> fprintf ppf "\tlxorint31" (* /spiwack *) diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index dc2220c14..0a631987e 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -107,9 +107,10 @@ type instruction = | Kisconst of Label.t (** conditional jump *) | Kareconst of int*Label.t (** conditional jump *) | Kcompint31 (** dynamic compilation of int31 *) - | Kdecompint31 (** dynamix decompilation of int31 - /spiwack *) - + | Kdecompint31 (** dynamix decompilation of int31 *) + | Klorint31 (** bitwise operations: or and xor *) + | Klandint31 + | Klxorint31 and bytecodes = instruction list diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 00f1f7fbd..680a5f9f2 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -258,6 +258,9 @@ let emit_instr = function | Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl | Kcompint31 -> out opCOMPINT31 | Kdecompint31 -> out opDECOMPINT31 + | Klorint31 -> out opORINT31 + | Klandint31 -> out opANDINT31 + | Klxorint31 -> out opXORINT31 (*/spiwack *) | Kstop -> out opSTOP diff --git a/kernel/environ.ml b/kernel/environ.ml index 50c7b11ae..2c723a834 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -521,6 +521,9 @@ fun env field value -> | KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31 | KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31 | KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31 + | KInt31 (_, Int31Lor) -> add_int31_binop_from_const Cbytecodes.Klorint31 + | KInt31 (_, Int31Land) -> add_int31_binop_from_const Cbytecodes.Klandint31 + | KInt31 (_, Int31Lxor) -> add_int31_binop_from_const Cbytecodes.Klxorint31 | _ -> env.retroknowledge in Retroknowledge.add_field retroknowledge_with_reactive_info field value diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 6f52edcd0..58bae94d6 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -65,6 +65,9 @@ type int31_field = | Int31Compare | Int31Head0 | Int31Tail0 + | Int31Lor + | Int31Land + | Int31Lxor type field = (* | KEq diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 88bdf706a..6b76e616a 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -52,6 +52,9 @@ type int31_field = | Int31Compare | Int31Head0 | Int31Tail0 + | Int31Lor + | Int31Land + | Int31Lxor type field = diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 6d3a95352..7a47c51ee 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -383,7 +383,9 @@ PRINTED BY pr_r_int31_field | [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ] | [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ] | [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ] - +| [ "int31" "lor" ] -> [ Retroknowledge.Int31Lor ] +| [ "int31" "land" ] -> [ Retroknowledge.Int31Land ] +| [ "int31" "lxor" ] -> [ Retroknowledge.Int31Lxor ] END ARGUMENT EXTEND retroknowledge_field 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. |