diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake.v')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 1706 |
1 files changed, 0 insertions, 1706 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v deleted file mode 100644 index 1425041a..00000000 --- a/theories/Numbers/Natural/BigN/NMake.v +++ /dev/null @@ -1,1706 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) -(************************************************************************) - -(** * NMake *) - -(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*) - -(** NB: This file contain the part which is independent from the underlying - representation. The representation-dependent (and macro-generated) part - is now in [NMake_gen]. *) - -Require Import Bool BigNumPrelude ZArith Nnat Ndigits CyclicAxioms DoubleType - Nbasic Wf_nat StreamMemo NSig NMake_gen. - -Module Make (W0:CyclicType) <: NType. - - (** Let's include the macro-generated part. Even if we can't functorize - things (due to Eval red_t below), the rest of the module only uses - elements mentionned in interface [NAbstract]. *) - - Include NMake_gen.Make W0. - - Open Scope Z_scope. - - Local Notation "[ x ]" := (to_Z x). - - Definition eq (x y : t) := [x] = [y]. - - Declare Reduction red_t := - lazy beta iota delta - [iter_t reduce same_level mk_t mk_t_S succ_t dom_t dom_op]. - - Ltac red_t := - match goal with |- ?u => let v := (eval red_t in u) in change v end. - - (** * Generic results *) - - Tactic Notation "destr_t" constr(x) "as" simple_intropattern(pat) := - destruct (destr_t x) as pat; cbv zeta; - rewrite ?iter_mk_t, ?spec_mk_t, ?spec_reduce. - - Lemma spec_same_level : forall A (P:Z->Z->A->Prop) - (f : forall n, dom_t n -> dom_t n -> A), - (forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)) -> - forall x y, P [x] [y] (same_level f x y). - Proof. - intros. apply spec_same_level_dep with (P:=fun _ => P); auto. - Qed. - - Theorem spec_pos: forall x, 0 <= [x]. - Proof. - intros x. destr_t x as (n,x). now case (ZnZ.spec_to_Z x). - Qed. - - Lemma digits_dom_op_incr : forall n m, (n<=m)%nat -> - (ZnZ.digits (dom_op n) <= ZnZ.digits (dom_op m))%positive. - Proof. - intros. - change (Zpos (ZnZ.digits (dom_op n)) <= Zpos (ZnZ.digits (dom_op m))). - rewrite !digits_dom_op, !Pshiftl_nat_Zpower. - apply Z.mul_le_mono_nonneg_l; auto with zarith. - apply Z.pow_le_mono_r; auto with zarith. - Qed. - - Definition to_N (x : t) := Z.to_N (to_Z x). - - (** * Zero, One *) - - Definition zero := mk_t O ZnZ.zero. - Definition one := mk_t O ZnZ.one. - - Theorem spec_0: [zero] = 0. - Proof. - unfold zero. rewrite spec_mk_t. exact ZnZ.spec_0. - Qed. - - Theorem spec_1: [one] = 1. - Proof. - unfold one. rewrite spec_mk_t. exact ZnZ.spec_1. - Qed. - - (** * Successor *) - - (** NB: it is crucial here and for the rest of this file to preserve - the let-in's. They allow to pre-compute once and for all the - field access to Z/nZ initial structures (when n=0..6). *) - - Local Notation succn := (fun n => - let op := dom_op n in - let succ_c := ZnZ.succ_c in - let one := ZnZ.one in - fun x => match succ_c x with - | C0 r => mk_t n r - | C1 r => mk_t_S n (WW one r) - end). - - Definition succ : t -> t := Eval red_t in iter_t succn. - - Lemma succ_fold : succ = iter_t succn. - Proof. red_t; reflexivity. Qed. - - Theorem spec_succ: forall n, [succ n] = [n] + 1. - Proof. - intros x. rewrite succ_fold. destr_t x as (n,x). - generalize (ZnZ.spec_succ_c x); case ZnZ.succ_c. - intros. rewrite spec_mk_t. assumption. - intros. unfold interp_carry in *. - rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_1. assumption. - Qed. - - (** Two *) - - (** Not really pretty, but since W0 might be Z/2Z, we're not sure - there's a proper 2 there. *) - - Definition two := succ one. - - Lemma spec_2 : [two] = 2. - Proof. - unfold two. now rewrite spec_succ, spec_1. - Qed. - - (** * Addition *) - - Local Notation addn := (fun n => - let op := dom_op n in - let add_c := ZnZ.add_c in - let one := ZnZ.one in - fun x y =>match add_c x y with - | C0 r => mk_t n r - | C1 r => mk_t_S n (WW one r) - end). - - Definition add : t -> t -> t := Eval red_t in same_level addn. - - Lemma add_fold : add = same_level addn. - Proof. red_t; reflexivity. Qed. - - Theorem spec_add: forall x y, [add x y] = [x] + [y]. - Proof. - intros x y. rewrite add_fold. apply spec_same_level; clear x y. - intros n x y. cbv beta iota zeta. - generalize (ZnZ.spec_add_c x y); case ZnZ.add_c; intros z H. - rewrite spec_mk_t. assumption. - rewrite spec_mk_t_S. unfold interp_carry in H. - simpl. rewrite ZnZ.spec_1. assumption. - Qed. - - (** * Predecessor *) - - Local Notation predn := (fun n => - let pred_c := ZnZ.pred_c in - fun x => match pred_c x with - | C0 r => reduce n r - | C1 _ => zero - end). - - Definition pred : t -> t := Eval red_t in iter_t predn. - - Lemma pred_fold : pred = iter_t predn. - Proof. red_t; reflexivity. Qed. - - Theorem spec_pred_pos : forall x, 0 < [x] -> [pred x] = [x] - 1. - Proof. - intros x. rewrite pred_fold. destr_t x as (n,x). intros H. - generalize (ZnZ.spec_pred_c x); case ZnZ.pred_c; intros y H'. - rewrite spec_reduce. assumption. - exfalso. unfold interp_carry in *. - generalize (ZnZ.spec_to_Z x) (ZnZ.spec_to_Z y); auto with zarith. - Qed. - - Theorem spec_pred0 : forall x, [x] = 0 -> [pred x] = 0. - Proof. - intros x. rewrite pred_fold. destr_t x as (n,x). intros H. - generalize (ZnZ.spec_pred_c x); case ZnZ.pred_c; intros y H'. - rewrite spec_reduce. - unfold interp_carry in H'. - generalize (ZnZ.spec_to_Z y); auto with zarith. - exact spec_0. - Qed. - - Lemma spec_pred x : [pred x] = Z.max 0 ([x]-1). - Proof. - rewrite Z.max_comm. - destruct (Z.max_spec ([x]-1) 0) as [(H,->)|(H,->)]. - - apply spec_pred0; generalize (spec_pos x); auto with zarith. - - apply spec_pred_pos; auto with zarith. - Qed. - - (** * Subtraction *) - - Local Notation subn := (fun n => - let sub_c := ZnZ.sub_c in - fun x y => match sub_c x y with - | C0 r => reduce n r - | C1 r => zero - end). - - Definition sub : t -> t -> t := Eval red_t in same_level subn. - - Lemma sub_fold : sub = same_level subn. - Proof. red_t; reflexivity. Qed. - - Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y]. - Proof. - intros x y. rewrite sub_fold. apply spec_same_level. clear x y. - intros n x y. simpl. - generalize (ZnZ.spec_sub_c x y); case ZnZ.sub_c; intros z H LE. - rewrite spec_reduce. assumption. - unfold interp_carry in H. - exfalso. - generalize (ZnZ.spec_to_Z z); auto with zarith. - Qed. - - Theorem spec_sub0 : forall x y, [x] < [y] -> [sub x y] = 0. - Proof. - intros x y. rewrite sub_fold. apply spec_same_level. clear x y. - intros n x y. simpl. - generalize (ZnZ.spec_sub_c x y); case ZnZ.sub_c; intros z H LE. - rewrite spec_reduce. - unfold interp_carry in H. - generalize (ZnZ.spec_to_Z z); auto with zarith. - exact spec_0. - Qed. - - Lemma spec_sub : forall x y, [sub x y] = Z.max 0 ([x]-[y]). - Proof. - intros. destruct (Z.le_gt_cases [y] [x]). - rewrite Z.max_r; auto with zarith. apply spec_sub_pos; auto. - rewrite Z.max_l; auto with zarith. apply spec_sub0; auto. - Qed. - - (** * Comparison *) - - Definition comparen_m n : - forall m, word (dom_t n) (S m) -> dom_t n -> comparison := - let op := dom_op n 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). - - Let spec_comparen_m: - forall n m (x : word (dom_t n) (S m)) (y : dom_t n), - comparen_m n m x y = Z.compare (eval n (S m) x) (ZnZ.to_Z y). - Proof. - intros n m x y. - unfold comparen_m, eval. - rewrite nmake_double. - apply spec_compare_mn_1. - exact ZnZ.spec_0. - intros. apply ZnZ.spec_compare. - exact ZnZ.spec_to_Z. - exact ZnZ.spec_compare. - exact ZnZ.spec_compare. - exact ZnZ.spec_to_Z. - Qed. - - Definition comparenm n m wx wy := - let mn := Max.max n m in - let d := diff n m in - let op := make_op mn in - ZnZ.compare - (castm (diff_r n m) (extend_tr wx (snd d))) - (castm (diff_l n m) (extend_tr wy (fst d))). - - Local Notation compare_folded := - (iter_sym _ - (fun n => ZnZ.compare (Ops:=dom_op n)) - comparen_m - comparenm - CompOpp). - - Definition compare : t -> t -> comparison := - Eval lazy beta iota delta [iter_sym dom_op dom_t comparen_m] in - compare_folded. - - Lemma compare_fold : compare = compare_folded. - Proof. - lazy beta iota delta [iter_sym dom_op dom_t comparen_m]. reflexivity. - Qed. - - Theorem spec_compare : forall x y, - compare x y = Z.compare [x] [y]. - Proof. - intros x y. rewrite compare_fold. apply spec_iter_sym; clear x y. - intros. apply ZnZ.spec_compare. - intros. cbv beta zeta. apply spec_comparen_m. - intros n m x y; unfold comparenm. - rewrite (spec_cast_l n m x), (spec_cast_r n m y). - unfold to_Z; apply ZnZ.spec_compare. - intros. subst. now rewrite <- Z.compare_antisym. - Qed. - - Definition eqb (x y : t) : bool := - match compare x y with - | Eq => true - | _ => false - end. - - Theorem spec_eqb x y : eqb x y = Z.eqb [x] [y]. - Proof. - apply eq_iff_eq_true. - unfold eqb. rewrite Z.eqb_eq, <- Z.compare_eq_iff, spec_compare. - split; [now destruct Z.compare | now intros ->]. - Qed. - - Definition lt (n m : t) := [n] < [m]. - Definition le (n m : t) := [n] <= [m]. - - Definition ltb (x y : t) : bool := - match compare x y with - | Lt => true - | _ => false - end. - - Theorem spec_ltb x y : ltb x y = Z.ltb [x] [y]. - Proof. - apply eq_iff_eq_true. - rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare. - split; [now destruct Z.compare | now intros ->]. - Qed. - - Definition leb (x y : t) : bool := - match compare x y with - | Gt => false - | _ => true - end. - - Theorem spec_leb x y : leb x y = Z.leb [x] [y]. - Proof. - apply eq_iff_eq_true. - rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - now destruct Z.compare; split. - Qed. - - Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end. - Definition max (n m : t) : t := match compare n m with Lt => m | _ => n end. - - Theorem spec_max : forall n m, [max n m] = Z.max [n] [m]. - Proof. - intros. unfold max, Z.max. rewrite spec_compare; destruct Z.compare; reflexivity. - Qed. - - Theorem spec_min : forall n m, [min n m] = Z.min [n] [m]. - Proof. - intros. unfold min, Z.min. rewrite spec_compare; destruct Z.compare; reflexivity. - Qed. - - (** * Multiplication *) - - 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 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 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 => - let (w,r) := mul_add_n1 (S m) x y zero in - if eq0 w then mk_t_w' n m r - else mk_t_w' n (S m) (WW (extend n m w) r). - - Definition mulnm n m x y := - let mn := Max.max n m in - let d := diff n m in - let op := make_op mn in - reduce_n (S mn) (ZnZ.mul_c - (castm (diff_r n m) (extend_tr x (snd d))) - (castm (diff_l n m) (extend_tr y (fst d)))). - - Local Notation mul_folded := - (iter_sym _ - (fun n => let mul_c := ZnZ.mul_c in - fun x y => reduce (S n) (succ_t _ (mul_c x y))) - wn_mul - mulnm - (fun x => x)). - - Definition mul : t -> t -> t := - Eval lazy beta iota delta - [iter_sym dom_op dom_t reduce succ_t extend zeron - wn_mul DoubleMul.w_mul_add mk_t_w'] in - mul_folded. - - Lemma mul_fold : mul = mul_folded. - Proof. - lazy beta iota delta - [iter_sym dom_op dom_t reduce succ_t extend zeron - wn_mul DoubleMul.w_mul_add mk_t_w']. reflexivity. - Qed. - - Lemma spec_muln: - forall n (x: word _ (S n)) y, - [Nn (S n) (ZnZ.mul_c (Ops:=make_op n) x y)] = [Nn n x] * [Nn n y]. - Proof. - intros n x y; unfold to_Z. - rewrite <- ZnZ.spec_mul_c. - rewrite make_op_S. - case ZnZ.mul_c; auto. - Qed. - - Lemma spec_mul_add_n1: forall n m x y z, - let (q,r) := DoubleMul.double_mul_add_n1 ZnZ.zero ZnZ.WW ZnZ.OW - (DoubleMul.w_mul_add ZnZ.zero ZnZ.succ ZnZ.add_c ZnZ.mul_c) - (S m) x y z in - ZnZ.to_Z q * (base (ZnZ.digits (nmake_op _ (dom_op n) (S m)))) - + eval n (S m) r = - eval n (S m) x * ZnZ.to_Z y + ZnZ.to_Z z. - Proof. - intros n m x y z. - rewrite digits_nmake. - unfold eval. rewrite nmake_double. - apply DoubleMul.spec_double_mul_add_n1. - apply ZnZ.spec_0. - exact ZnZ.spec_WW. - exact ZnZ.spec_OW. - apply DoubleCyclic.spec_mul_add. - Qed. - - Lemma spec_wn_mul : forall n m x y, - [wn_mul n m x y] = (eval n (S m) x) * ZnZ.to_Z y. - Proof. - intros; unfold wn_mul. - generalize (spec_mul_add_n1 n m x y ZnZ.zero). - case DoubleMul.double_mul_add_n1; intros q r Hqr. - rewrite ZnZ.spec_0, Z.add_0_r in Hqr. rewrite <- Hqr. - generalize (ZnZ.spec_eq0 q); case ZnZ.eq0; intros HH. - rewrite HH; auto. simpl. apply spec_mk_t_w'. - clear. - rewrite spec_mk_t_w'. - set (m' := S m) in *. - unfold eval. - rewrite nmake_WW. f_equal. f_equal. - rewrite <- spec_mk_t. - symmetry. apply spec_extend. - Qed. - - Theorem spec_mul : forall x y, [mul x y] = [x] * [y]. - Proof. - intros x y. rewrite mul_fold. apply spec_iter_sym; clear x y. - intros n x y. cbv zeta beta. - rewrite spec_reduce, spec_succ_t, <- ZnZ.spec_mul_c; auto. - apply spec_wn_mul. - intros n m x y; unfold mulnm. rewrite spec_reduce_n. - rewrite (spec_cast_l n m x), (spec_cast_r n m y). - apply spec_muln. - intros. rewrite Z.mul_comm; auto. - Qed. - - (** * Division by a smaller number *) - - Definition wn_divn1 n := - let op := dom_op n in - let zd := ZnZ.zdigits 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). - - 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 - let (q, r):= ZnZ.div_gt - (castm (diff_r n m) (extend_tr wx (snd d))) - (castm (diff_l n m) (extend_tr wy (fst d))) in - (reduce_n mn q, reduce_n mn r). - - Local Notation div_gt_folded := - (iter _ - (fun n => let div_gt := ZnZ.div_gt in - fun x y => let (u,v) := div_gt x y in (reduce n u, reduce n v)) - (fun n => - let div_gt := ZnZ.div_gt in - fun m x y => - let y' := DoubleBase.get_low (zeron n) (S m) y in - let (u,v) := div_gt x y' in (reduce n u, reduce n v)) - wn_divn1 - div_gtnm). - - Definition div_gt := - Eval lazy beta iota delta - [iter dom_op dom_t reduce zeron wn_divn1 mk_t_w' mk_t] in - div_gt_folded. - - Lemma div_gt_fold : div_gt = div_gt_folded. - Proof. - lazy beta iota delta [iter dom_op dom_t reduce zeron wn_divn1 mk_t_w' mk_t]. - reflexivity. - Qed. - - Lemma spec_get_endn: forall n m x y, - eval n m x <= [mk_t n y] -> - [mk_t n (DoubleBase.get_low (zeron n) m x)] = eval n m x. - Proof. - intros n m x y H. - unfold eval. rewrite nmake_double. - rewrite spec_mk_t in *. - apply DoubleBase.spec_get_low. - apply spec_zeron. - exact ZnZ.spec_to_Z. - apply Z.le_lt_trans with (ZnZ.to_Z y); auto. - rewrite <- nmake_double; auto. - case (ZnZ.spec_to_Z y); auto. - Qed. - - Definition spec_divn1 n := - DoubleDivn1.spec_double_divn1 - (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n) - ZnZ.WW ZnZ.head0 - ZnZ.add_mul_div ZnZ.div21 - ZnZ.compare ZnZ.sub ZnZ.to_Z - ZnZ.spec_to_Z - ZnZ.spec_zdigits - ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0 - ZnZ.spec_add_mul_div ZnZ.spec_div21 - ZnZ.spec_compare ZnZ.spec_sub. - - Lemma spec_div_gt_aux : forall x y, [x] > [y] -> 0 < [y] -> - let (q,r) := div_gt x y in - [x] = [q] * [y] + [r] /\ 0 <= [r] < [y]. - Proof. - intros x y. rewrite div_gt_fold. apply spec_iter; clear x y. - intros n x y H1 H2. simpl. - generalize (ZnZ.spec_div_gt x y H1 H2); case ZnZ.div_gt. - intros u v. rewrite 2 spec_reduce. auto. - intros n m x y H1 H2. cbv zeta beta. - generalize (ZnZ.spec_div_gt x - (DoubleBase.get_low (zeron n) (S m) y)). - case ZnZ.div_gt. - intros u v H3; repeat rewrite spec_reduce. - generalize (spec_get_endn n (S m) y x). rewrite !spec_mk_t. intros H4. - rewrite H4 in H3; auto with zarith. - intros n m x y H1 H2. - generalize (spec_divn1 n (S m) x y H2). - unfold wn_divn1; case DoubleDivn1.double_divn1. - intros u v H3. - rewrite spec_mk_t_w', spec_mk_t. - rewrite <- !nmake_double in H3; auto. - intros n m x y H1 H2; unfold div_gtnm. - generalize (ZnZ.spec_div_gt - (castm (diff_r n m) - (extend_tr x (snd (diff n m)))) - (castm (diff_l n m) - (extend_tr y (fst (diff n m))))). - case ZnZ.div_gt. - intros xx yy HH. - repeat rewrite spec_reduce_n. - rewrite (spec_cast_l n m x), (spec_cast_r n m y). - unfold to_Z; apply HH. - rewrite (spec_cast_l n m x) in H1; auto. - rewrite (spec_cast_r n m y) in H1; auto. - rewrite (spec_cast_r n m y) in H2; auto. - Qed. - - Theorem spec_div_gt: forall x y, [x] > [y] -> 0 < [y] -> - let (q,r) := div_gt x y in - [q] = [x] / [y] /\ [r] = [x] mod [y]. - Proof. - intros x y H1 H2; generalize (spec_div_gt_aux x y H1 H2); case div_gt. - intros q r (H3, H4); split. - apply (Zdiv_unique [x] [y] [q] [r]); auto. - rewrite Z.mul_comm; auto. - apply (Zmod_unique [x] [y] [q] [r]); auto. - rewrite Z.mul_comm; auto. - Qed. - - (** * General Division *) - - Definition div_eucl (x y : t) : t * t := - if eqb y zero then (zero,zero) else - match compare x y with - | Eq => (one, zero) - | Lt => (zero, x) - | Gt => div_gt x y - end. - - Theorem spec_div_eucl: forall x y, - let (q,r) := div_eucl x y in - ([q], [r]) = Z.div_eucl [x] [y]. - Proof. - intros x y. unfold div_eucl. - rewrite spec_eqb, spec_compare, spec_0. - case Z.eqb_spec. - intros ->. rewrite spec_0. destruct [x]; auto. - intros H'. - assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith). - clear H'. - case Z.compare_spec; intros Cmp; - rewrite ?spec_0, ?spec_1; intros; auto with zarith. - rewrite Cmp; generalize (Z_div_same [y] (Z.lt_gt _ _ H)) - (Z_mod_same [y] (Z.lt_gt _ _ H)); - unfold Z.div, Z.modulo; case Z.div_eucl; intros; subst; auto. - assert (LeLt: 0 <= [x] < [y]) by (generalize (spec_pos x); auto). - generalize (Zdiv_small _ _ LeLt) (Zmod_small _ _ LeLt); - unfold Z.div, Z.modulo; case Z.div_eucl; intros; subst; auto. - generalize (spec_div_gt _ _ (Z.lt_gt _ _ Cmp) H); auto. - unfold Z.div, Z.modulo; case Z.div_eucl; case div_gt. - intros a b c d (H1, H2); subst; auto. - Qed. - - Definition div (x y : t) : t := fst (div_eucl x y). - - Theorem spec_div: - forall x y, [div x y] = [x] / [y]. - Proof. - intros x y; unfold div; generalize (spec_div_eucl x y); - case div_eucl; simpl fst. - intros xx yy; unfold Z.div; case Z.div_eucl; intros qq rr H; - injection H; auto. - Qed. - - (** * Modulo by a smaller number *) - - Definition wn_modn1 n := - let op := dom_op n in - let zd := ZnZ.zdigits 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). - - 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 - reduce_n mn (ZnZ.modulo_gt - (castm (diff_r n m) (extend_tr wx (snd d))) - (castm (diff_l n m) (extend_tr wy (fst d)))). - - Local Notation mod_gt_folded := - (iter _ - (fun n => let modulo_gt := ZnZ.modulo_gt in - fun x y => reduce n (modulo_gt x y)) - (fun n => let modulo_gt := ZnZ.modulo_gt in - fun m x y => - reduce n (modulo_gt x (DoubleBase.get_low (zeron n) (S m) y))) - wn_modn1 - mod_gtnm). - - Definition mod_gt := - Eval lazy beta iota delta [iter dom_op dom_t reduce wn_modn1 zeron] in - mod_gt_folded. - - Lemma mod_gt_fold : mod_gt = mod_gt_folded. - Proof. - lazy beta iota delta [iter dom_op dom_t reduce wn_modn1 zeron]. - reflexivity. - Qed. - - Definition spec_modn1 n := - DoubleDivn1.spec_double_modn1 - (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n) - ZnZ.WW ZnZ.head0 - ZnZ.add_mul_div ZnZ.div21 - ZnZ.compare ZnZ.sub ZnZ.to_Z - ZnZ.spec_to_Z - ZnZ.spec_zdigits - ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0 - ZnZ.spec_add_mul_div ZnZ.spec_div21 - ZnZ.spec_compare ZnZ.spec_sub. - - Theorem spec_mod_gt: - forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y]. - Proof. - intros x y. rewrite mod_gt_fold. apply spec_iter; clear x y. - intros n x y H1 H2. simpl. rewrite spec_reduce. - exact (ZnZ.spec_modulo_gt x y H1 H2). - intros n m x y H1 H2. cbv zeta beta. rewrite spec_reduce. - rewrite <- spec_mk_t in H1. - rewrite <- (spec_get_endn n (S m) y x); auto with zarith. - rewrite spec_mk_t. - apply ZnZ.spec_modulo_gt; auto. - rewrite <- (spec_get_endn n (S m) y x), !spec_mk_t in H1; auto with zarith. - rewrite <- (spec_get_endn n (S m) y x), !spec_mk_t in H2; auto with zarith. - intros n m x y H1 H2. unfold wn_modn1. rewrite spec_reduce. - unfold eval; rewrite nmake_double. - apply (spec_modn1 n); auto. - intros n m x y H1 H2; unfold mod_gtnm. - repeat rewrite spec_reduce_n. - rewrite (spec_cast_l n m x), (spec_cast_r n m y). - unfold to_Z; apply ZnZ.spec_modulo_gt. - rewrite (spec_cast_l n m x) in H1; auto. - rewrite (spec_cast_r n m y) in H1; auto. - rewrite (spec_cast_r n m y) in H2; auto. - Qed. - - (** * General Modulo *) - - Definition modulo (x y : t) : t := - if eqb y zero then zero else - match compare x y with - | Eq => zero - | Lt => x - | Gt => mod_gt x y - end. - - Theorem spec_modulo: - forall x y, [modulo x y] = [x] mod [y]. - Proof. - intros x y. unfold modulo. - rewrite spec_eqb, spec_compare, spec_0. - case Z.eqb_spec. - intros ->; rewrite spec_0. destruct [x]; auto. - intro H'. - assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith). - clear H'. - case Z.compare_spec; - rewrite ?spec_0, ?spec_1; intros; try split; auto with zarith. - rewrite H0; symmetry; apply Z_mod_same; auto with zarith. - symmetry; apply Zmod_small; auto with zarith. - generalize (spec_pos x); auto with zarith. - apply spec_mod_gt; auto with zarith. - Qed. - - (** * Square *) - - Local Notation squaren := (fun n => - let square_c := ZnZ.square_c in - fun x => reduce (S n) (succ_t _ (square_c x))). - - Definition square : t -> t := Eval red_t in iter_t squaren. - - Lemma square_fold : square = iter_t squaren. - Proof. red_t; reflexivity. Qed. - - Theorem spec_square: forall x, [square x] = [x] * [x]. - Proof. - intros x. rewrite square_fold. destr_t x as (n,x). - rewrite spec_succ_t. exact (ZnZ.spec_square_c x). - Qed. - - (** * Square Root *) - - Local Notation sqrtn := (fun n => - let sqrt := ZnZ.sqrt in - fun x => reduce n (sqrt x)). - - Definition sqrt : t -> t := Eval red_t in iter_t sqrtn. - - Lemma sqrt_fold : sqrt = iter_t sqrtn. - Proof. red_t; reflexivity. Qed. - - Theorem spec_sqrt_aux: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. - Proof. - intros x. rewrite sqrt_fold. destr_t x as (n,x). exact (ZnZ.spec_sqrt x). - Qed. - - Theorem spec_sqrt: forall x, [sqrt x] = Z.sqrt [x]. - Proof. - intros x. - symmetry. apply Z.sqrt_unique. - rewrite <- ! Z.pow_2_r. apply spec_sqrt_aux. - Qed. - - (** * Power *) - - Fixpoint pow_pos (x:t)(p:positive) : t := - match p with - | xH => x - | xO p => square (pow_pos x p) - | xI p => mul (square (pow_pos x p)) x - end. - - Theorem spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n. - Proof. - intros x n; generalize x; elim n; clear n x; simpl pow_pos. - intros; rewrite spec_mul; rewrite spec_square; rewrite H. - rewrite Pos2Z.inj_xI; rewrite Zpower_exp; auto with zarith. - rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith. - rewrite Z.pow_2_r; rewrite Z.pow_1_r; auto. - intros; rewrite spec_square; rewrite H. - rewrite Pos2Z.inj_xO; auto with zarith. - rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith. - rewrite Z.pow_2_r; auto. - intros; rewrite Z.pow_1_r; auto. - Qed. - - Definition pow_N (x:t)(n:N) : t := match n with - | BinNat.N0 => one - | BinNat.Npos p => pow_pos x p - end. - - Theorem spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z.of_N n. - Proof. - destruct n; simpl. apply spec_1. - apply spec_pow_pos. - Qed. - - Definition pow (x y:t) : t := pow_N x (to_N y). - - Theorem spec_pow : forall x y, [pow x y] = [x] ^ [y]. - Proof. - intros. unfold pow, to_N. - now rewrite spec_pow_N, Z2N.id by apply spec_pos. - Qed. - - - (** * digits - - Number of digits in the representation of a numbers - (including head zero's). - NB: This function isn't a morphism for setoid [eq]. - *) - - Local Notation digitsn := (fun n => - let digits := ZnZ.digits (dom_op n) in - fun _ => digits). - - Definition digits : t -> positive := Eval red_t in iter_t digitsn. - - Lemma digits_fold : digits = iter_t digitsn. - Proof. red_t; reflexivity. Qed. - - Theorem spec_digits: forall x, 0 <= [x] < 2 ^ Zpos (digits x). - Proof. - intros x. rewrite digits_fold. destr_t x as (n,x). exact (ZnZ.spec_to_Z x). - Qed. - - Lemma digits_level : forall x, digits x = ZnZ.digits (dom_op (level x)). - Proof. - intros x. rewrite digits_fold. unfold level. destr_t x as (n,x). reflexivity. - Qed. - - (** * Gcd *) - - Definition gcd_gt_body a b cont := - match compare b zero with - | Gt => - let r := mod_gt a b in - match compare r zero with - | Gt => cont r (mod_gt b r) - | _ => b - end - | _ => a - end. - - Theorem Zspec_gcd_gt_body: forall a b cont p, - [a] > [b] -> [a] < 2 ^ p -> - (forall a1 b1, [a1] < 2 ^ (p - 1) -> [a1] > [b1] -> - Zis_gcd [a1] [b1] [cont a1 b1]) -> - Zis_gcd [a] [b] [gcd_gt_body a b cont]. - Proof. - intros a b cont p H2 H3 H4; unfold gcd_gt_body. - rewrite ! spec_compare, spec_0. case Z.compare_spec. - intros ->; apply Zis_gcd_0. - intros HH; absurd (0 <= [b]); auto with zarith. - case (spec_digits b); auto with zarith. - intros H5; case Z.compare_spec. - intros H6; rewrite <- (Z.mul_1_r [b]). - rewrite (Z_div_mod_eq [a] [b]); auto with zarith. - rewrite <- spec_mod_gt; auto with zarith. - rewrite H6; rewrite Z.add_0_r. - apply Zis_gcd_mult; apply Zis_gcd_1. - intros; apply False_ind. - case (spec_digits (mod_gt a b)); auto with zarith. - intros H6; apply DoubleDiv.Zis_gcd_mod; auto with zarith. - apply DoubleDiv.Zis_gcd_mod; auto with zarith. - rewrite <- spec_mod_gt; auto with zarith. - assert (F2: [b] > [mod_gt a b]). - case (Z_mod_lt [a] [b]); auto with zarith. - repeat rewrite <- spec_mod_gt; auto with zarith. - assert (F3: [mod_gt a b] > [mod_gt b (mod_gt a b)]). - case (Z_mod_lt [b] [mod_gt a b]); auto with zarith. - rewrite <- spec_mod_gt; auto with zarith. - repeat rewrite <- spec_mod_gt; auto with zarith. - apply H4; auto with zarith. - apply Z.mul_lt_mono_pos_r with 2; auto with zarith. - apply Z.le_lt_trans with ([b] + [mod_gt a b]); auto with zarith. - apply Z.le_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith. - - apply Z.add_le_mono_r. - rewrite <- (Z.mul_1_l [b]) at 1. - apply Z.mul_le_mono_nonneg_r; auto with zarith. - change 1 with (Z.succ 0). apply Z.le_succ_l. - apply Z.div_str_pos; auto with zarith. - - rewrite Z.mul_comm; rewrite spec_mod_gt; auto with zarith. - rewrite <- Z_div_mod_eq; auto with zarith. - rewrite Z.mul_comm, <- Z.pow_succ_r, Z.sub_1_r, Z.succ_pred; auto. - apply Z.le_0_sub. change 1 with (Z.succ 0). apply Z.le_succ_l. - destruct p; simpl in H3; auto with zarith. - Qed. - - Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) : t := - gcd_gt_body a b - (fun a b => - match p with - | xH => cont a b - | xO p => gcd_gt_aux p (gcd_gt_aux p cont) a b - | xI p => gcd_gt_aux p (gcd_gt_aux p cont) a b - end). - - Theorem Zspec_gcd_gt_aux: forall p n a b cont, - [a] > [b] -> [a] < 2 ^ (Zpos p + n) -> - (forall a1 b1, [a1] < 2 ^ n -> [a1] > [b1] -> - Zis_gcd [a1] [b1] [cont a1 b1]) -> - Zis_gcd [a] [b] [gcd_gt_aux p cont a b]. - intros p; elim p; clear p. - intros p Hrec n a b cont H2 H3 H4. - unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xI p) + n); auto. - intros a1 b1 H6 H7. - apply Hrec with (Zpos p + n); auto. - replace (Zpos p + (Zpos p + n)) with - (Zpos (xI p) + n - 1); auto. - rewrite Pos2Z.inj_xI; ring. - intros a2 b2 H9 H10. - apply Hrec with n; auto. - intros p Hrec n a b cont H2 H3 H4. - unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xO p) + n); auto. - intros a1 b1 H6 H7. - apply Hrec with (Zpos p + n - 1); auto. - replace (Zpos p + (Zpos p + n - 1)) with - (Zpos (xO p) + n - 1); auto. - rewrite Pos2Z.inj_xO; ring. - intros a2 b2 H9 H10. - apply Hrec with (n - 1); auto. - replace (Zpos p + (n - 1)) with - (Zpos p + n - 1); auto with zarith. - intros a3 b3 H12 H13; apply H4; auto with zarith. - apply Z.lt_le_trans with (1 := H12). - apply Z.pow_le_mono_r; auto with zarith. - intros n a b cont H H2 H3. - simpl gcd_gt_aux. - apply Zspec_gcd_gt_body with (n + 1); auto with zarith. - rewrite Z.add_comm; auto. - intros a1 b1 H5 H6; apply H3; auto. - replace n with (n + 1 - 1); auto; try ring. - Qed. - - Definition gcd_cont a b := - match compare one b with - | Eq => one - | _ => a - end. - - Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b. - - Theorem spec_gcd_gt: forall a b, - [a] > [b] -> [gcd_gt a b] = Z.gcd [a] [b]. - Proof. - intros a b H2. - case (spec_digits (gcd_gt a b)); intros H3 H4. - case (spec_digits a); intros H5 H6. - symmetry; apply Zis_gcd_gcd; auto with zarith. - unfold gcd_gt; apply Zspec_gcd_gt_aux with 0; auto with zarith. - intros a1 a2; rewrite Z.pow_0_r. - case (spec_digits a2); intros H7 H8; - intros; apply False_ind; auto with zarith. - Qed. - - Definition gcd (a b : t) : t := - match compare a b with - | Eq => a - | Lt => gcd_gt b a - | Gt => gcd_gt a b - end. - - Theorem spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b]. - Proof. - intros a b. - case (spec_digits a); intros H1 H2. - case (spec_digits b); intros H3 H4. - unfold gcd. rewrite spec_compare. case Z.compare_spec. - intros HH; rewrite HH; symmetry; apply Zis_gcd_gcd; auto. - apply Zis_gcd_refl. - intros; transitivity (Z.gcd [b] [a]). - apply spec_gcd_gt; auto with zarith. - apply Zis_gcd_gcd; auto with zarith. - apply Z.gcd_nonneg. - apply Zis_gcd_sym; apply Zgcd_is_gcd. - intros; apply spec_gcd_gt; auto with zarith. - Qed. - - (** * Parity test *) - - Definition even : t -> bool := Eval red_t in - iter_t (fun n x => ZnZ.is_even x). - - Definition odd x := negb (even x). - - Lemma even_fold : even = iter_t (fun n x => ZnZ.is_even x). - Proof. red_t; reflexivity. Qed. - - Theorem spec_even_aux: forall x, - if even x then [x] mod 2 = 0 else [x] mod 2 = 1. - Proof. - intros x. rewrite even_fold. destr_t x as (n,x). - exact (ZnZ.spec_is_even x). - Qed. - - Theorem spec_even: forall x, even x = Z.even [x]. - Proof. - intros x. assert (H := spec_even_aux x). symmetry. - rewrite (Z.div_mod [x] 2); auto with zarith. - destruct (even x); rewrite H, ?Z.add_0_r. - rewrite Zeven_bool_iff. apply Zeven_2p. - apply not_true_is_false. rewrite Zeven_bool_iff. - apply Zodd_not_Zeven. apply Zodd_2p_plus_1. - Qed. - - Theorem spec_odd: forall x, odd x = Z.odd [x]. - Proof. - intros x. unfold odd. - assert (H := spec_even_aux x). symmetry. - rewrite (Z.div_mod [x] 2); auto with zarith. - destruct (even x); rewrite H, ?Z.add_0_r; simpl negb. - apply not_true_is_false. rewrite Zodd_bool_iff. - apply Zeven_not_Zodd. apply Zeven_2p. - apply Zodd_bool_iff. apply Zodd_2p_plus_1. - Qed. - - (** * Conversion *) - - Definition pheight p := - Peano.pred (Pos.to_nat (get_height (ZnZ.digits (dom_op 0)) (plength p))). - - Theorem pheight_correct: forall p, - Zpos p < 2 ^ (Zpos (ZnZ.digits (dom_op 0)) * 2 ^ (Z.of_nat (pheight p))). - Proof. - intros p; unfold pheight. - rewrite Nat2Z.inj_pred by apply Pos2Nat.is_pos. - rewrite positive_nat_Z. - rewrite <- Z.sub_1_r. - assert (F2:= (get_height_correct (ZnZ.digits (dom_op 0)) (plength p))). - apply Z.lt_le_trans with (Zpos (Pos.succ p)). - rewrite Pos2Z.inj_succ; auto with zarith. - apply Z.le_trans with (1 := plength_pred_correct (Pos.succ p)). - rewrite Pos.pred_succ. - apply Z.pow_le_mono_r; auto with zarith. - Qed. - - Definition of_pos (x:positive) : t := - let n := pheight x in - reduce n (snd (ZnZ.of_pos x)). - - Theorem spec_of_pos: forall x, - [of_pos x] = Zpos x. - Proof. - intros x; unfold of_pos. - rewrite spec_reduce. - simpl. - apply ZnZ.of_pos_correct. - unfold base. - apply Z.lt_le_trans with (1 := pheight_correct x). - apply Z.pow_le_mono_r; auto with zarith. - rewrite (digits_dom_op (_ _)), Pshiftl_nat_Zpower. auto with zarith. - Qed. - - Definition of_N (x:N) : t := - match x with - | BinNat.N0 => zero - | Npos p => of_pos p - end. - - Theorem spec_of_N: forall x, - [of_N x] = Z.of_N x. - Proof. - intros x; case x. - simpl of_N. exact spec_0. - intros p; exact (spec_of_pos p). - Qed. - - (** * [head0] and [tail0] - - Number of zero at the beginning and at the end of - the representation of the number. - NB: these functions are not morphism for setoid [eq]. - *) - - Local Notation head0n := (fun n => - let head0 := ZnZ.head0 in - fun x => reduce n (head0 x)). - - Definition head0 : t -> t := Eval red_t in iter_t head0n. - - Lemma head0_fold : head0 = iter_t head0n. - Proof. red_t; reflexivity. Qed. - - Theorem spec_head00: forall x, [x] = 0 -> [head0 x] = Zpos (digits x). - Proof. - intros x. rewrite head0_fold, digits_fold. destr_t x as (n,x). - exact (ZnZ.spec_head00 x). - Qed. - - Lemma pow2_pos_minus_1 : forall z, 0<z -> 2^(z-1) = 2^z / 2. - Proof. - intros. apply Zdiv_unique with 0; auto with zarith. - change 2 with (2^1) at 2. - rewrite <- Zpower_exp; auto with zarith. - rewrite Z.add_0_r. f_equal. auto with zarith. - Qed. - - Theorem spec_head0: forall x, 0 < [x] -> - 2 ^ (Zpos (digits x) - 1) <= 2 ^ [head0 x] * [x] < 2 ^ Zpos (digits x). - Proof. - intros x. rewrite pow2_pos_minus_1 by (red; auto). - rewrite head0_fold, digits_fold. destr_t x as (n,x). exact (ZnZ.spec_head0 x). - Qed. - - Local Notation tail0n := (fun n => - let tail0 := ZnZ.tail0 in - fun x => reduce n (tail0 x)). - - Definition tail0 : t -> t := Eval red_t in iter_t tail0n. - - Lemma tail0_fold : tail0 = iter_t tail0n. - Proof. red_t; reflexivity. Qed. - - Theorem spec_tail00: forall x, [x] = 0 -> [tail0 x] = Zpos (digits x). - Proof. - intros x. rewrite tail0_fold, digits_fold. destr_t x as (n,x). - exact (ZnZ.spec_tail00 x). - Qed. - - Theorem spec_tail0: forall x, - 0 < [x] -> exists y, 0 <= y /\ [x] = (2 * y + 1) * 2 ^ [tail0 x]. - Proof. - intros x. rewrite tail0_fold. destr_t x as (n,x). exact (ZnZ.spec_tail0 x). - Qed. - - (** * [Ndigits] - - Same as [digits] but encoded using large integers - NB: this function is not a morphism for setoid [eq]. - *) - - Local Notation Ndigitsn := (fun n => - let d := reduce n (ZnZ.zdigits (dom_op n)) in - fun _ => d). - - Definition Ndigits : t -> t := Eval red_t in iter_t Ndigitsn. - - Lemma Ndigits_fold : Ndigits = iter_t Ndigitsn. - Proof. red_t; reflexivity. Qed. - - Theorem spec_Ndigits: forall x, [Ndigits x] = Zpos (digits x). - Proof. - intros x. rewrite Ndigits_fold, digits_fold. destr_t x as (n,x). - apply ZnZ.spec_zdigits. - Qed. - - (** * Binary logarithm *) - - Local Notation log2n := (fun n => - let op := dom_op n in - let zdigits := ZnZ.zdigits op in - let head0 := ZnZ.head0 in - let sub_carry := ZnZ.sub_carry in - fun x => reduce n (sub_carry zdigits (head0 x))). - - Definition log2 : t -> t := Eval red_t in - let log2 := iter_t log2n in - fun x => if eqb x zero then zero else log2 x. - - Lemma log2_fold : - log2 = fun x => if eqb x zero then zero else iter_t log2n x. - Proof. red_t; reflexivity. Qed. - - Lemma spec_log2_0 : forall x, [x] = 0 -> [log2 x] = 0. - Proof. - intros x H. rewrite log2_fold. - rewrite spec_eqb, H. rewrite spec_0. simpl. exact spec_0. - Qed. - - Lemma head0_zdigits : forall n (x : dom_t n), - 0 < ZnZ.to_Z x -> - ZnZ.to_Z (ZnZ.head0 x) < ZnZ.to_Z (ZnZ.zdigits (dom_op n)). - Proof. - intros n x H. - destruct (ZnZ.spec_head0 x H) as (_,H0). - intros. - assert (H1 := ZnZ.spec_to_Z (ZnZ.head0 x)). - assert (H2 := ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))). - unfold base in *. - rewrite ZnZ.spec_zdigits in H2 |- *. - set (h := ZnZ.to_Z (ZnZ.head0 x)) in *; clearbody h. - set (d := ZnZ.digits (dom_op n)) in *; clearbody d. - destruct (Z_lt_le_dec h (Zpos d)); auto. exfalso. - assert (1 * 2^Zpos d <= ZnZ.to_Z x * 2^h). - apply Z.mul_le_mono_nonneg; auto with zarith. - apply Z.pow_le_mono_r; auto with zarith. - rewrite Z.mul_comm in H0. auto with zarith. - Qed. - - Lemma spec_log2_pos : forall x, [x]<>0 -> - 2^[log2 x] <= [x] < 2^([log2 x]+1). - Proof. - intros x H. rewrite log2_fold. - rewrite spec_eqb. rewrite spec_0. - case Z.eqb_spec. - auto with zarith. - clear H. - destr_t x as (n,x). intros H. - rewrite ZnZ.spec_sub_carry. - assert (H0 := ZnZ.spec_to_Z x). - assert (H1 := ZnZ.spec_to_Z (ZnZ.head0 x)). - assert (H2 := ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))). - assert (H3 := head0_zdigits n x). - rewrite Zmod_small by auto with zarith. - rewrite Z.sub_simpl_r. - rewrite (Z.mul_lt_mono_pos_l (2^(ZnZ.to_Z (ZnZ.head0 x)))); - auto with zarith. - rewrite (Z.mul_le_mono_pos_l _ _ (2^(ZnZ.to_Z (ZnZ.head0 x)))); - auto with zarith. - rewrite <- 2 Zpower_exp; auto with zarith. - rewrite !Z.add_sub_assoc, !Z.add_simpl_l. - rewrite ZnZ.spec_zdigits. - rewrite pow2_pos_minus_1 by (red; auto). - apply ZnZ.spec_head0; auto with zarith. - Qed. - - Lemma spec_log2 : forall x, [log2 x] = Z.log2 [x]. - Proof. - intros. destruct (Z_lt_ge_dec 0 [x]). - symmetry. apply Z.log2_unique. apply spec_pos. - apply spec_log2_pos. intro EQ; rewrite EQ in *; auto with zarith. - rewrite spec_log2_0. rewrite Z.log2_nonpos; auto with zarith. - generalize (spec_pos x); auto with zarith. - Qed. - - Lemma log2_digits_head0 : forall x, 0 < [x] -> - [log2 x] = Zpos (digits x) - [head0 x] - 1. - Proof. - intros. rewrite log2_fold. - rewrite spec_eqb. rewrite spec_0. - case Z.eqb_spec. - auto with zarith. - intros _. revert H. rewrite digits_fold, head0_fold. destr_t x as (n,x). - rewrite ZnZ.spec_sub_carry. - intros. - generalize (head0_zdigits n x H). - generalize (ZnZ.spec_to_Z (ZnZ.head0 x)). - generalize (ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))). - rewrite ZnZ.spec_zdigits. intros. apply Zmod_small. - auto with zarith. - Qed. - - (** * Right shift *) - - Local Notation shiftrn := (fun n => - let op := dom_op n in - let zdigits := ZnZ.zdigits op in - let sub_c := ZnZ.sub_c in - let add_mul_div := ZnZ.add_mul_div in - let zzero := ZnZ.zero in - fun x p => match sub_c zdigits p with - | C0 d => reduce n (add_mul_div d zzero x) - | C1 _ => zero - end). - - Definition shiftr : t -> t -> t := Eval red_t in - same_level shiftrn. - - Lemma shiftr_fold : shiftr = same_level shiftrn. - Proof. red_t; reflexivity. Qed. - - Lemma div_pow2_bound :forall x y z, - 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z. - Proof. - intros x y z HH HH1 HH2. - split; auto with zarith. - apply Z.le_lt_trans with (2 := HH2); auto with zarith. - apply Zdiv_le_upper_bound; auto with zarith. - pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith. - apply Z.mul_le_mono_nonneg_l; auto. - apply Z.pow_le_mono_r; auto with zarith. - rewrite Z.pow_0_r; ring. - Qed. - - Theorem spec_shiftr_pow2 : forall x n, - [shiftr x n] = [x] / 2 ^ [n]. - Proof. - intros x y. rewrite shiftr_fold. apply spec_same_level. clear x y. - intros n x p. simpl. - assert (Hx := ZnZ.spec_to_Z x). - assert (Hy := ZnZ.spec_to_Z p). - generalize (ZnZ.spec_sub_c (ZnZ.zdigits (dom_op n)) p). - case ZnZ.sub_c; intros d H; unfold interp_carry in *; simpl. - (** Subtraction without underflow : [ p <= digits ] *) - rewrite spec_reduce. - rewrite ZnZ.spec_zdigits in H. - rewrite ZnZ.spec_add_mul_div by auto with zarith. - rewrite ZnZ.spec_0, Z.mul_0_l, Z.add_0_l. - rewrite Zmod_small. - f_equal. f_equal. auto with zarith. - split. auto with zarith. - apply div_pow2_bound; auto with zarith. - (** Subtraction with underflow : [ digits < p ] *) - rewrite ZnZ.spec_0. symmetry. - apply Zdiv_small. - split; auto with zarith. - apply Z.lt_le_trans with (base (ZnZ.digits (dom_op n))); auto with zarith. - unfold base. apply Z.pow_le_mono_r; auto with zarith. - rewrite ZnZ.spec_zdigits in H. - generalize (ZnZ.spec_to_Z d); auto with zarith. - Qed. - - Lemma spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p]. - Proof. - intros. - now rewrite spec_shiftr_pow2, Z.shiftr_div_pow2 by apply spec_pos. - Qed. - - (** * Left shift *) - - (** First an unsafe version, working correctly only if - the representation is large enough *) - - Local Notation unsafe_shiftln := (fun n => - let op := dom_op n in - let add_mul_div := ZnZ.add_mul_div in - let zero := ZnZ.zero in - fun x p => reduce n (add_mul_div p x zero)). - - Definition unsafe_shiftl : t -> t -> t := Eval red_t in - same_level unsafe_shiftln. - - Lemma unsafe_shiftl_fold : unsafe_shiftl = same_level unsafe_shiftln. - Proof. red_t; reflexivity. Qed. - - Theorem spec_unsafe_shiftl_aux : forall x p K, - 0 <= K -> - [x] < 2^K -> - [p] + K <= Zpos (digits x) -> - [unsafe_shiftl x p] = [x] * 2 ^ [p]. - Proof. - intros x p. - rewrite unsafe_shiftl_fold. rewrite digits_level. - apply spec_same_level_dep. - intros n m z z' r LE H K HK H1 H2. apply (H K); auto. - transitivity (Zpos (ZnZ.digits (dom_op n))); auto. - apply digits_dom_op_incr; auto. - clear x p. - intros n x p K HK Hx Hp. simpl. rewrite spec_reduce. - destruct (ZnZ.spec_to_Z x). - destruct (ZnZ.spec_to_Z p). - rewrite ZnZ.spec_add_mul_div by (omega with *). - rewrite ZnZ.spec_0, Zdiv_0_l, Z.add_0_r. - apply Zmod_small. unfold base. - split; auto with zarith. - rewrite Z.mul_comm. - apply Z.lt_le_trans with (2^(ZnZ.to_Z p + K)). - rewrite Zpower_exp; auto with zarith. - apply Z.mul_lt_mono_pos_l; auto with zarith. - apply Z.pow_le_mono_r; auto with zarith. - Qed. - - Theorem spec_unsafe_shiftl: forall x p, - [p] <= [head0 x] -> [unsafe_shiftl x p] = [x] * 2 ^ [p]. - Proof. - intros. - destruct (Z.eq_dec [x] 0) as [EQ|NEQ]. - (* [x] = 0 *) - apply spec_unsafe_shiftl_aux with 0; auto with zarith. - now rewrite EQ. - rewrite spec_head00 in *; auto with zarith. - (* [x] <> 0 *) - apply spec_unsafe_shiftl_aux with ([log2 x] + 1); auto with zarith. - generalize (spec_pos (log2 x)); auto with zarith. - destruct (spec_log2_pos x); auto with zarith. - rewrite log2_digits_head0; auto with zarith. - generalize (spec_pos x); auto with zarith. - Qed. - - (** Then we define a function doubling the size of the representation - but without changing the value of the number. *) - - Local Notation double_size_n := (fun n => - let zero := ZnZ.zero in - fun x => mk_t_S n (WW zero x)). - - Definition double_size : t -> t := Eval red_t in - iter_t double_size_n. - - Lemma double_size_fold : double_size = iter_t double_size_n. - Proof. red_t; reflexivity. Qed. - - Lemma double_size_level : forall x, level (double_size x) = S (level x). - Proof. - intros x. rewrite double_size_fold; unfold level at 2. destr_t x as (n,x). - apply mk_t_S_level. - Qed. - - Theorem spec_double_size_digits: - forall x, Zpos (digits (double_size x)) = 2 * (Zpos (digits x)). - Proof. - intros x. rewrite ! digits_level, double_size_level. - rewrite 2 digits_dom_op, 2 Pshiftl_nat_Zpower, - Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith. - ring. - Qed. - - Theorem spec_double_size: forall x, [double_size x] = [x]. - Proof. - intros x. rewrite double_size_fold. destr_t x as (n,x). - rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_0. auto with zarith. - Qed. - - Theorem spec_double_size_head0: - forall x, 2 * [head0 x] <= [head0 (double_size x)]. - Proof. - intros x. - assert (F1:= spec_pos (head0 x)). - assert (F2: 0 < Zpos (digits x)). - red; auto. - assert (HH := spec_pos x). Z.le_elim HH. - generalize HH; rewrite <- (spec_double_size x); intros HH1. - case (spec_head0 x HH); intros _ HH2. - case (spec_head0 _ HH1). - rewrite (spec_double_size x); rewrite (spec_double_size_digits x). - intros HH3 _. - case (Z.le_gt_cases ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4. - absurd (2 ^ (2 * [head0 x] )* [x] < 2 ^ [head0 (double_size x)] * [x]); auto. - apply Z.le_ngt. - apply Z.mul_le_mono_nonneg_r; auto with zarith. - apply Z.pow_le_mono_r; auto; auto with zarith. - assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1)). - { apply Z.le_succ_l in HH. change (1 <= [x]) in HH. - Z.le_elim HH. - - apply Z.mul_le_mono_pos_r with (2 ^ 1); auto with zarith. - rewrite <- (fun x y z => Z.pow_add_r x (y - z)); auto with zarith. - rewrite Z.sub_add. - apply Z.le_trans with (2 := Z.lt_le_incl _ _ HH2). - apply Z.mul_le_mono_nonneg_l; auto with zarith. - rewrite Z.pow_1_r; auto with zarith. - - apply Z.pow_le_mono_r; auto with zarith. - case (Z.le_gt_cases (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6. - absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith. - rewrite <- HH; rewrite Z.mul_1_r. - apply Z.pow_le_mono_r; auto with zarith. } - rewrite (Z.mul_comm 2). - rewrite Z.pow_mul_r; auto with zarith. - rewrite Z.pow_2_r. - apply Z.lt_le_trans with (2 := HH3). - rewrite <- Z.mul_assoc. - replace (2 * Zpos (digits x) - 1) with - ((Zpos (digits x) - 1) + (Zpos (digits x))). - rewrite Zpower_exp; auto with zarith. - apply Zmult_lt_compat2; auto with zarith. - split; auto with zarith. - apply Z.mul_pos_pos; auto with zarith. - rewrite Pos2Z.inj_xO; ring. - apply Z.lt_le_incl; auto. - repeat rewrite spec_head00; auto. - rewrite spec_double_size_digits. - rewrite Pos2Z.inj_xO; auto with zarith. - rewrite spec_double_size; auto. - Qed. - - Theorem spec_double_size_head0_pos: - forall x, 0 < [head0 (double_size x)]. - Proof. - intros x. - assert (F := Pos2Z.is_pos (digits x)). - assert (F0 := spec_pos (head0 (double_size x))). - Z.le_elim F0; auto. - assert (F1 := spec_pos (head0 x)). - Z.le_elim F1. - apply Z.lt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith. - assert (F3 := spec_pos x). - Z.le_elim F3. - generalize F3; rewrite <- (spec_double_size x); intros F4. - absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x))). - { apply Z.le_ngt. - apply Z.pow_le_mono_r; auto with zarith. - rewrite Pos2Z.inj_xO; auto with zarith. } - case (spec_head0 x F3). - rewrite <- F1; rewrite Z.pow_0_r; rewrite Z.mul_1_l; intros _ HH. - apply Z.le_lt_trans with (2 := HH). - case (spec_head0 _ F4). - rewrite (spec_double_size x); rewrite (spec_double_size_digits x). - rewrite <- F0; rewrite Z.pow_0_r; rewrite Z.mul_1_l; auto. - generalize F1; rewrite (spec_head00 _ (eq_sym F3)); auto with zarith. - Qed. - - (** Finally we iterate [double_size] enough before [unsafe_shiftl] - in order to get a fully correct [shiftl]. *) - - Definition shiftl_aux_body cont x n := - match compare n (head0 x) with - Gt => cont (double_size x) n - | _ => unsafe_shiftl x n - end. - - Theorem spec_shiftl_aux_body: forall n x p cont, - 2^ Zpos p <= [head0 x] -> - (forall x, 2 ^ (Zpos p + 1) <= [head0 x]-> - [cont x n] = [x] * 2 ^ [n]) -> - [shiftl_aux_body cont x n] = [x] * 2 ^ [n]. - Proof. - intros n x p cont H1 H2; unfold shiftl_aux_body. - rewrite spec_compare; case Z.compare_spec; intros H. - apply spec_unsafe_shiftl; auto with zarith. - apply spec_unsafe_shiftl; auto with zarith. - rewrite H2. - rewrite spec_double_size; auto. - rewrite Z.add_comm; rewrite Zpower_exp; auto with zarith. - apply Z.le_trans with (2 := spec_double_size_head0 x). - rewrite Z.pow_1_r; apply Z.mul_le_mono_nonneg_l; auto with zarith. - Qed. - - Fixpoint shiftl_aux p cont x n := - shiftl_aux_body - (fun x n => match p with - | xH => cont x n - | xO p => shiftl_aux p (shiftl_aux p cont) x n - | xI p => shiftl_aux p (shiftl_aux p cont) x n - end) x n. - - Theorem spec_shiftl_aux: forall p q x n cont, - 2 ^ (Zpos q) <= [head0 x] -> - (forall x, 2 ^ (Zpos p + Zpos q) <= [head0 x] -> - [cont x n] = [x] * 2 ^ [n]) -> - [shiftl_aux p cont x n] = [x] * 2 ^ [n]. - Proof. - intros p; elim p; unfold shiftl_aux; fold shiftl_aux; clear p. - intros p Hrec q x n cont H1 H2. - apply spec_shiftl_aux_body with (q); auto. - intros x1 H3; apply Hrec with (q + 1)%positive; auto. - intros x2 H4; apply Hrec with (p + q + 1)%positive; auto. - rewrite <- Pos.add_assoc. - rewrite Pos2Z.inj_add; auto. - intros x3 H5; apply H2. - rewrite Pos2Z.inj_xI. - replace (2 * Zpos p + 1 + Zpos q) with (Zpos p + Zpos (p + q + 1)); - auto. - rewrite !Pos2Z.inj_add; ring. - intros p Hrec q n x cont H1 H2. - apply spec_shiftl_aux_body with (q); auto. - intros x1 H3; apply Hrec with (q); auto. - apply Z.le_trans with (2 := H3); auto with zarith. - apply Z.pow_le_mono_r; auto with zarith. - intros x2 H4; apply Hrec with (p + q)%positive; auto. - intros x3 H5; apply H2. - rewrite (Pos2Z.inj_xO p). - replace (2 * Zpos p + Zpos q) with (Zpos p + Zpos (p + q)); - auto. - rewrite Pos2Z.inj_add; ring. - intros q n x cont H1 H2. - apply spec_shiftl_aux_body with (q); auto. - rewrite Z.add_comm; auto. - Qed. - - Definition shiftl x n := - shiftl_aux_body - (shiftl_aux_body - (shiftl_aux (digits n) unsafe_shiftl)) x n. - - Theorem spec_shiftl_pow2 : forall x n, - [shiftl x n] = [x] * 2 ^ [n]. - Proof. - intros x n; unfold shiftl, shiftl_aux_body. - rewrite spec_compare; case Z.compare_spec; intros H. - apply spec_unsafe_shiftl; auto with zarith. - apply spec_unsafe_shiftl; auto with zarith. - rewrite <- (spec_double_size x). - rewrite spec_compare; case Z.compare_spec; intros H1. - apply spec_unsafe_shiftl; auto with zarith. - apply spec_unsafe_shiftl; auto with zarith. - rewrite <- (spec_double_size (double_size x)). - apply spec_shiftl_aux with 1%positive. - apply Z.le_trans with (2 := spec_double_size_head0 (double_size x)). - replace (2 ^ 1) with (2 * 1). - apply Z.mul_le_mono_nonneg_l; auto with zarith. - generalize (spec_double_size_head0_pos x); auto with zarith. - rewrite Z.pow_1_r; ring. - intros x1 H2; apply spec_unsafe_shiftl. - apply Z.le_trans with (2 := H2). - apply Z.le_trans with (2 ^ Zpos (digits n)); auto with zarith. - case (spec_digits n); auto with zarith. - apply Z.pow_le_mono_r; auto with zarith. - Qed. - - Lemma spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p]. - Proof. - intros. - now rewrite spec_shiftl_pow2, Z.shiftl_mul_pow2 by apply spec_pos. - Qed. - - (** Other bitwise operations *) - - Definition testbit x n := odd (shiftr x n). - - Lemma spec_testbit: forall x p, testbit x p = Z.testbit [x] [p]. - Proof. - intros. unfold testbit. symmetry. - rewrite spec_odd, spec_shiftr. apply Z.testbit_odd. - Qed. - - Definition div2 x := shiftr x one. - - Lemma spec_div2: forall x, [div2 x] = Z.div2 [x]. - Proof. - intros. unfold div2. symmetry. - rewrite spec_shiftr, spec_1. apply Z.div2_spec. - Qed. - - 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. - - Lemma lor_fold : lor = same_level lorn. - Proof. red_t; reflexivity. Qed. - - Theorem spec_lor x y : [lor x y] = Z.lor [x] [y]. - Proof. - rewrite lor_fold. apply spec_same_level; clear x y. - intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_lor. - Qed. - - 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. - rewrite land_fold. apply spec_same_level; clear x y. - intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_land. - Qed. - - 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. - rewrite lxor_fold. apply spec_same_level; clear x y. - intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_lxor. - Qed. - - 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. |