diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN')
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 198 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 1706 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 1017 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 569 |
4 files changed, 0 insertions, 3490 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v deleted file mode 100644 index e8ff516f..00000000 --- a/theories/Numbers/Natural/BigN/BigN.v +++ /dev/null @@ -1,198 +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 *) -(************************************************************************) - -(** * Efficient arbitrary large natural numbers in base 2^31 *) - -(** Initial Author: Arnaud Spiwack *) - -Require Export Int31. -Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake - NProperties GenericMinMax. - -(** The following [BigN] module regroups both the operations and - all the abstract properties: - - - [NMake.Make Int31Cyclic] provides the operations and basic specs - w.r.t. ZArith - - [NTypeIsNAxioms] shows (mainly) that these operations implement - the interface [NAxioms] - - [NProp] adds all generic properties derived from [NAxioms] - - [MinMax*Properties] provides properties of [min] and [max]. - -*) - -Delimit Scope bigN_scope with bigN. - -Module BigN <: NType <: OrderedTypeFull <: TotalOrder := - NMake.Make Int31Cyclic - <+ NTypeIsNAxioms - <+ NBasicProp [no inline] <+ NExtraProp [no inline] - <+ HasEqBool2Dec [no inline] - <+ MinMaxLogicalProperties [no inline] - <+ MinMaxDecProperties [no inline]. - -(** Notations about [BigN] *) - -Local Open Scope bigN_scope. - -Notation bigN := BigN.t. -Bind Scope bigN_scope with bigN BigN.t BigN.t'. -Arguments BigN.N0 _%int31. -Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *) -Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *) -Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *) -Infix "+" := BigN.add : bigN_scope. -Infix "-" := BigN.sub : bigN_scope. -Infix "*" := BigN.mul : bigN_scope. -Infix "/" := BigN.div : bigN_scope. -Infix "^" := BigN.pow : bigN_scope. -Infix "?=" := BigN.compare : bigN_scope. -Infix "=?" := BigN.eqb (at level 70, no associativity) : bigN_scope. -Infix "<=?" := BigN.leb (at level 70, no associativity) : bigN_scope. -Infix "<?" := BigN.ltb (at level 70, no associativity) : bigN_scope. -Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope. -Notation "x != y" := (~x==y) (at level 70, no associativity) : bigN_scope. -Infix "<" := BigN.lt : bigN_scope. -Infix "<=" := BigN.le : bigN_scope. -Notation "x > y" := (y < x) (only parsing) : bigN_scope. -Notation "x >= y" := (y <= x) (only parsing) : bigN_scope. -Notation "x < y < z" := (x<y /\ y<z) : bigN_scope. -Notation "x < y <= z" := (x<y /\ y<=z) : bigN_scope. -Notation "x <= y < z" := (x<=y /\ y<z) : bigN_scope. -Notation "x <= y <= z" := (x<=y /\ y<=z) : bigN_scope. -Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. -Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope. - -(** Example of reasoning about [BigN] *) - -Theorem succ_pred: forall q : bigN, - 0 < q -> BigN.succ (BigN.pred q) == q. -Proof. -intros; apply BigN.succ_pred. -intro H'; rewrite H' in H; discriminate. -Qed. - -(** [BigN] is a semi-ring *) - -Lemma BigNring : semi_ring_theory 0 1 BigN.add BigN.mul BigN.eq. -Proof. -constructor. -exact BigN.add_0_l. exact BigN.add_comm. exact BigN.add_assoc. -exact BigN.mul_1_l. exact BigN.mul_0_l. exact BigN.mul_comm. -exact BigN.mul_assoc. exact BigN.mul_add_distr_r. -Qed. - -Lemma BigNeqb_correct : forall x y, (x =? y) = true -> x==y. -Proof. now apply BigN.eqb_eq. Qed. - -Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow. -Proof. -constructor. -intros. red. rewrite BigN.spec_pow, BigN.spec_of_N. -rewrite Zpower_theory.(rpow_pow_N). -destruct n; simpl. reflexivity. -induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto. -Qed. - -Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _) - (fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b). -Proof. -constructor. unfold id. intros a b. -BigN.zify. -case Z.eqb_spec. -BigN.zify. auto with zarith. -intros NEQ. -generalize (BigN.spec_div_eucl a b). -generalize (Z_div_mod_full [a] [b] NEQ). -destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1 as EQr EQq. -BigN.zify. rewrite EQr, EQq; auto. -Qed. - - -(** Detection of constants *) - -Ltac isStaticWordCst t := - match t with - | W0 => constr:(true) - | WW ?t1 ?t2 => - match isStaticWordCst t1 with - | false => constr:(false) - | true => isStaticWordCst t2 - end - | _ => isInt31cst t - end. - -Ltac isBigNcst t := - match t with - | BigN.N0 ?t => isStaticWordCst t - | BigN.N1 ?t => isStaticWordCst t - | BigN.N2 ?t => isStaticWordCst t - | BigN.N3 ?t => isStaticWordCst t - | BigN.N4 ?t => isStaticWordCst t - | BigN.N5 ?t => isStaticWordCst t - | BigN.N6 ?t => isStaticWordCst t - | BigN.Nn ?n ?t => match isnatcst n with - | true => isStaticWordCst t - | false => constr:(false) - end - | BigN.zero => constr:(true) - | BigN.one => constr:(true) - | BigN.two => constr:(true) - | _ => constr:(false) - end. - -Ltac BigNcst t := - match isBigNcst t with - | true => constr:(t) - | false => constr:(NotConstant) - end. - -Ltac BigN_to_N t := - match isBigNcst t with - | true => eval vm_compute in (BigN.to_N t) - | false => constr:(NotConstant) - end. - -Ltac Ncst t := - match isNcst t with - | true => constr:(t) - | false => constr:(NotConstant) - end. - -(** Registration for the "ring" tactic *) - -Add Ring BigNr : BigNring - (decidable BigNeqb_correct, - constants [BigNcst], - power_tac BigNpower [BigN_to_N], - div BigNdiv). - -Section TestRing. -Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x. -intros. ring_simplify. reflexivity. -Qed. -End TestRing. - -(** We benefit also from an "order" tactic *) - -Ltac bigN_order := BigN.order. - -Section TestOrder. -Let test : forall x y : bigN, x<=y -> y<=x -> x==y. -Proof. bigN_order. Qed. -End TestOrder. - -(** We can use at least a bit of (r)omega by translating to [Z]. *) - -Section TestOmega. -Let test : forall x y : bigN, x<=y -> y<=x -> x==y. -Proof. intros x y. BigN.zify. omega. Qed. -End TestOmega. - -(** Todo: micromega *) 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. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml deleted file mode 100644 index 5177fae6..00000000 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ /dev/null @@ -1,1017 +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 *) -(************************************************************************) - -(*S NMake_gen.ml : this file generates NMake_gen.v *) - - -(*s The parameter that control the generation: *) - -let size = 6 (* how many times should we repeat the Z/nZ --> Z/2nZ - process before relying on a generic construct *) - -(*s Some utilities *) - -let rec iter_str n s = if n = 0 then "" else (iter_str (n-1) s) ^ s - -let rec iter_str_gen n f = if n < 0 then "" else (iter_str_gen (n-1) f) ^ (f n) - -let rec iter_name i j base sep = - if i >= j then base^(string_of_int i) - else (iter_name i (j-1) base sep)^sep^" "^base^(string_of_int j) - -let pr s = Printf.printf (s^^"\n") - -(*s The actual printing *) - -let _ = - -pr -"(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \\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_gen *) - -(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*) - -(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *) - -Require Import BigNumPrelude ZArith Ndigits CyclicAxioms - DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic - Wf_nat StreamMemo. - -Module Make (W0:CyclicType) <: NAbstract. - - (** * The word types *) -"; - -pr " Local Notation w0 := W0.t."; -for i = 1 to size do - pr " Definition w%i := zn2z w%i." i (i-1) -done; -pr ""; - -pr " (** * The operation type classes for the word types *) -"; - -pr " Local Notation w0_op := W0.ops."; -for i = 1 to min 3 size do - pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops w%i_op." i i (i-1) -done; -for i = 4 to size do - pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops_karatsuba w%i_op." i i (i-1) -done; -for i = size+1 to size+3 do - pr " Instance w%i_op : ZnZ.Ops (word w%i %i) := mk_zn2z_ops_karatsuba w%i_op." i size (i-size) (i-1) -done; -pr ""; - - pr " Section Make_op."; - pr " Variable mk : forall w', ZnZ.Ops w' -> ZnZ.Ops (zn2z w')."; - pr ""; - pr " Fixpoint make_op_aux (n:nat) : ZnZ.Ops (word w%i (S n)):=" size; - pr " match n return ZnZ.Ops (word w%i (S n)) with" size; - pr " | O => w%i_op" (size+1); - pr " | S n1 =>"; - pr " match n1 return ZnZ.Ops (word w%i (S (S n1))) with" size; - pr " | O => w%i_op" (size+2); - pr " | S n2 =>"; - pr " match n2 return ZnZ.Ops (word w%i (S (S (S n2)))) with" size; - pr " | O => w%i_op" (size+3); - pr " | S n3 => mk _ (mk _ (mk _ (make_op_aux n3)))"; - pr " end"; - pr " end"; - pr " end."; - pr ""; - pr " End Make_op."; - pr ""; - pr " Definition omake_op := make_op_aux mk_zn2z_ops_karatsuba."; - pr ""; - pr ""; - pr " Definition make_op_list := dmemo_list _ omake_op."; - pr ""; - pr " Instance make_op n : ZnZ.Ops (word w%i (S n))" size; - pr " := dmemo_get _ omake_op n make_op_list."; - pr ""; - -pr " Ltac unfold_ops := unfold omake_op, make_op_aux, w%i_op, w%i_op." (size+3) (size+2); - -pr -" - Lemma make_op_omake: forall n, make_op n = omake_op n. - Proof. - intros n; unfold make_op, make_op_list. - refine (dmemo_get_correct _ _ _). - Qed. - - Theorem make_op_S: forall n, - make_op (S n) = mk_zn2z_ops_karatsuba (make_op n). - Proof. - intros n. do 2 rewrite make_op_omake. - revert n. fix IHn 1. - do 3 (destruct n; [unfold_ops; reflexivity|]). - simpl mk_zn2z_ops_karatsuba. simpl word in *. - rewrite <- (IHn n). auto. - Qed. - - (** * The main type [t], isomorphic with [exists n, word w0 n] *) -"; - - pr " Inductive t' :="; - for i = 0 to size do - pr " | N%i : w%i -> t'" i i - done; - pr " | Nn : forall n, word w%i (S n) -> t'." size; - pr ""; - pr " Definition t := t'."; - pr ""; - - pr " (** * A generic toolbox for building and deconstructing [t] *)"; - pr ""; - - pr " Local Notation SizePlus n := %sn%s." - (iter_str size "(S ") (iter_str size ")"); - pr " Local Notation Size := (SizePlus O)."; - pr ""; - - pr " Tactic Notation (at level 3) \"do_size\" tactic3(t) := do %i t." (size+1); - pr ""; - - pr " Definition dom_t n := match n with"; - for i = 0 to size do - pr " | %i => w%i" i i; - done; - pr " | %sn => word w%i n" (if size=0 then "" else "SizePlus ") size; - pr " end."; - pr ""; - -pr -" Instance dom_op n : ZnZ.Ops (dom_t n) | 10. - Proof. - do_size (destruct n; [simpl;auto with *|]). - unfold dom_t. auto with *. - Defined. -"; - - pr " Definition iter_t {A:Type}(f : forall n, dom_t n -> A) : t -> A :="; - for i = 0 to size do - pr " let f%i := f %i in" i i; - done; - pr " let fn n := f (SizePlus (S n)) in"; - pr " fun x => match x with"; - for i = 0 to size do - pr " | N%i wx => f%i wx" i i; - done; - pr " | Nn n wx => fn n wx"; - pr " end."; - pr ""; - - pr " Definition mk_t (n:nat) : dom_t n -> t :="; - pr " match n as n' return dom_t n' -> t with"; - for i = 0 to size do - pr " | %i => N%i" i i; - done; - pr " | %s(S n) => Nn n" (if size=0 then "" else "SizePlus "); - pr " end."; - pr ""; - -pr -" Definition level := iter_t (fun n _ => n). - - Inductive View_t : t -> Prop := - Mk_t : forall n (x : dom_t n), View_t (mk_t n x). - - Lemma destr_t : forall x, View_t x. - Proof. - intros x. generalize (Mk_t (level x)). destruct x; simpl; auto. - Defined. - - Lemma iter_mk_t : forall A (f:forall n, dom_t n -> A), - forall n x, iter_t f (mk_t n x) = f n x. - Proof. - do_size (destruct n; try reflexivity). - Qed. - - (** * Projection to ZArith *) - - Definition to_Z : t -> Z := - Eval lazy beta iota delta [iter_t dom_t dom_op] in - iter_t (fun _ x => ZnZ.to_Z x). - - Notation \"[ x ]\" := (to_Z x). - - Theorem spec_mk_t : forall n (x:dom_t n), [mk_t n x] = ZnZ.to_Z x. - Proof. - intros. change to_Z with (iter_t (fun _ x => ZnZ.to_Z x)). - rewrite iter_mk_t; auto. - Qed. - - (** * Regular make op, without memoization or karatsuba - - This will normally never be used for actual computations, - but only for specification purpose when using - [word (dom_t n) m] intermediate values. *) - - Fixpoint nmake_op (ww:Type) (ww_op: ZnZ.Ops ww) (n: nat) : - ZnZ.Ops (word ww n) := - match n return ZnZ.Ops (word ww n) with - O => ww_op - | S n1 => mk_zn2z_ops (nmake_op ww ww_op n1) - end. - - Definition eval n m := ZnZ.to_Z (Ops:=nmake_op _ (dom_op n) m). - - Theorem nmake_op_S: forall ww (w_op: ZnZ.Ops ww) x, - nmake_op _ w_op (S x) = mk_zn2z_ops (nmake_op _ w_op x). - Proof. - auto. - Qed. - - Theorem digits_nmake_S :forall n ww (w_op: ZnZ.Ops ww), - ZnZ.digits (nmake_op _ w_op (S n)) = - xO (ZnZ.digits (nmake_op _ w_op n)). - Proof. - auto. - Qed. - - Theorem digits_nmake : forall n ww (w_op: ZnZ.Ops ww), - ZnZ.digits (nmake_op _ w_op n) = Pos.shiftl_nat (ZnZ.digits w_op) n. - Proof. - induction n. auto. - intros ww ww_op. rewrite Pshiftl_nat_S, <- IHn; auto. - Qed. - - Theorem nmake_double: forall n ww (w_op: ZnZ.Ops ww), - ZnZ.to_Z (Ops:=nmake_op _ w_op n) = - @DoubleBase.double_to_Z _ (ZnZ.digits w_op) (ZnZ.to_Z (Ops:=w_op)) n. - Proof. - intros n; elim n; auto; clear n. - intros n Hrec ww ww_op; simpl DoubleBase.double_to_Z; unfold zn2z_to_Z. - rewrite <- Hrec; auto. - unfold DoubleBase.double_wB; rewrite <- digits_nmake; auto. - Qed. - - Theorem nmake_WW: forall ww ww_op n xh xl, - (ZnZ.to_Z (Ops:=nmake_op ww ww_op (S n)) (WW xh xl) = - ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xh * - base (ZnZ.digits (nmake_op ww ww_op n)) + - ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xl)%%Z. - Proof. - auto. - Qed. - - (** * The specification proofs for the word operators *) -"; - - if size <> 0 then - pr " Typeclasses Opaque %s." (iter_name 1 size "w" ""); - pr ""; - - pr " Instance w0_spec: ZnZ.Specs w0_op := W0.specs."; - for i = 1 to min 3 size do - pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs w%i_spec." i i (i-1) - done; - for i = 4 to size do - pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." i i (i-1) - done; - pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." (size+1) (size+1) size; - - -pr " - Instance wn_spec (n:nat) : ZnZ.Specs (make_op n). - Proof. - induction n. - rewrite make_op_omake; simpl; auto with *. - rewrite make_op_S. exact (mk_zn2z_specs_karatsuba IHn). - Qed. - - Instance dom_spec n : ZnZ.Specs (dom_op n) | 10. - Proof. - do_size (destruct n; auto with *). apply wn_spec. - Qed. - - Let make_op_WW : forall n x y, - (ZnZ.to_Z (Ops:=make_op (S n)) (WW x y) = - ZnZ.to_Z (Ops:=make_op n) x * base (ZnZ.digits (make_op n)) - + ZnZ.to_Z (Ops:=make_op n) y)%%Z. - Proof. - intros n x y; rewrite make_op_S; auto. - Qed. - - (** * Zero *) - - Definition zero0 : w0 := ZnZ.zero. - - Definition zeron n : dom_t n := - match n with - | O => zero0 - | SizePlus (S n) => W0 - | _ => W0 - end. - - Lemma spec_zeron : forall n, ZnZ.to_Z (zeron n) = 0%%Z. - Proof. - do_size (destruct n; - [match goal with - |- @eq Z (_ (zeron ?n)) _ => - apply (ZnZ.spec_0 (Specs:=dom_spec n)) - end|]). - destruct n; auto. simpl. rewrite make_op_S. fold word. - apply (ZnZ.spec_0 (Specs:=wn_spec (SizePlus 0))). - Qed. - - (** * Digits *) - - Lemma digits_make_op_0 : forall n, - ZnZ.digits (make_op n) = Pos.shiftl_nat (ZnZ.digits (dom_op Size)) (S n). - Proof. - induction n. - auto. - replace (ZnZ.digits (make_op (S n))) with (xO (ZnZ.digits (make_op n))). - rewrite IHn; auto. - rewrite make_op_S; auto. - Qed. - - Lemma digits_make_op : forall n, - ZnZ.digits (make_op n) = Pos.shiftl_nat (ZnZ.digits w0_op) (SizePlus (S n)). - Proof. - intros. rewrite digits_make_op_0. - replace (SizePlus (S n)) with (S n + Size) by (rewrite <- plus_comm; auto). - rewrite Pshiftl_nat_plus. auto. - Qed. - - Lemma digits_dom_op : forall n, - ZnZ.digits (dom_op n) = Pos.shiftl_nat (ZnZ.digits w0_op) n. - Proof. - do_size (destruct n; try reflexivity). - exact (digits_make_op n). - Qed. - - Lemma digits_dom_op_nmake : forall n m, - ZnZ.digits (dom_op (m+n)) = ZnZ.digits (nmake_op _ (dom_op n) m). - Proof. - intros. rewrite digits_nmake, 2 digits_dom_op. apply Pshiftl_nat_plus. - Qed. - - (** * Conversion between [zn2z (dom_t n)] and [dom_t (S n)]. - - These two types are provably equal, but not convertible, - hence we need some work. We now avoid using generic casts - (i.e. rewrite via proof of equalities in types), since - proving things with them is a mess. - *) - - Definition succ_t n : zn2z (dom_t n) -> dom_t (S n) := - match n with - | SizePlus (S _) => fun x => x - | _ => fun x => x - end. - - Lemma spec_succ_t : forall n x, - ZnZ.to_Z (succ_t n x) = - zn2z_to_Z (base (ZnZ.digits (dom_op n))) ZnZ.to_Z x. - Proof. - do_size (destruct n ; [reflexivity|]). - intros. simpl. rewrite make_op_S. simpl. auto. - Qed. - - Definition pred_t n : dom_t (S n) -> zn2z (dom_t n) := - match n with - | SizePlus (S _) => fun x => x - | _ => fun x => x - end. - - Lemma succ_pred_t : forall n x, succ_t n (pred_t n x) = x. - Proof. - do_size (destruct n ; [reflexivity|]). reflexivity. - Qed. - - (** We can hence project from [zn2z (dom_t n)] to [t] : *) - - Definition mk_t_S n (x : zn2z (dom_t n)) : t := - mk_t (S n) (succ_t n x). - - Lemma spec_mk_t_S : forall n x, - [mk_t_S n x] = zn2z_to_Z (base (ZnZ.digits (dom_op n))) ZnZ.to_Z x. - Proof. - intros. unfold mk_t_S. rewrite spec_mk_t. apply spec_succ_t. - Qed. - - Lemma mk_t_S_level : forall n x, level (mk_t_S n x) = S n. - Proof. - intros. unfold mk_t_S, level. rewrite iter_mk_t; auto. - Qed. - - (** * Conversion from [word (dom_t n) m] to [dom_t (m+n)]. - - Things are more complex here. We start with a naive version - that breaks zn2z-trees and reconstruct them. Doing this is - quite unfortunate, but I don't know how to fully avoid that. - (cast someday ?). Then we build an optimized version where - all basic cases (n<=6 or m<=7) are nicely handled. - *) - - Definition zn2z_map {A} {B} (f:A->B) (x:zn2z A) : zn2z B := - match x with - | W0 => W0 - | WW h l => WW (f h) (f l) - end. - - Lemma zn2z_map_id : forall A f (x:zn2z A), (forall u, f u = u) -> - zn2z_map f x = x. - Proof. - destruct x; auto; intros. - simpl; f_equal; auto. - Qed. - - (** The naive version *) - - Fixpoint plus_t n m : word (dom_t n) m -> dom_t (m+n) := - match m as m' return word (dom_t n) m' -> dom_t (m'+n) with - | O => fun x => x - | S m => fun x => succ_t _ (zn2z_map (plus_t n m) x) - end. - - Theorem spec_plus_t : forall n m (x:word (dom_t n) m), - ZnZ.to_Z (plus_t n m x) = eval n m x. - Proof. - unfold eval. - induction m. - simpl; auto. - intros. - simpl plus_t; simpl plus. rewrite spec_succ_t. - destruct x. - simpl; auto. - fold word in w, w0. - simpl. rewrite 2 IHm. f_equal. f_equal. f_equal. - apply digits_dom_op_nmake. - Qed. - - Definition mk_t_w n m (x:word (dom_t n) m) : t := - mk_t (m+n) (plus_t n m x). - - Theorem spec_mk_t_w : forall n m (x:word (dom_t n) m), - [mk_t_w n m x] = eval n m x. - Proof. - intros. unfold mk_t_w. rewrite spec_mk_t. apply spec_plus_t. - Qed. - - (** The optimized version. - - NB: the last particular case for m could depend on n, - but it's simplier to just expand everywhere up to m=7 - (cf [mk_t_w'] later). - *) - - Definition plus_t' n : forall m, word (dom_t n) m -> dom_t (m+n) := - match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with - | SizePlus (S n') as n => plus_t n - | _ as n => - fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with - | SizePlus (S (S m')) as m => plus_t n m - | _ => fun x => x - end - end. - - Lemma plus_t_equiv : forall n m x, - plus_t' n m x = plus_t n m x. - Proof. - (do_size try destruct n); try reflexivity; - (do_size try destruct m); try destruct m; try reflexivity; - simpl; symmetry; repeat (intros; apply zn2z_map_id; trivial). - Qed. - - Lemma spec_plus_t' : forall n m x, - ZnZ.to_Z (plus_t' n m x) = eval n m x. - Proof. - intros; rewrite plus_t_equiv. apply spec_plus_t. - Qed. - - (** Particular cases [Nk x] = eval i j x with specific k,i,j - can be solved by the following tactic *) - - Ltac solve_eval := - intros; rewrite <- spec_plus_t'; unfold to_Z; simpl dom_op; reflexivity. - - (** The last particular case that remains useful *) - - Lemma spec_eval_size : forall n x, [Nn n x] = eval Size (S n) x. - Proof. - induction n. - solve_eval. - destruct x as [ | xh xl ]. - simpl. unfold eval. rewrite make_op_S. rewrite nmake_op_S. auto. - simpl word in xh, xl |- *. - unfold to_Z in *. rewrite make_op_WW. - unfold eval in *. rewrite nmake_WW. - f_equal; auto. - f_equal; auto. - f_equal. - rewrite <- digits_dom_op_nmake. rewrite plus_comm; auto. - Qed. - - (** An optimized [mk_t_w]. - - We could say mk_t_w' := mk_t _ (plus_t' n m x) - (TODO: WHY NOT, BTW ??). - Instead we directly define functions for all intersting [n], - reverting to naive [mk_t_w] at places that should normally - never be used (see [mul] and [div_gt]). - *) -"; - -for i = 0 to size-1 do -let pattern = (iter_str (size+1-i) "(S ") ^ "_" ^ (iter_str (size+1-i) ")") in -pr -" Definition mk_t_%iw m := Eval cbv beta zeta iota delta [ mk_t plus ] in - match m return word w%i (S m) -> t with - | %s as p => mk_t_w %i (S p) - | p => mk_t (%i+p) - end. -" i i pattern i (i+1) -done; - -pr -" Definition mk_t_w' n : forall m, word (dom_t n) (S m) -> t := - match n return (forall m, word (dom_t n) (S m) -> t) with"; -for i = 0 to size-1 do pr " | %i => mk_t_%iw" i i done; -pr -" | Size => Nn - | _ as n' => fun m => mk_t_w n' (S m) - end. -"; - -pr -" Ltac solve_spec_mk_t_w' := - rewrite <- spec_plus_t'; - match goal with _ : word (dom_t ?n) ?m |- _ => apply (spec_mk_t (n+m)) end. - - Theorem spec_mk_t_w' : - forall n m x, [mk_t_w' n m x] = eval n (S m) x. - Proof. - intros. - repeat (apply spec_mk_t_w || (destruct n; - [repeat (apply spec_mk_t_w || (destruct m; [solve_spec_mk_t_w'|]))|])). - apply spec_eval_size. - Qed. - - (** * Extend : injecting [dom_t n] into [word (dom_t n) (S m)] *) - - Definition extend n m (x:dom_t n) : word (dom_t n) (S m) := - DoubleBase.extend_aux m (WW (zeron n) x). - - Lemma spec_extend : forall n m x, - [mk_t n x] = eval n (S m) (extend n m x). - Proof. - intros. unfold eval, extend. - rewrite spec_mk_t. - assert (H : forall (x:dom_t n), - (ZnZ.to_Z (zeron n) * base (ZnZ.digits (dom_op n)) + ZnZ.to_Z x = - ZnZ.to_Z x)%%Z). - clear; intros; rewrite spec_zeron; auto. - rewrite <- (@DoubleBase.spec_extend _ - (WW (zeron n)) (ZnZ.digits (dom_op n)) ZnZ.to_Z H m x). - simpl. rewrite digits_nmake, <- nmake_double. auto. - Qed. - - (** A particular case of extend, used in [same_level]: - [extend_size] is [extend Size] *) - - Definition extend_size := DoubleBase.extend (WW (W0:dom_t Size)). - - Lemma spec_extend_size : forall n x, [mk_t Size x] = [Nn n (extend_size n x)]. - Proof. - intros. rewrite spec_eval_size. apply (spec_extend Size n). - Qed. - - (** Misc results about extensions *) - - Let spec_extend_WW : forall n x, - [Nn (S n) (WW W0 x)] = [Nn n x]. - Proof. - intros n x. - set (N:=SizePlus (S n)). - change ([Nn (S n) (extend N 0 x)]=[mk_t N x]). - rewrite (spec_extend N 0). - solve_eval. - Qed. - - Let spec_extend_tr: forall m n w, - [Nn (m + n) (extend_tr w m)] = [Nn n w]. - Proof. - induction m; auto. - intros n x; simpl extend_tr. - simpl plus; rewrite spec_extend_WW; auto. - Qed. - - Let spec_cast_l: forall n m x1, - [Nn n x1] = - [Nn (Max.max n m) (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))]. - Proof. - intros n m x1; case (diff_r n m); simpl castm. - rewrite spec_extend_tr; auto. - Qed. - - Let spec_cast_r: forall n m x1, - [Nn m x1] = - [Nn (Max.max n m) (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))]. - Proof. - intros n m x1; case (diff_l n m); simpl castm. - rewrite spec_extend_tr; auto. - Qed. - - Ltac unfold_lets := - match goal with - | h : _ |- _ => unfold h; clear h; unfold_lets - | _ => idtac - end. - - (** * [same_level] - - Generic binary operator construction, by extending the smaller - argument to the level of the other. - *) - - Section SameLevel. - - Variable res: Type. - Variable P : Z -> Z -> res -> Prop. - Variable f : forall n, dom_t n -> dom_t n -> res. - Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y). -"; - -for i = 0 to size do -pr " Let f%i : w%i -> w%i -> res := f %i." i i i i -done; -pr -" Let fn n := f (SizePlus (S n)). - - Let Pf' : - forall n x y u v, u = [mk_t n x] -> v = [mk_t n y] -> P u v (f n x y). - Proof. - intros. subst. rewrite 2 spec_mk_t. apply Pf. - Qed. -"; - -let ext i j s = - if j <= i then s else Printf.sprintf "(extend %i %i %s)" i (j-i-1) s -in - -pr " Notation same_level_folded := (fun x y => match x, y with"; -for i = 0 to size do - for j = 0 to size do - pr " | N%i wx, N%i wy => f%i %s %s" i j (max i j) (ext i j "wx") (ext j i "wy") - done; - pr " | N%i wx, Nn m wy => fn m (extend_size m %s) wy" i (ext i size "wx") -done; -for i = 0 to size do - pr " | Nn n wx, N%i wy => fn n wx (extend_size n %s)" i (ext i size "wy") -done; -pr -" | Nn n wx, Nn m wy => - let mn := Max.max n m in - let d := diff n m in - fn mn - (castm (diff_r n m) (extend_tr wx (snd d))) - (castm (diff_l n m) (extend_tr wy (fst d))) - end). -"; - -pr -" Definition same_level := Eval lazy beta iota delta - [ DoubleBase.extend DoubleBase.extend_aux extend zeron ] - in same_level_folded. - - Lemma spec_same_level_0: forall x y, P [x] [y] (same_level x y). - Proof. - change same_level with same_level_folded. unfold_lets. - destruct x, y; apply Pf'; simpl mk_t; rewrite <- ?spec_extend_size; - match goal with - | |- context [ extend ?n ?m _ ] => apply (spec_extend n m) - | |- context [ castm _ _ ] => apply spec_cast_l || apply spec_cast_r - | _ => reflexivity - end. - Qed. - - End SameLevel. - - Arguments same_level [res] f x y. - - Theorem spec_same_level_dep : - forall res - (P : nat -> Z -> Z -> res -> Prop) - (Pantimon : forall n m z z' r, n <= m -> P m z z' r -> P n z z' r) - (f : forall n, dom_t n -> dom_t n -> res) - (Pf: forall n x y, P n (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)), - forall x y, P (level x) [x] [y] (same_level f x y). - Proof. - intros res P Pantimon f Pf. - set (f' := fun n x y => (n, f n x y)). - set (P' := fun z z' r => P (fst r) z z' (snd r)). - assert (FST : forall x y, level x <= fst (same_level f' x y)) - by (destruct x, y; simpl; omega with * ). - assert (SND : forall x y, same_level f x y = snd (same_level f' x y)) - by (destruct x, y; reflexivity). - intros. eapply Pantimon; [eapply FST|]. - rewrite SND. eapply (@spec_same_level_0 _ P' f'); eauto. - Qed. - - (** * [iter] - - Generic binary operator construction, by splitting the larger - argument in blocks and applying the smaller argument to them. - *) - - Section Iter. - - Variable res: Type. - Variable P: Z -> Z -> res -> Prop. - - Variable f : forall n, dom_t n -> dom_t n -> res. - Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y). - - Variable fd : forall n m, dom_t n -> word (dom_t n) (S m) -> res. - Variable fg : forall n m, word (dom_t n) (S m) -> dom_t n -> res. - Variable Pfd : forall n m x y, P (ZnZ.to_Z x) (eval n (S m) y) (fd n m x y). - Variable Pfg : forall n m x y, P (eval n (S m) x) (ZnZ.to_Z y) (fg n m x y). - - Variable fnm: forall n m, word (dom_t Size) (S n) -> word (dom_t Size) (S m) -> res. - Variable Pfnm: forall n m x y, P [Nn n x] [Nn m y] (fnm n m x y). - - Let Pf' : - forall n x y u v, u = [mk_t n x] -> v = [mk_t n y] -> P u v (f n x y). - Proof. - intros. subst. rewrite 2 spec_mk_t. apply Pf. - Qed. - - Let Pfd' : forall n m x y u v, u = [mk_t n x] -> v = eval n (S m) y -> - P u v (fd n m x y). - Proof. - intros. subst. rewrite spec_mk_t. apply Pfd. - Qed. - - Let Pfg' : forall n m x y u v, u = eval n (S m) x -> v = [mk_t n y] -> - P u v (fg n m x y). - Proof. - intros. subst. rewrite spec_mk_t. apply Pfg. - Qed. -"; - -for i = 0 to size do -pr " Let f%i := f %i." i i -done; - -for i = 0 to size do -pr " Let f%in := fd %i." i i; -pr " Let fn%i := fg %i." i i; -done; - -pr " Notation iter_folded := (fun x y => match x, y with"; -for i = 0 to size do - for j = 0 to size do - pr " | N%i wx, N%i wy => f%s wx wy" i j - (if i = j then string_of_int i - else if i < j then string_of_int i ^ "n " ^ string_of_int (j-i-1) - else "n" ^ string_of_int j ^ " " ^ string_of_int (i-j-1)) - done; - pr " | N%i wx, Nn m wy => f%in m %s wy" i size (ext i size "wx") -done; -for i = 0 to size do - pr " | Nn n wx, N%i wy => fn%i n wx %s" i size (ext i size "wy") -done; -pr -" | Nn n wx, Nn m wy => fnm n m wx wy - end). -"; - -pr -" Definition iter := Eval lazy beta iota delta - [extend DoubleBase.extend DoubleBase.extend_aux zeron] - in iter_folded. - - Lemma spec_iter: forall x y, P [x] [y] (iter x y). - Proof. - change iter with iter_folded; unfold_lets. - destruct x; destruct y; apply Pf' || apply Pfd' || apply Pfg' || apply Pfnm; - simpl mk_t; - match goal with - | |- ?x = ?x => reflexivity - | |- [Nn _ _] = _ => apply spec_eval_size - | |- context [extend ?n ?m _] => apply (spec_extend n m) - | _ => idtac - end; - unfold to_Z; rewrite <- spec_plus_t'; simpl dom_op; reflexivity. - Qed. - - End Iter. -"; - -pr -" Definition switch - (P:nat->Type)%s - (fn:forall n, P n) n := - match n return P n with" - (iter_str_gen size (fun i -> Printf.sprintf "(f%i:P %i)" i i)); -for i = 0 to size do pr " | %i => f%i" i i done; -pr -" | n => fn n - end. -"; - -pr -" Lemma spec_switch : forall P (f:forall n, P n) n, - switch P %sf n = f n. - Proof. - repeat (destruct n; try reflexivity). - Qed. -" (iter_str_gen size (fun i -> Printf.sprintf "(f %i) " i)); - -pr -" (** * [iter_sym] - - A variant of [iter] for symmetric functions, or pseudo-symmetric - functions (when f y x can be deduced from f x y). - *) - - Section IterSym. - - Variable res: Type. - Variable P: Z -> Z -> res -> Prop. - - Variable f : forall n, dom_t n -> dom_t n -> res. - Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y). - - Variable fg : forall n m, word (dom_t n) (S m) -> dom_t n -> res. - Variable Pfg : forall n m x y, P (eval n (S m) x) (ZnZ.to_Z y) (fg n m x y). - - Variable fnm: forall n m, word (dom_t Size) (S n) -> word (dom_t Size) (S m) -> res. - Variable Pfnm: forall n m x y, P [Nn n x] [Nn m y] (fnm n m x y). - - Variable opp: res -> res. - Variable Popp : forall u v r, P u v r -> P v u (opp r). -"; - -for i = 0 to size do -pr " Let f%i := f %i." i i -done; - -for i = 0 to size do -pr " Let fn%i := fg %i." i i; -done; - -pr " Let f' := switch _ %s f." (iter_name 0 size "f" ""); -pr " Let fg' := switch _ %s fg." (iter_name 0 size "fn" ""); - -pr -" Local Notation iter_sym_folded := - (iter res f' (fun n m x y => opp (fg' n m y x)) fg' fnm). - - Definition iter_sym := - Eval lazy beta zeta iota delta [iter f' fg' switch] in iter_sym_folded. - - Lemma spec_iter_sym: forall x y, P [x] [y] (iter_sym x y). - Proof. - intros. change iter_sym with iter_sym_folded. apply spec_iter; clear x y. - unfold_lets. - intros. rewrite spec_switch. auto. - intros. apply Popp. unfold_lets. rewrite spec_switch; auto. - intros. unfold_lets. rewrite spec_switch; auto. - auto. - Qed. - - End IterSym. - - (** * Reduction - - [reduce] can be used instead of [mk_t], it will choose the - lowest possible level. NB: We only search and remove leftmost - W0's via ZnZ.eq0, any non-W0 block ends the process, even - if its value is 0. - *) - - (** First, a direct version ... *) - - Fixpoint red_t n : dom_t n -> t := - match n return dom_t n -> t with - | O => N0 - | S n => fun x => - let x' := pred_t n x in - reduce_n1 _ _ (N0 zero0) ZnZ.eq0 (red_t n) (mk_t_S n) x' - end. - - Lemma spec_red_t : forall n x, [red_t n x] = [mk_t n x]. - Proof. - induction n. - reflexivity. - intros. - simpl red_t. unfold reduce_n1. - rewrite <- (succ_pred_t n x) at 2. - remember (pred_t n x) as x'. - rewrite spec_mk_t, spec_succ_t. - destruct x' as [ | xh xl]. simpl. apply ZnZ.spec_0. - generalize (ZnZ.spec_eq0 xh); case ZnZ.eq0; intros H. - rewrite IHn, spec_mk_t. simpl. rewrite H; auto. - apply spec_mk_t_S. - Qed. - - (** ... then a specialized one *) -"; - -for i = 0 to size do -pr " Definition eq0%i := @ZnZ.eq0 _ w%i_op." i i; -done; - -pr " - Definition reduce_0 := N0."; -for i = 1 to size do - pr " Definition reduce_%i :=" i; - pr " Eval lazy beta iota delta [reduce_n1] in"; - pr " reduce_n1 _ _ (N0 zero0) eq0%i reduce_%i N%i." (i-1) (i-1) i -done; - - pr " Definition reduce_%i :=" (size+1); - pr " Eval lazy beta iota delta [reduce_n1] in"; - pr " reduce_n1 _ _ (N0 zero0) eq0%i reduce_%i (Nn 0)." size size; - - pr " Definition reduce_n n :="; - pr " Eval lazy beta iota delta [reduce_n] in"; - pr " reduce_n _ _ (N0 zero0) reduce_%i Nn n." (size + 1); - pr ""; - -pr " Definition reduce n : dom_t n -> t :="; -pr " match n with"; -for i = 0 to size do -pr " | %i => reduce_%i" i i; -done; -pr " | %s(S n) => reduce_n n" (if size=0 then "" else "SizePlus "); -pr " end."; -pr ""; - -pr " Ltac unfold_red := unfold reduce, %s." (iter_name 1 size "reduce_" ","); -pr ""; -for i = 0 to size do -pr " Declare Equivalent Keys reduce reduce_%i." i; -done; -pr " Declare Equivalent Keys reduce_n reduce_%i." (size + 1); - -pr " - Ltac solve_red := - let H := fresh in let G := fresh in - match goal with - | |- ?P (S ?n) => assert (H:P n) by solve_red - | _ => idtac - end; - intros n G x; destruct (le_lt_eq_dec _ _ G) as [LT|EQ]; - solve [ - apply (H _ (lt_n_Sm_le _ _ LT)) | - inversion LT | - subst; change (reduce 0 x = red_t 0 x); reflexivity | - specialize (H (pred n)); subst; destruct x; - [|unfold_red; rewrite H; auto]; reflexivity - ]. - - Lemma reduce_equiv : forall n x, n <= Size -> reduce n x = red_t n x. - Proof. - set (P N := forall n, n <= N -> forall x, reduce n x = red_t n x). - intros n x H. revert n H x. change (P Size). solve_red. - Qed. - - Lemma spec_reduce_n : forall n x, [reduce_n n x] = [Nn n x]. - Proof. - assert (H : forall x, reduce_%i x = red_t (SizePlus 1) x). - destruct x; [|unfold reduce_%i; rewrite (reduce_equiv Size)]; auto. - induction n. - intros. rewrite H. apply spec_red_t. - destruct x as [|xh xl]. - simpl. rewrite make_op_S. exact ZnZ.spec_0. - fold word in *. - destruct xh; auto. - simpl reduce_n. - rewrite IHn. - rewrite spec_extend_WW; auto. - Qed. -" (size+1) (size+1); - -pr -" Lemma spec_reduce : forall n x, [reduce n x] = ZnZ.to_Z x. - Proof. - do_size (destruct n; - [intros; rewrite reduce_equiv;[apply spec_red_t|auto with arith]|]). - apply spec_reduce_n. - Qed. - -End Make. -"; diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v deleted file mode 100644 index 18d0262c..00000000 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ /dev/null @@ -1,569 +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 *) -(************************************************************************) - -Require Import ZArith Ndigits. -Require Import BigNumPrelude. -Require Import Max. -Require Import DoubleType. -Require Import DoubleBase. -Require Import CyclicAxioms. -Require Import DoubleCyclic. - -Arguments mk_zn2z_ops [t] ops. -Arguments mk_zn2z_ops_karatsuba [t] ops. -Arguments mk_zn2z_specs [t ops] specs. -Arguments mk_zn2z_specs_karatsuba [t ops] specs. -Arguments ZnZ.digits [t] Ops. -Arguments ZnZ.zdigits [t] Ops. - -Lemma Pshiftl_nat_Zpower : forall n p, - Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n. -Proof. - intros. - rewrite Z.mul_comm. - induction n. simpl; auto. - transitivity (2 * (2 ^ Z.of_nat n * Zpos p)). - rewrite <- IHn. auto. - rewrite Z.mul_assoc. - rewrite Nat2Z.inj_succ. - rewrite <- Z.pow_succ_r; auto with zarith. -Qed. - -(* To compute the necessary height *) - -Fixpoint plength (p: positive) : positive := - match p with - xH => xH - | xO p1 => Pos.succ (plength p1) - | xI p1 => Pos.succ (plength p1) - end. - -Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z. -assert (F: (forall p, 2 ^ (Zpos (Pos.succ p)) = 2 * 2 ^ Zpos p)%Z). -intros p; replace (Zpos (Pos.succ p)) with (1 + Zpos p)%Z. -rewrite Zpower_exp; auto with zarith. -rewrite Pos2Z.inj_succ; unfold Z.succ; auto with zarith. -intros p; elim p; simpl plength; auto. -intros p1 Hp1; rewrite F; repeat rewrite Pos2Z.inj_xI. -assert (tmp: (forall p, 2 * p = p + p)%Z); - try repeat rewrite tmp; auto with zarith. -intros p1 Hp1; rewrite F; rewrite (Pos2Z.inj_xO p1). -assert (tmp: (forall p, 2 * p = p + p)%Z); - try repeat rewrite tmp; auto with zarith. -rewrite Z.pow_1_r; auto with zarith. -Qed. - -Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Pos.pred p)))%Z. -intros p; case (Pos.succ_pred_or p); intros H1. -subst; simpl plength. -rewrite Z.pow_1_r; auto with zarith. -pattern p at 1; rewrite <- H1. -rewrite Pos2Z.inj_succ; unfold Z.succ; auto with zarith. -generalize (plength_correct (Pos.pred p)); auto with zarith. -Qed. - -Definition Pdiv p q := - match Z.div (Zpos p) (Zpos q) with - Zpos q1 => match (Zpos p) - (Zpos q) * (Zpos q1) with - Z0 => q1 - | _ => (Pos.succ q1) - end - | _ => xH - end. - -Theorem Pdiv_le: forall p q, - Zpos p <= Zpos q * Zpos (Pdiv p q). -intros p q. -unfold Pdiv. -assert (H1: Zpos q > 0); auto with zarith. -assert (H1b: Zpos p >= 0); auto with zarith. -generalize (Z_div_ge0 (Zpos p) (Zpos q) H1 H1b). -generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Z.div. - intros HH _; rewrite HH; rewrite Z.mul_0_r; rewrite Z.mul_1_r; simpl. -case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith. -intros q1 H2. -replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q). - 2: pattern (Zpos p) at 2; rewrite H2; auto with zarith. -generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2; - case Z.modulo. - intros HH _; rewrite HH; auto with zarith. - intros r1 HH (_,HH1); rewrite HH; rewrite Pos2Z.inj_succ. - unfold Z.succ; rewrite Z.mul_add_distr_l; auto with zarith. - intros r1 _ (HH,_); case HH; auto. -intros q1 HH; rewrite HH. -unfold Z.ge; simpl Z.compare; intros HH1; case HH1; auto. -Qed. - -Definition is_one p := match p with xH => true | _ => false end. - -Theorem is_one_one: forall p, is_one p = true -> p = xH. -intros p; case p; auto; intros p1 H1; discriminate H1. -Qed. - -Definition get_height digits p := - let r := Pdiv p digits in - if is_one r then xH else Pos.succ (plength (Pos.pred r)). - -Theorem get_height_correct: - forall digits N, - Zpos N <= Zpos digits * (2 ^ (Zpos (get_height digits N) -1)). -intros digits N. -unfold get_height. -assert (H1 := Pdiv_le N digits). -case_eq (is_one (Pdiv N digits)); intros H2. -rewrite (is_one_one _ H2) in H1. -rewrite Z.mul_1_r in H1. -change (2^(1-1))%Z with 1; rewrite Z.mul_1_r; auto. -clear H2. -apply Z.le_trans with (1 := H1). -apply Z.mul_le_mono_nonneg_l; auto with zarith. -rewrite Pos2Z.inj_succ; unfold Z.succ. -rewrite Z.add_comm; rewrite Z.add_simpl_l. -apply plength_pred_correct. -Qed. - -Definition zn2z_word_comm : forall w n, zn2z (word w n) = word (zn2z w) n. - fix zn2z_word_comm 2. - intros w n; case n. - reflexivity. - intros n0;simpl. - case (zn2z_word_comm w n0). - reflexivity. -Defined. - -Fixpoint extend (n:nat) {struct n} : forall w:Type, zn2z w -> word w (S n) := - match n return forall w:Type, zn2z w -> word w (S n) with - | O => fun w x => x - | S m => - let aux := extend m in - fun w x => WW W0 (aux w x) - end. - -Section ExtendMax. - -Open Scope nat_scope. - -Fixpoint plusnS (n m: nat) {struct n} : (n + S m = S (n + m))%nat := - match n return (n + S m = S (n + m))%nat with - | 0 => eq_refl (S m) - | S n1 => - let v := S (S n1 + m) in - eq_ind_r (fun n => S n = v) (eq_refl v) (plusnS n1 m) - end. - -Fixpoint plusn0 n : n + 0 = n := - match n return (n + 0 = n) with - | 0 => eq_refl 0 - | S n1 => - let v := S n1 in - eq_ind_r (fun n : nat => S n = v) (eq_refl v) (plusn0 n1) - end. - - Fixpoint diff (m n: nat) {struct m}: nat * nat := - match m, n with - O, n => (O, n) - | m, O => (m, O) - | S m1, S n1 => diff m1 n1 - end. - -Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n := - match m return fst (diff m n) + n = max m n with - | 0 => - match n return (n = max 0 n) with - | 0 => eq_refl _ - | S n0 => eq_refl _ - end - | S m1 => - match n return (fst (diff (S m1) n) + n = max (S m1) n) - with - | 0 => plusn0 _ - | S n1 => - let v := fst (diff m1 n1) + n1 in - let v1 := fst (diff m1 n1) + S n1 in - eq_ind v (fun n => v1 = S n) - (eq_ind v1 (fun n => v1 = n) (eq_refl v1) (S v) (plusnS _ _)) - _ (diff_l _ _) - end - end. - -Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n := - match m return (snd (diff m n) + m = max m n) with - | 0 => - match n return (snd (diff 0 n) + 0 = max 0 n) with - | 0 => eq_refl _ - | S _ => plusn0 _ - end - | S m => - match n return (snd (diff (S m) n) + S m = max (S m) n) with - | 0 => eq_refl (snd (diff (S m) 0) + S m) - | S n1 => - let v := S (max m n1) in - eq_ind_r (fun n => n = v) - (eq_ind_r (fun n => S n = v) - (eq_refl v) (diff_r _ _)) (plusnS _ _) - end - end. - - Variable w: Type. - - Definition castm (m n: nat) (H: m = n) (x: word w (S m)): - (word w (S n)) := - match H in (_ = y) return (word w (S y)) with - | eq_refl => x - end. - -Variable m: nat. -Variable v: (word w (S m)). - -Fixpoint extend_tr (n : nat) {struct n}: (word w (S (n + m))) := - match n return (word w (S (n + m))) with - | O => v - | S n1 => WW W0 (extend_tr n1) - end. - -End ExtendMax. - -Arguments extend_tr [w m] v n. -Arguments castm [w m n] H x. - - - -Section Reduce. - - Variable w : Type. - Variable nT : Type. - Variable N0 : nT. - Variable eq0 : w -> bool. - Variable reduce_n : w -> nT. - Variable zn2z_to_Nt : zn2z w -> nT. - - Definition reduce_n1 (x:zn2z w) := - match x with - | W0 => N0 - | WW xh xl => - if eq0 xh then reduce_n xl - else zn2z_to_Nt x - end. - -End Reduce. - -Section ReduceRec. - - Variable w : Type. - Variable nT : Type. - Variable N0 : nT. - Variable reduce_1n : zn2z w -> nT. - Variable c : forall n, word w (S n) -> nT. - - Fixpoint reduce_n (n:nat) : word w (S n) -> nT := - match n return word w (S n) -> nT with - | O => reduce_1n - | S m => fun x => - match x with - | W0 => N0 - | WW xh xl => - match xh with - | W0 => @reduce_n m xl - | _ => @c (S m) x - end - end - end. - -End ReduceRec. - -Section CompareRec. - - Variable wm w : Type. - Variable w_0 : w. - Variable compare : w -> w -> comparison. - Variable compare0_m : wm -> comparison. - Variable compare_m : wm -> w -> comparison. - - Fixpoint compare0_mn (n:nat) : word wm n -> comparison := - match n return word wm n -> comparison with - | O => compare0_m - | S m => fun x => - match x with - | W0 => Eq - | WW xh xl => - match compare0_mn m xh with - | Eq => compare0_mn m xl - | r => Lt - end - end - end. - - Variable wm_base: positive. - Variable wm_to_Z: wm -> Z. - Variable w_to_Z: w -> Z. - Variable w_to_Z_0: w_to_Z w_0 = 0. - Variable spec_compare0_m: forall x, - compare0_m x = (w_to_Z w_0 ?= wm_to_Z x). - Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base. - - Let double_to_Z := double_to_Z wm_base wm_to_Z. - Let double_wB := double_wB wm_base. - - Lemma base_xO: forall n, base (xO n) = (base n)^2. - Proof. - intros n1; unfold base. - rewrite (Pos2Z.inj_xO n1); rewrite Z.mul_comm; rewrite Z.pow_mul_r; auto with zarith. - Qed. - - Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n := - (spec_double_to_Z wm_base wm_to_Z wm_to_Z_pos). - - Declare Equivalent Keys compare0_mn compare0_m. - - Lemma spec_compare0_mn: forall n x, - compare0_mn n x = (0 ?= double_to_Z n x). - Proof. - intros n; elim n; clear n; auto. - intros x; rewrite spec_compare0_m; rewrite w_to_Z_0; auto. - intros n Hrec x; case x; unfold compare0_mn; fold compare0_mn; auto. - fold word in *. - intros xh xl. - rewrite 2 Hrec. - simpl double_to_Z. - set (wB := DoubleBase.double_wB wm_base n). - case Z.compare_spec; intros Cmp. - rewrite <- Cmp. reflexivity. - symmetry. apply Z.gt_lt, Z.lt_gt. (* ;-) *) - assert (0 < wB). - unfold wB, DoubleBase.double_wB, base; auto with zarith. - change 0 with (0 + 0); apply Z.add_lt_le_mono; auto with zarith. - apply Z.mul_pos_pos; auto with zarith. - case (double_to_Z_pos n xl); auto with zarith. - case (double_to_Z_pos n xh); intros; exfalso; omega. - Qed. - - Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison := - match n return word wm n -> w -> comparison with - | O => compare_m - | S m => fun x y => - match x with - | W0 => compare w_0 y - | WW xh xl => - match compare0_mn m xh with - | Eq => compare_mn_1 m xl y - | r => Gt - end - end - end. - - Variable spec_compare: forall x y, - compare x y = Z.compare (w_to_Z x) (w_to_Z y). - Variable spec_compare_m: forall x y, - compare_m x y = Z.compare (wm_to_Z x) (w_to_Z y). - Variable wm_base_lt: forall x, - 0 <= w_to_Z x < base (wm_base). - - Let double_wB_lt: forall n x, - 0 <= w_to_Z x < (double_wB n). - Proof. - intros n x; elim n; simpl; auto; clear n. - intros n (H0, H); split; auto. - apply Z.lt_le_trans with (1:= H). - unfold double_wB, DoubleBase.double_wB; simpl. - rewrite base_xO. - set (u := base (Pos.shiftl_nat wm_base n)). - assert (0 < u). - unfold u, base; auto with zarith. - replace (u^2) with (u * u); simpl; auto with zarith. - apply Z.le_trans with (1 * u); auto with zarith. - unfold Z.pow_pos; simpl; ring. - Qed. - - - Lemma spec_compare_mn_1: forall n x y, - compare_mn_1 n x y = Z.compare (double_to_Z n x) (w_to_Z y). - Proof. - intros n; elim n; simpl; auto; clear n. - intros n Hrec x; case x; clear x; auto. - intros y; rewrite spec_compare; rewrite w_to_Z_0. reflexivity. - intros xh xl y; simpl; - rewrite spec_compare0_mn, Hrec. case Z.compare_spec. - intros H1b. - rewrite <- H1b; rewrite Z.mul_0_l; rewrite Z.add_0_l; auto. - symmetry. apply Z.lt_gt. - case (double_wB_lt n y); intros _ H0. - apply Z.lt_le_trans with (1:= H0). - fold double_wB. - case (double_to_Z_pos n xl); intros H1 H2. - apply Z.le_trans with (double_to_Z n xh * double_wB n); auto with zarith. - apply Z.le_trans with (1 * double_wB n); auto with zarith. - case (double_to_Z_pos n xh); intros; exfalso; omega. - Qed. - -End CompareRec. - - -Section AddS. - - Variable w wm : Type. - Variable incr : wm -> carry wm. - Variable addr : w -> wm -> carry wm. - Variable injr : w -> zn2z wm. - - Variable w_0 u: w. - Fixpoint injs (n:nat): word w (S n) := - match n return (word w (S n)) with - O => WW w_0 u - | S n1 => (WW W0 (injs n1)) - end. - - Definition adds x y := - match y with - W0 => C0 (injr x) - | WW hy ly => match addr x ly with - C0 z => C0 (WW hy z) - | C1 z => match incr hy with - C0 z1 => C0 (WW z1 z) - | C1 z1 => C1 (WW z1 z) - end - end - end. - -End AddS. - - Fixpoint length_pos x := - match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end. - - Theorem length_pos_lt: forall x y, - (length_pos x < length_pos y)%nat -> Zpos x < Zpos y. - Proof. - intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac]; - intros y; case y; clear y; intros y1 H || intros H; simpl length_pos; - try (rewrite (Pos2Z.inj_xI x1) || rewrite (Pos2Z.inj_xO x1)); - try (rewrite (Pos2Z.inj_xI y1) || rewrite (Pos2Z.inj_xO y1)); - try (inversion H; fail); - try (assert (Zpos x1 < Zpos y1); [apply Hrec; apply lt_S_n | idtac]; auto with zarith); - assert (0 < Zpos y1); auto with zarith; red; auto. - Qed. - - Theorem cancel_app: forall A B (f g: A -> B) x, f = g -> f x = g x. - Proof. - intros A B f g x H; rewrite H; auto. - Qed. - - - Section SimplOp. - - Variable w: Type. - - Theorem digits_zop: forall t (ops : ZnZ.Ops t), - ZnZ.digits (mk_zn2z_ops ops) = xO (ZnZ.digits ops). - Proof. - intros ww x; auto. - Qed. - - Theorem digits_kzop: forall t (ops : ZnZ.Ops t), - ZnZ.digits (mk_zn2z_ops_karatsuba ops) = xO (ZnZ.digits ops). - Proof. - intros ww x; auto. - Qed. - - Theorem make_zop: forall t (ops : ZnZ.Ops t), - @ZnZ.to_Z _ (mk_zn2z_ops ops) = - fun z => match z with - | W0 => 0 - | WW xh xl => ZnZ.to_Z xh * base (ZnZ.digits ops) - + ZnZ.to_Z xl - end. - Proof. - intros ww x; auto. - Qed. - - Theorem make_kzop: forall t (ops: ZnZ.Ops t), - @ZnZ.to_Z _ (mk_zn2z_ops_karatsuba ops) = - fun z => match z with - | W0 => 0 - | WW xh xl => ZnZ.to_Z xh * base (ZnZ.digits ops) - + ZnZ.to_Z xl - end. - Proof. - intros ww x; auto. - Qed. - - End SimplOp. - -(** Abstract vision of a datatype of arbitrary-large numbers. - Concrete operations can be derived from these generic - fonctions, in particular from [iter_t] and [same_level]. -*) - -Module Type NAbstract. - -(** The domains: a sequence of [Z/nZ] structures *) - -Parameter dom_t : nat -> Type. -Declare Instance dom_op n : ZnZ.Ops (dom_t n). -Declare Instance dom_spec n : ZnZ.Specs (dom_op n). - -Axiom digits_dom_op : forall n, - ZnZ.digits (dom_op n) = Pos.shiftl_nat (ZnZ.digits (dom_op 0)) n. - -(** The type [t] of arbitrary-large numbers, with abstract constructor [mk_t] - and destructor [destr_t] and iterator [iter_t] *) - -Parameter t : Type. - -Parameter mk_t : forall (n:nat), dom_t n -> t. - -Inductive View_t : t -> Prop := - Mk_t : forall n (x : dom_t n), View_t (mk_t n x). - -Axiom destr_t : forall x, View_t x. (* i.e. every x is a (mk_t n xw) *) - -Parameter iter_t : forall {A:Type}(f : forall n, dom_t n -> A), t -> A. - -Axiom iter_mk_t : forall A (f:forall n, dom_t n -> A), - forall n x, iter_t f (mk_t n x) = f n x. - -(** Conversion to [ZArith] *) - -Parameter to_Z : t -> Z. -Local Notation "[ x ]" := (to_Z x). - -Axiom spec_mk_t : forall n x, [mk_t n x] = ZnZ.to_Z x. - -(** [reduce] is like [mk_t], but try to minimise the level of the number *) - -Parameter reduce : forall (n:nat), dom_t n -> t. -Axiom spec_reduce : forall n x, [reduce n x] = ZnZ.to_Z x. - -(** Number of level in the tree representation of a number. - NB: This function isn't a morphism for setoid [eq]. *) - -Definition level := iter_t (fun n _ => n). - -(** [same_level] and its rich specification, indexed by [level] *) - -Parameter same_level : forall {A:Type} - (f : forall n, dom_t n -> dom_t n -> A), t -> t -> A. - -Axiom spec_same_level_dep : - forall res - (P : nat -> Z -> Z -> res -> Prop) - (Pantimon : forall n m z z' r, (n <= m)%nat -> P m z z' r -> P n z z' r) - (f : forall n, dom_t n -> dom_t n -> res) - (Pf: forall n x y, P n (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)), - forall x y, P (level x) [x] [y] (same_level f x y). - -(** [mk_t_S] : building a number of the next level *) - -Parameter mk_t_S : forall (n:nat), zn2z (dom_t n) -> t. - -Axiom spec_mk_t_S : forall n (x:zn2z (dom_t n)), - [mk_t_S n x] = zn2z_to_Z (base (ZnZ.digits (dom_op n))) ZnZ.to_Z x. - -Axiom mk_t_S_level : forall n x, level (mk_t_S n x) = S n. - -End NAbstract. |