diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN')
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 109 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 1576 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 3511 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 323 |
4 files changed, 2522 insertions, 2997 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 7c480862..072b75f7 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,7 +12,7 @@ Require Export Int31. Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake - NProperties NDiv GenericMinMax. + NProperties GenericMinMax. (** The following [BigN] module regroups both the operations and all the abstract properties: @@ -21,73 +21,63 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake w.r.t. ZArith - [NTypeIsNAxioms] shows (mainly) that these operations implement the interface [NAxioms] - - [NPropSig] adds all generic properties derived from [NAxioms] - - [NDivPropFunct] provides generic properties of [div] and [mod]. + - [NProp] adds all generic properties derived from [NAxioms] - [MinMax*Properties] provides properties of [min] and [max]. *) -Module BigN <: NType <: OrderedTypeFull <: TotalOrder := - NMake.Make Int31Cyclic <+ NTypeIsNAxioms - <+ !NPropSig <+ !NDivPropFunct <+ HasEqBool2Dec - <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. +Delimit Scope bigN_scope with bigN. +Module BigN <: NType <: OrderedTypeFull <: TotalOrder. + Include NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope]. + Bind Scope bigN_scope with t t'. + Include NTypeIsNAxioms + <+ NProp [no inline] + <+ HasEqBool2Dec [no inline] + <+ MinMaxLogicalProperties [no inline] + <+ MinMaxDecProperties [no inline]. +End BigN. + +(** Nota concerning scopes : for the first Include, we cannot bind + the scope bigN_scope to a type that doesn't exists yet. + We hence need to explicitely declare the scope substitution. + For the next Include, the abstract type t (in scope abstract_scope) + gets substituted to concrete BigN.t (in scope bigN_scope), + and the corresponding argument scope are fixed automatically. +*) (** Notations about [BigN] *) -Notation bigN := BigN.t. - -Delimit Scope bigN_scope with bigN. -Bind Scope bigN_scope with bigN. -Bind Scope bigN_scope with BigN.t. -Bind Scope bigN_scope with BigN.t_. -(* Bind Scope has no retroactive effect, let's declare scopes by hand. *) -Arguments Scope BigN.to_Z [bigN_scope]. -Arguments Scope BigN.succ [bigN_scope]. -Arguments Scope BigN.pred [bigN_scope]. -Arguments Scope BigN.square [bigN_scope]. -Arguments Scope BigN.add [bigN_scope bigN_scope]. -Arguments Scope BigN.sub [bigN_scope bigN_scope]. -Arguments Scope BigN.mul [bigN_scope bigN_scope]. -Arguments Scope BigN.div [bigN_scope bigN_scope]. -Arguments Scope BigN.eq [bigN_scope bigN_scope]. -Arguments Scope BigN.lt [bigN_scope bigN_scope]. -Arguments Scope BigN.le [bigN_scope bigN_scope]. -Arguments Scope BigN.eq [bigN_scope bigN_scope]. -Arguments Scope BigN.compare [bigN_scope bigN_scope]. -Arguments Scope BigN.min [bigN_scope bigN_scope]. -Arguments Scope BigN.max [bigN_scope bigN_scope]. -Arguments Scope BigN.eq_bool [bigN_scope bigN_scope]. -Arguments Scope BigN.power_pos [bigN_scope positive_scope]. -Arguments Scope BigN.power [bigN_scope N_scope]. -Arguments Scope BigN.sqrt [bigN_scope]. -Arguments Scope BigN.div_eucl [bigN_scope bigN_scope]. -Arguments Scope BigN.modulo [bigN_scope bigN_scope]. -Arguments Scope BigN.gcd [bigN_scope bigN_scope]. +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.power : 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)%bigN (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" := (BigN.lt y x)(only parsing) : bigN_scope. -Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope. -Notation "x < y < z" := (x<y /\ y<z)%bigN : bigN_scope. -Notation "x < y <= z" := (x<y /\ y<=z)%bigN : bigN_scope. -Notation "x <= y < z" := (x<=y /\ y<z)%bigN : bigN_scope. -Notation "x <= y <= z" := (x<=y /\ y<=z)%bigN : 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. -Local Open Scope bigN_scope. - (** Example of reasoning about [BigN] *) Theorem succ_pred: forall q : bigN, @@ -107,29 +97,29 @@ 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, BigN.eq_bool x y = true -> x==y. +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 (@id N) BigN.power. +Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow. Proof. constructor. -intros. red. rewrite BigN.spec_power. unfold id. -destruct Zpower_theory as [EQ]. rewrite EQ. +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 BigN.eq_bool b 0 then (0,a) else BigN.div_eucl a b). + (fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b). Proof. constructor. unfold id. intros a b. BigN.zify. -generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0). +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), Zdiv_eucl as (q',r'). +destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r'). intros (EQ,_). injection 1. intros EQr EQq. BigN.zify. rewrite EQr, EQq; auto. Qed. @@ -163,6 +153,7 @@ Ltac isBigNcst t := end | BigN.zero => constr:true | BigN.one => constr:true + | BigN.two => constr:true | _ => constr:false end. @@ -172,6 +163,12 @@ Ltac BigNcst 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 @@ -183,11 +180,11 @@ Ltac Ncst t := Add Ring BigNr : BigNring (decidable BigNeqb_correct, constants [BigNcst], - power_tac BigNpower [Ncst], + power_tac BigNpower [BigN_to_N], div BigNdiv). Section TestRing. -Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x. +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. diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 2b70f1bb..5012a1b9 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,118 +16,577 @@ representation. The representation-dependent (and macro-generated) part is now in [NMake_gen]. *) -Require Import BigNumPrelude ZArith CyclicAxioms. -Require Import Nbasic Wf_nat StreamMemo NSig NMake_gen. +Require Import Bool BigNumPrelude ZArith Nnat Ndigits CyclicAxioms DoubleType + Nbasic Wf_nat StreamMemo NSig NMake_gen. -Module Make (Import W0:CyclicType) <: NType. +Module Make (W0:CyclicType) <: NType. - (** Macro-generated part *) + (** 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. simpl. + 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 *) - Lemma spec_pred : forall x, [pred x] = Zmax 0 ([x]-1). + 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. destruct (Zle_lt_or_eq _ _ (spec_pos x)). - rewrite Zmax_r; auto with zarith. - apply spec_pred_pos; auto. - rewrite <- H; apply spec_pred0; auto. + 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 *) - Lemma spec_sub : forall x y, [sub x y] = Zmax 0 ([x]-[y]). + 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. destruct (Zle_or_lt [y] [x]). - rewrite Zmax_r; auto with zarith. apply spec_sub_pos; auto. - rewrite Zmax_l; auto with zarith. apply spec_sub0; auto. + 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 *) - Theorem spec_compare : forall x y, compare x y = Zcompare [x] [y]. + 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 _ op in + let compare := @ZnZ.compare _ 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 _ (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. generalize (spec_compare_aux x y); destruct compare; - intros; symmetry; try rewrite Zcompare_Eq_iff_eq; assumption. + 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 eq_bool x y := + Definition eqb (x y : t) : bool := match compare x y with | Eq => true | _ => false end. - Theorem spec_eq_bool : forall x y, eq_bool x y = Zeq_bool [x] [y]. + 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. - intros. unfold eq_bool, Zeq_bool. rewrite spec_compare; reflexivity. + apply eq_iff_eq_true. + rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare. + split; [now destruct Z.compare | now intros ->]. Qed. - Theorem spec_eq_bool_aux: forall x y, - if eq_bool x y then [x] = [y] else [x] <> [y]. + 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. - intros x y; unfold eq_bool. - generalize (spec_compare_aux x y); case compare; auto with zarith. + apply eq_iff_eq_true. + rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. + destruct Z.compare; split; try easy. now destruct 1. Qed. - Definition lt n m := [n] < [m]. - Definition le n m := [n] <= [m]. + 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. - Definition min n m := match compare n m with Gt => m | _ => n end. - Definition max n m := 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_max : forall n m, [max n m] = Zmax [n] [m]. + Theorem spec_min : forall n m, [min n m] = Z.min [n] [m]. Proof. - intros. unfold max, Zmax. rewrite spec_compare; destruct Zcompare; reflexivity. + intros. unfold min, Z.min. rewrite spec_compare; destruct Z.compare; reflexivity. Qed. - Theorem spec_min : forall n m, [min n m] = Zmin [n] [m]. + (** * 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 _ op in + let succ := @ZnZ.succ _ op in + let add_c := @ZnZ.add_c _ op in + let mul_c := @ZnZ.mul_c _ op in + let ww := @ZnZ.WW _ op in + let ow := @ZnZ.OW _ op in + let eq0 := @ZnZ.eq0 _ op 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. - intros. unfold min, Zmin. rewrite spec_compare; destruct Zcompare; reflexivity. + 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. - (** * Power *) + 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. - Fixpoint power_pos (x:t) (p:positive) {struct p} : t := - match p with - | xH => x - | xO p => square (power_pos x p) - | xI p => mul (square (power_pos x p)) x - end. + 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_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. + Theorem spec_mul : forall x y, [mul x y] = [x] * [y]. Proof. - intros x n; generalize x; elim n; clear n x; simpl power_pos. - intros; rewrite spec_mul; rewrite spec_square; rewrite H. - rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith. - rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith. - rewrite Zpower_2; rewrite Zpower_1_r; auto. - intros; rewrite spec_square; rewrite H. - rewrite Zpos_xO; auto with zarith. - rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith. - rewrite Zpower_2; auto. - intros; rewrite Zpower_1_r; auto. + 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. - Definition power x (n:N) := match n with - | BinNat.N0 => one - | BinNat.Npos p => power_pos x p - end. + (** * 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 _ op in + let ww := @ZnZ.WW _ op in + let head0 := @ZnZ.head0 _ op in + let add_mul_div := @ZnZ.add_mul_div _ op in + let div21 := @ZnZ.div21 _ op in + let compare := @ZnZ.compare _ op in + let sub := @ZnZ.sub _ op 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). + + Let 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. - Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n. + Let 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. - destruct n; simpl. apply (spec_1 w0_spec). - apply spec_power_pos. + 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. - (** * Div *) + (** * General Division *) - Definition div_eucl x y := - if eq_bool y zero then (zero,zero) else + 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) @@ -136,49 +595,123 @@ Module Make (Import W0:CyclicType) <: NType. Theorem spec_div_eucl: forall x y, let (q,r) := div_eucl x y in - ([q], [r]) = Zdiv_eucl [x] [y]. + ([q], [r]) = Z.div_eucl [x] [y]. Proof. - assert (F0: [zero] = 0). - exact (spec_0 w0_spec). - assert (F1: [one] = 1). - exact (spec_1 w0_spec). intros x y. unfold div_eucl. - generalize (spec_eq_bool_aux y zero). destruct eq_bool; rewrite F0. - intro H. rewrite H. destruct [x]; auto. - intro H'. - assert (0 < [y]) by (generalize (spec_pos y); auto with zarith). + 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'. - generalize (spec_compare_aux x y); case compare; try rewrite F0; - try rewrite F1; intros; auto with zarith. - rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H)) - (Z_mod_same [y] (Zlt_gt _ _ H)); - unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto. - assert (F2: 0 <= [x] < [y]). - generalize (spec_pos x); auto. - generalize (Zdiv_small _ _ F2) - (Zmod_small _ _ F2); - unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto. - generalize (spec_div_gt _ _ H0 H); auto. - unfold Zdiv, Zmod; case Zdiv_eucl; case div_gt. + 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 := fst (div_eucl x y). + 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 Zdiv; case Zdiv_eucl; intros qq rr H; + 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 _ op in + let head0 := @ZnZ.head0 _ op in + let add_mul_div := @ZnZ.add_mul_div _ op in + let div21 := @ZnZ.div21 _ op in + let compare := @ZnZ.compare _ op in + let sub := @ZnZ.sub _ op 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). + + Let 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. + + Let 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. - (** * Modulo *) + (** * General Modulo *) - Definition modulo x y := - if eq_bool y zero then zero else + Definition modulo (x y : t) : t := + if eqb y zero then zero else match compare x y with | Eq => zero | Lt => x @@ -188,25 +721,130 @@ Module Make (Import W0:CyclicType) <: NType. Theorem spec_modulo: forall x y, [modulo x y] = [x] mod [y]. Proof. - assert (F0: [zero] = 0). - exact (spec_0 w0_spec). - assert (F1: [one] = 1). - exact (spec_1 w0_spec). intros x y. unfold modulo. - generalize (spec_eq_bool_aux y zero). destruct eq_bool; rewrite F0. - intro H; rewrite H. destruct [x]; auto. + 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'. - generalize (spec_compare_aux x y); case compare; try rewrite F0; - try rewrite F1; intros; try split; auto with zarith. - rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith. - apply sym_equal; apply Zmod_small; auto with zarith. + 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. + 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 := @@ -226,19 +864,16 @@ Module Make (Import W0:CyclicType) <: NType. Zis_gcd [a1] [b1] [cont a1 b1]) -> Zis_gcd [a] [b] [gcd_gt_body a b cont]. Proof. - assert (F1: [zero] = 0). - unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto. intros a b cont p H2 H3 H4; unfold gcd_gt_body. - generalize (spec_compare_aux b zero); case compare; try rewrite F1. - intros HH; rewrite HH; apply Zis_gcd_0. + 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; generalize (spec_compare_aux (mod_gt a b) zero); - case compare; try rewrite F1. - intros H6; rewrite <- (Zmult_1_r [b]). + 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 Zplus_0_r. + 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. @@ -253,27 +888,22 @@ Module Make (Import W0:CyclicType) <: NType. rewrite <- spec_mod_gt; auto with zarith. repeat rewrite <- spec_mod_gt; auto with zarith. apply H4; auto with zarith. - apply Zmult_lt_reg_r with 2; auto with zarith. - apply Zle_lt_trans with ([b] + [mod_gt a b]); auto with zarith. - apply Zle_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith. - apply Zplus_le_compat_r. - pattern [b] at 1; rewrite <- (Zmult_1_l [b]). - apply Zmult_le_compat_r; auto with zarith. - case (Zle_lt_or_eq 0 ([a]/[b])); auto with zarith. - intros HH; rewrite (Z_div_mod_eq [a] [b]) in H2; - try rewrite <- HH in H2; auto with zarith. - case (Z_mod_lt [a] [b]); auto with zarith. - rewrite Zmult_comm; rewrite spec_mod_gt; auto with zarith. - rewrite <- Z_div_mod_eq; auto with zarith. - pattern 2 at 2; rewrite <- (Zpower_1_r 2). - rewrite <- Zpower_exp; auto with zarith. - ring_simplify (p - 1 + 1); auto. - case (Zle_lt_or_eq 0 p); auto with zarith. - generalize H3; case p; simpl Zpower; auto with zarith. - intros HH; generalize H3; rewrite <- HH; simpl Zpower; auto with zarith. - Qed. - - Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) {struct p} : t := + 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 @@ -294,7 +924,7 @@ Module Make (Import W0:CyclicType) <: NType. apply Hrec with (Zpos p + n); auto. replace (Zpos p + (Zpos p + n)) with (Zpos (xI p) + n - 1); auto. - rewrite Zpos_xI; ring. + 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. @@ -303,23 +933,18 @@ Module Make (Import W0:CyclicType) <: NType. apply Hrec with (Zpos p + n - 1); auto. replace (Zpos p + (Zpos p + n - 1)) with (Zpos (xO p) + n - 1); auto. - rewrite Zpos_xO; ring. + 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 Zlt_le_trans with (1 := H12). - case (Zle_or_lt 1 n); intros HH. - apply Zpower_le_monotone; auto with zarith. - apply Zle_trans with 0; auto with zarith. - assert (HH1: n - 1 < 0); auto with zarith. - generalize HH1; case (n - 1); auto with zarith. - intros p1 HH2; discriminate. + 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 Zplus_comm; auto. + rewrite Z.add_comm; auto. intros a1 b1 H5 H6; apply H3; auto. replace n with (n + 1 - 1); auto; try ring. Qed. @@ -333,192 +958,699 @@ Module Make (Import W0:CyclicType) <: NType. 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] = Zgcd [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. - apply sym_equal; apply Zis_gcd_gcd; auto with zarith. + 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 Zpower_0_r. + 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 := + 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] = Zgcd [a] [b]. + 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; generalize (spec_compare_aux a b); case compare. - intros HH; rewrite HH; apply sym_equal; apply Zis_gcd_gcd; auto. + unfold gcd. rewrite spec_compare. case Z.compare_spec. + intros HH; rewrite HH; symmetry; apply Zis_gcd_gcd; auto. apply Zis_gcd_refl. - intros; apply trans_equal with (Zgcd [b] [a]). + intros; transitivity (Z.gcd [b] [a]). apply spec_gcd_gt; auto with zarith. apply Zis_gcd_gcd; auto with zarith. - apply Zgcd_is_pos. + apply Z.gcd_nonneg. apply Zis_gcd_sym; apply Zgcd_is_gcd. - intros; apply spec_gcd_gt; auto. + 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 of_N x := + 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. + [of_N x] = Z.of_N x. Proof. intros x; case x. - simpl of_N. - unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto. + simpl of_N. exact spec_0. intros p; exact (spec_of_pos p). Qed. + (** * [head0] and [tail0] - (** * Shift *) + 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]. + *) - Definition shiftr n x := - match compare n (Ndigits x) with - | Lt => unsafe_shiftr n x - | _ => N0 w_0 - end. + 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. - Theorem spec_shiftr: forall n x, - [shiftr n x] = [x] / 2 ^ [n]. - Proof. - intros n x; unfold shiftr; - generalize (spec_compare_aux n (Ndigits x)); case compare; intros H. - apply trans_equal with (1 := spec_0 w0_spec). - apply sym_equal; apply Zdiv_small; rewrite H. - rewrite spec_Ndigits; exact (spec_digits x). - rewrite <- spec_unsafe_shiftr; auto with zarith. - apply trans_equal with (1 := spec_0 w0_spec). - apply sym_equal; apply Zdiv_small. - rewrite spec_Ndigits in H; case (spec_digits x); intros H1 H2. - split; auto. - apply Zlt_le_trans with (1 := H2). - apply Zpower_le_monotone; auto with zarith. - Qed. - - Definition shiftl_aux_body cont n x := - match compare n (head0 x) with - Gt => cont n (double_size x) - | _ => unsafe_shiftl n x + 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 p x cont, + Theorem spec_shiftl_aux_body: forall n x p cont, 2^ Zpos p <= [head0 x] -> (forall x, 2 ^ (Zpos p + 1) <= [head0 x]-> - [cont n x] = [x] * 2 ^ [n]) -> - [shiftl_aux_body cont n x] = [x] * 2 ^ [n]. + [cont x n] = [x] * 2 ^ [n]) -> + [shiftl_aux_body cont x n] = [x] * 2 ^ [n]. Proof. - intros n p x cont H1 H2; unfold shiftl_aux_body. - generalize (spec_compare_aux n (head0 x)); case compare; intros H. + 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 Zplus_comm; rewrite Zpower_exp; auto with zarith. - apply Zle_trans with (2 := spec_double_size_head0 x). - rewrite Zpower_1_r; apply Zmult_le_compat_l; auto with zarith. + 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 n x {struct p} := + Fixpoint shiftl_aux p cont x n := shiftl_aux_body - (fun n x => match p with - | xH => cont n x - | xO p => shiftl_aux p (shiftl_aux p cont) n x - | xI p => shiftl_aux p (shiftl_aux p cont) n x - end) n x. + (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 n x cont, + 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 n x] = [x] * 2 ^ [n]) -> - [shiftl_aux p cont n x] = [x] * 2 ^ [n]. + [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 n x cont H1 H2. + 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 <- Pplus_assoc. - rewrite Zpos_plus_distr; auto. + rewrite <- Pos.add_assoc. + rewrite Pos2Z.inj_add; auto. intros x3 H5; apply H2. - rewrite Zpos_xI. + rewrite Pos2Z.inj_xI. replace (2 * Zpos p + 1 + Zpos q) with (Zpos p + Zpos (p + q + 1)); auto. - repeat rewrite Zpos_plus_distr; ring. + 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 Zle_trans with (2 := H3); auto with zarith. - apply Zpower_le_monotone; auto with zarith. + 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 (Zpos_xO p). + rewrite (Pos2Z.inj_xO p). replace (2 * Zpos p + Zpos q) with (Zpos p + Zpos (p + q)); auto. - repeat rewrite Zpos_plus_distr; ring. + rewrite Pos2Z.inj_add; ring. intros q n x cont H1 H2. apply spec_shiftl_aux_body with (q); auto. - rewrite Zplus_comm; auto. + rewrite Z.add_comm; auto. Qed. - Definition shiftl n x := + Definition shiftl x n := shiftl_aux_body (shiftl_aux_body - (shiftl_aux (digits n) unsafe_shiftl)) n x. + (shiftl_aux (digits n) unsafe_shiftl)) x n. - Theorem spec_shiftl: forall n x, - [shiftl n x] = [x] * 2 ^ [n]. + Theorem spec_shiftl_pow2 : forall x n, + [shiftl x n] = [x] * 2 ^ [n]. Proof. - intros n x; unfold shiftl, shiftl_aux_body. - generalize (spec_compare_aux n (head0 x)); case compare; intros H. + 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). - generalize (spec_compare_aux n (head0 (double_size x))); case compare; intros H1. + 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 Zle_trans with (2 := spec_double_size_head0 (double_size x)). + apply Z.le_trans with (2 := spec_double_size_head0 (double_size x)). replace (2 ^ 1) with (2 * 1). - apply Zmult_le_compat_l; auto with zarith. + apply Z.mul_le_mono_nonneg_l; auto with zarith. generalize (spec_double_size_head0_pos x); auto with zarith. - rewrite Zpower_1_r; ring. + rewrite Z.pow_1_r; ring. intros x1 H2; apply spec_unsafe_shiftl. - apply Zle_trans with (2 := H2). - apply Zle_trans with (2 ^ Zpos (digits n)); auto with zarith. + 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 Zpower_le_monotone; 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. - (** * Zero and One *) + (** Other bitwise operations *) - Theorem spec_0: [zero] = 0. + Definition testbit x n := odd (shiftr x n). + + Lemma spec_testbit: forall x p, testbit x p = Z.testbit [x] [p]. Proof. - exact (spec_0 w0_spec). + intros. unfold testbit. symmetry. + rewrite spec_odd, spec_shiftr. apply Z.testbit_odd. Qed. - Theorem spec_1: [one] = 1. + 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. + + (** TODO : provide efficient versions instead of just converting + from/to N (see with Laurent) *) + + Definition lor x y := of_N (N.lor (to_N x) (to_N y)). + Definition land x y := of_N (N.land (to_N x) (to_N y)). + Definition ldiff x y := of_N (N.ldiff (to_N x) (to_N y)). + Definition lxor x y := of_N (N.lxor (to_N x) (to_N y)). + + Lemma spec_land: forall x y, [land x y] = Z.land [x] [y]. Proof. - exact (spec_1 w0_spec). + intros x y. unfold land. rewrite spec_of_N. unfold to_N. + generalize (spec_pos x), (spec_pos y). + destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2). Qed. + Lemma spec_lor: forall x y, [lor x y] = Z.lor [x] [y]. + Proof. + intros x y. unfold lor. rewrite spec_of_N. unfold to_N. + generalize (spec_pos x), (spec_pos y). + destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2). + Qed. + + Lemma spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y]. + Proof. + intros x y. unfold ldiff. rewrite spec_of_N. unfold to_N. + generalize (spec_pos x), (spec_pos y). + destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2). + Qed. + + Lemma spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y]. + Proof. + intros x y. unfold lxor. rewrite spec_of_N. unfold to_N. + generalize (spec_pos x), (spec_pos y). + destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2). + Qed. End Make. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 67a62c40..278cc8bf 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,100 +8,88 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: NMake_gen.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) +(*S NMake_gen.ml : this file generates NMake_gen.v *) -(*S NMake_gen.ml : this file generates NMake.v *) - -(*s The two parameters that control the generation: *) +(*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 *) -let gen_proof = true (* should we generate proofs ? *) - (*s Some utilities *) -let t = "t" -let c = "N" -let pz n = if n == 0 then "w_0" else "W0" -let rec gen2 n = if n == 0 then "1" else if n == 1 then "2" - else "2 * " ^ (gen2 (n - 1)) -let rec genxO n s = - if n == 0 then s else " (xO" ^ (genxO (n - 1) s) ^ ")" +let rec iter_str n s = if n = 0 then "" else (iter_str (n-1) s) ^ s -(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to - /dev/null, but for being compatible with earlier ocaml and not - relying on system-dependent stuff like open_out "/dev/null", - let's use instead a magical hack *) +let rec iter_str_gen n f = if n < 0 then "" else (iter_str_gen (n-1) f) ^ (f n) -(* Standard printer, with a final newline *) -let pr s = Printf.printf (s^^"\n") -(* Printing to /dev/null *) -let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ()) - : ('a, out_channel, unit) format -> 'a) -(* Proof printer : prints iff gen_proof is true *) -let pp = if gen_proof then pr else pn -(* Printer for admitted parts : prints iff gen_proof is false *) -let pa = if not gen_proof then pr else pn -(* Same as before, but without the final newline *) -let pr0 = Printf.printf -let pp0 = if gen_proof then pr0 else pn +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 "(************************************************************************)"; - pr "(* v * The Coq Proof Assistant / The Coq Development Team *)"; - pr "(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)"; - pr "(* \\VV/ **************************************************************)"; - pr "(* // * This file is distributed under the terms of the *)"; - pr "(* * GNU Lesser General Public License Version 2.1 *)"; - pr "(************************************************************************)"; - pr "(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)"; - pr "(************************************************************************)"; - pr ""; - pr "(** * NMake *)"; - pr ""; - pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)"; - pr ""; - pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)"; - pr ""; - pr "Require Import BigNumPrelude ZArith CyclicAxioms"; - pr " DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic"; - pr " Wf_nat StreamMemo."; - pr ""; - pr "Module Make (Import W0:CyclicType)."; - pr ""; +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 *) +(************************************************************************) - pr " Definition w0 := W0.w."; - for i = 1 to size do - pr " Definition w%i := zn2z w%i." i (i-1) - done; - pr ""; +(** * NMake_gen *) - pr " Definition w0_op := W0.w_op."; - for i = 1 to 3 do - pr " Definition w%i_op := mk_zn2z_op w%i_op." i (i-1) - done; - for i = 4 to size + 3 do - pr " Definition w%i_op := mk_zn2z_op_karatsuba w%i_op." i (i-1) - done; - pr ""; +(** 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_op w' -> znz_op (zn2z w')."; + pr " Variable mk : forall w', ZnZ.Ops w' -> ZnZ.Ops (zn2z w')."; pr ""; - pr " Fixpoint make_op_aux (n:nat) : znz_op (word w%i (S n)):=" size; - pr " match n return znz_op (word w%i (S n)) with" size; + 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_op (word w%i (S (S n1))) with" size; + 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_op (word w%i (S (S (S n2)))) with" size; + 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"; @@ -110,2565 +98,912 @@ let _ = pr ""; pr " End Make_op."; pr ""; - pr " Definition omake_op := make_op_aux mk_zn2z_op_karatsuba."; + pr " Definition omake_op := make_op_aux mk_zn2z_ops_karatsuba."; pr ""; pr ""; pr " Definition make_op_list := dmemo_list _ omake_op."; pr ""; - pr " Definition make_op n := dmemo_get _ omake_op n make_op_list."; - pr ""; - pr " Lemma make_op_omake: forall n, make_op n = omake_op n."; - pr " intros n; unfold make_op, make_op_list."; - pr " refine (dmemo_get_correct _ _ _)."; - pr " Qed."; + pr " Instance make_op n : ZnZ.Ops (word w%i (S n))" size; + pr " := dmemo_get _ omake_op n make_op_list."; pr ""; - pr " Inductive %s_ :=" t; - for i = 0 to size do - pr " | %s%i : w%i -> %s_" c i i t - done; - pr " | %sn : forall n, word w%i (S n) -> %s_." c size t; - pr ""; - pr " Definition %s := %s_." t t; - pr ""; - pr " Definition w_0 := w0_op.(znz_0)."; - pr ""; +pr " Ltac unfold_ops := unfold omake_op, make_op_aux, w%i_op, w%i_op." (size+3) (size+2); - for i = 0 to size do - pr " Definition one%i := w%i_op.(znz_1)." i i - done; - pr ""; +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. - pr " Definition zero := %s0 w_0." c; - pr " Definition one := %s0 one0." c; - pr ""; + (** * The main type [t], isomorphic with [exists n, word w0 n] *) +"; - pr " Definition to_Z x :="; - pr " match x with"; + pr " Inductive t' :="; for i = 0 to size do - pr " | %s%i wx => w%i_op.(znz_to_Z) wx" c i i + pr " | N%i : w%i -> t'" i i done; - pr " | %sn n wx => (make_op n).(znz_to_Z) wx" c; - pr " end."; + pr " | Nn : forall n, word w%i (S n) -> t'." size; pr ""; - - pr " Open Scope Z_scope."; - pr " Notation \"[ x ]\" := (to_Z x)."; - pr ""; - - pr " Definition to_N x := Zabs_N (to_Z x)."; + pr " Definition t := t'."; pr ""; - - pr " Definition eq x y := (to_Z x = to_Z y)."; - pr ""; - - pp " (* Regular make op (no karatsuba) *)"; - pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) :"; - pp " znz_op (word ww n) :="; - pp " match n return znz_op (word ww n) with"; - pp " O => ww_op"; - pp " | S n1 => mk_zn2z_op (nmake_op ww ww_op n1)"; - pp " end."; - pp ""; - pp " (* Simplification by rewriting for nmake_op *)"; - pp " Theorem nmake_op_S: forall ww (w_op: znz_op ww) x,"; - pp " nmake_op _ w_op (S x) = mk_zn2z_op (nmake_op _ w_op x)."; - pp " auto."; - pp " Qed."; - pp ""; - - - pr " (* Eval and extend functions for each level *)"; - for i = 0 to size do - pp " Let nmake_op%i := nmake_op _ w%i_op." i i; - pp " Let eval%in n := znz_to_Z (nmake_op%i n)." i i; - if i == 0 then - pr " Let extend%i := DoubleBase.extend (WW w_0)." i - else - pr " Let extend%i := DoubleBase.extend (WW (W0: w%i))." i i; - done; + pr " Bind Scope abstract_scope with t t'."; pr ""; - - pp " Theorem digits_doubled:forall n ww (w_op: znz_op ww),"; - pp " znz_digits (nmake_op _ w_op n) ="; - pp " DoubleBase.double_digits (znz_digits w_op) n."; - pp " Proof."; - pp " intros n; elim n; auto; clear n."; - pp " intros n Hrec ww ww_op; simpl DoubleBase.double_digits."; - pp " rewrite <- Hrec; auto."; - pp " Qed."; - pp ""; - pp " Theorem nmake_double: forall n ww (w_op: znz_op ww),"; - pp " znz_to_Z (nmake_op _ w_op n) ="; - pp " @DoubleBase.double_to_Z _ (znz_digits w_op) (znz_to_Z w_op) n."; - pp " Proof."; - pp " intros n; elim n; auto; clear n."; - pp " intros n Hrec ww ww_op; simpl DoubleBase.double_to_Z; unfold zn2z_to_Z."; - pp " rewrite <- Hrec; auto."; - pp " unfold DoubleBase.double_wB; rewrite <- digits_doubled; auto."; - pp " Qed."; - pp ""; - - - pp " Theorem digits_nmake:forall n ww (w_op: znz_op ww),"; - pp " znz_digits (nmake_op _ w_op (S n)) ="; - pp " xO (znz_digits (nmake_op _ w_op n))."; - pp " Proof."; - pp " auto."; - pp " Qed."; - pp ""; - - - pp " Theorem znz_nmake_op: forall ww ww_op n xh xl,"; - pp " znz_to_Z (nmake_op ww ww_op (S n)) (WW xh xl) ="; - pp " znz_to_Z (nmake_op ww ww_op n) xh *"; - pp " base (znz_digits (nmake_op ww ww_op n)) +"; - pp " znz_to_Z (nmake_op ww ww_op n) xl."; - pp " Proof."; - pp " auto."; - pp " Qed."; - pp ""; - - pp " Theorem make_op_S: forall n,"; - pp " make_op (S n) = mk_zn2z_op_karatsuba (make_op n)."; - pp " intro n."; - pp " do 2 rewrite make_op_omake."; - pp " pattern n; apply lt_wf_ind; clear n."; - pp " intros n; case n; clear n."; - pp " intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 2); - pp " intros n; case n; clear n."; - pp " intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 3); - pp " intros n; case n; clear n."; - pp " intros _; unfold omake_op, make_op_aux, w%i_op, w%i_op; apply refl_equal." (size + 3) (size + 2); - pp " intros n Hrec."; - pp " change (omake_op (S (S (S (S n))))) with"; - pp " (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (omake_op (S n)))))."; - pp " change (omake_op (S (S (S n)))) with"; - pp " (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (omake_op n))))."; - pp " rewrite Hrec; auto with arith."; - pp " Qed."; - pp ""; - - - for i = 1 to size + 2 do - pp " Let znz_to_Z_%i: forall x y," i; - pp " znz_to_Z w%i_op (WW x y) =" i; - pp " znz_to_Z w%i_op x * base (znz_digits w%i_op) + znz_to_Z w%i_op y." (i-1) (i-1) (i-1); - pp " Proof."; - pp " auto."; - pp " Qed."; - pp ""; - done; - - pp " Let znz_to_Z_n: forall n x y,"; - pp " znz_to_Z (make_op (S n)) (WW x y) ="; - pp " znz_to_Z (make_op n) x * base (znz_digits (make_op n)) + znz_to_Z (make_op n) y."; - pp " Proof."; - pp " intros n x y; rewrite make_op_S; auto."; - pp " Qed."; - pp ""; - - pp " Let w0_spec: znz_spec w0_op := W0.w_spec."; - for i = 1 to 3 do - pp " Let w%i_spec: znz_spec w%i_op := mk_znz2_spec w%i_spec." i i (i-1) - done; - for i = 4 to size + 3 do - pp " Let w%i_spec : znz_spec w%i_op := mk_znz2_karatsuba_spec w%i_spec." i i (i-1) - done; - pp ""; - - pp " Let wn_spec: forall n, znz_spec (make_op n)."; - pp " intros n; elim n; clear n."; - pp " exact w%i_spec." (size + 1); - pp " intros n Hrec; rewrite make_op_S."; - pp " exact (mk_znz2_karatsuba_spec Hrec)."; - pp " Qed."; - pp ""; - - for i = 0 to size do - pr " Definition w%i_eq0 := w%i_op.(znz_eq0)." i i; - pr " Let spec_w%i_eq0: forall x, if w%i_eq0 x then [%s%i x] = 0 else True." i i c i; - pa " Admitted."; - pp " Proof."; - pp " intros x; unfold w%i_eq0, to_Z; generalize (spec_eq0 w%i_spec x);" i i; - pp " case znz_eq0; auto."; - pp " Qed."; - pr ""; - done; + pr " (** * A generic toolbox for building and deconstructing [t] *)"; pr ""; - - for i = 0 to size do - pp " Theorem digits_w%i: znz_digits w%i_op = znz_digits (nmake_op _ w0_op %i)." i i i; - if i == 0 then - pp " auto." - else - pp " rewrite digits_nmake; rewrite <- digits_w%i; auto." (i - 1); - pp " Qed."; - pp ""; - pp " Let spec_double_eval%in: forall n, eval%in n = DoubleBase.double_to_Z (znz_digits w%i_op) (znz_to_Z w%i_op) n." i i i i; - pp " Proof."; - pp " intros n; exact (nmake_double n w%i w%i_op)." i i; - pp " Qed."; - pp ""; - done; - - for i = 0 to size do - for j = 0 to (size - i) do - pp " Theorem digits_w%in%i: znz_digits w%i_op = znz_digits (nmake_op _ w%i_op %i)." i j (i + j) i j; - pp " Proof."; - if j == 0 then - if i == 0 then - pp " auto." - else - begin - pp " apply trans_equal with (xO (znz_digits w%i_op))." (i + j -1); - pp " auto."; - pp " unfold nmake_op; auto."; - end - else - begin - pp " apply trans_equal with (xO (znz_digits w%i_op))." (i + j -1); - pp " auto."; - pp " rewrite digits_nmake."; - pp " rewrite digits_w%in%i." i (j - 1); - pp " auto."; - end; - pp " Qed."; - pp ""; - pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j; - pp " Proof."; - if j == 0 then - pp " intros x; rewrite spec_double_eval%in; unfold DoubleBase.double_to_Z, to_Z; auto." i - else - begin - pp " intros x; case x."; - pp " auto."; - pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (i + j); - pp " rewrite digits_w%in%i." i (j - 1); - pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (j - 1); - pp " unfold eval%in, nmake_op%i." i i; - pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (j - 1); - end; - pp " Qed."; - if i + j <> size then - begin - pp " Let spec_extend%in%i: forall x, [%s%i x] = [%s%i (extend%i %i x)]." i (i + j + 1) c i c (i + j + 1) i j; - if j == 0 then - begin - pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." i (i + j); - pp " unfold to_Z; rewrite znz_to_Z_%i." (i + j + 1); - pp " rewrite (spec_0 w%i_spec); auto." (i + j); - end - else - begin - pp " intros x; change (extend%i %i x) with (WW (znz_0 w%i_op) (extend%i %i x))." i j (i + j) i (j - 1); - pp " unfold to_Z; rewrite znz_to_Z_%i." (i + j + 1); - pp " rewrite (spec_0 w%i_spec)." (i + j); - pp " generalize (spec_extend%in%i x); unfold to_Z." i (i + j); - pp " intros HH; rewrite <- HH; auto."; - end; - pp " Qed."; - pp ""; - end; - done; - - pp " Theorem digits_w%in%i: znz_digits w%i_op = znz_digits (nmake_op _ w%i_op %i)." i (size - i + 1) (size + 1) i (size - i + 1); - pp " Proof."; - pp " apply trans_equal with (xO (znz_digits w%i_op))." size; - pp " auto."; - pp " rewrite digits_nmake."; - pp " rewrite digits_w%in%i." i (size - i); - pp " auto."; - pp " Qed."; - pp ""; - - pp " Let spec_eval%in%i: forall x, [%sn 0 x] = eval%in %i x." i (size - i + 1) c i (size - i + 1); - pp " Proof."; - pp " intros x; case x."; - pp " auto."; - pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 1); - pp " rewrite digits_w%in%i." i (size - i); - pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (size - i); - pp " unfold eval%in, nmake_op%i." i i; - pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size - i); - pp " Qed."; - pp ""; - - pp " Let spec_eval%in%i: forall x, [%sn 1 x] = eval%in %i x." i (size - i + 2) c i (size - i + 2); - pp " intros x; case x."; - pp " auto."; - pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 2); - pp " rewrite digits_w%in%i." i (size + 1 - i); - pp " generalize (spec_eval%in%i); unfold to_Z; change (make_op 0) with (w%i_op); intros HH; repeat rewrite HH." i (size + 1 - i) (size + 1); - pp " unfold eval%in, nmake_op%i." i i; - pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size + 1 - i); - pp " Qed."; - pp ""; - done; - - pp " Let digits_w%in: forall n," size; - pp " znz_digits (make_op n) = znz_digits (nmake_op _ w%i_op (S n))." size; - pp " intros n; elim n; clear n."; - pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size; - pp " rewrite nmake_op_S; apply sym_equal; auto."; - pp " intros n Hrec."; - pp " replace (znz_digits (make_op (S n))) with (xO (znz_digits (make_op n)))."; - pp " rewrite Hrec."; - pp " rewrite nmake_op_S; apply sym_equal; auto."; - pp " rewrite make_op_S; apply sym_equal; auto."; - pp " Qed."; - pp ""; - - pp " Let spec_eval%in: forall n x, [%sn n x] = eval%in (S n) x." size c size; - pp " intros n; elim n; clear n."; - pp " exact spec_eval%in1." size; - pp " intros n Hrec x; case x; clear x."; - pp " unfold to_Z, eval%in, nmake_op%i." size size; - pp " rewrite make_op_S; rewrite nmake_op_S; auto."; - pp " intros xh xl."; - pp " unfold to_Z in Hrec |- *."; - pp " rewrite znz_to_Z_n."; - pp " rewrite digits_w%in." size; - pp " repeat rewrite Hrec."; - pp " unfold eval%in, nmake_op%i." size size; - pp " apply sym_equal; rewrite nmake_op_S; auto."; - pp " Qed."; - pp ""; - - pp " Let spec_extend%in: forall n x, [%s%i x] = [%sn n (extend%i n x)]." size c size c size ; - pp " intros n; elim n; clear n."; - pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." size size; - pp " unfold to_Z."; - pp " change (make_op 0) with w%i_op." (size + 1); - pp " rewrite znz_to_Z_%i; rewrite (spec_0 w%i_spec); auto." (size + 1) size; - pp " intros n Hrec x."; - pp " change (extend%i (S n) x) with (WW W0 (extend%i n x))." size size; - pp " unfold to_Z in Hrec |- *; rewrite znz_to_Z_n; auto."; - pp " rewrite <- Hrec."; - pp " replace (znz_to_Z (make_op n) W0) with 0; auto."; - pp " case n; auto; intros; rewrite make_op_S; auto."; - pp " Qed."; - pp ""; - - pr " Theorem spec_pos: forall x, 0 <= [x]."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; clear x."; - for i = 0 to size do - pp " intros x; case (spec_to_Z w%i_spec x); auto." i; - done; - pp " intros n x; case (spec_to_Z (wn_spec n) x); auto."; - pp " Qed."; + pr " Local Notation SizePlus n := %sn%s." + (iter_str size "(S ") (iter_str size ")"); + pr " Local Notation Size := (SizePlus O)."; pr ""; - pp " Let spec_extendn_0: forall n wx, [%sn n (extend n _ wx)] = [%sn 0 wx]." c c; - pp " intros n; elim n; auto."; - pp " intros n1 Hrec wx; simpl extend; rewrite <- Hrec; auto."; - pp " unfold to_Z."; - pp " case n1; auto; intros n2; repeat rewrite make_op_S; auto."; - pp " Qed."; - pp ""; - pp " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx]." c c; - pp " Proof."; - pp " intros n x; unfold to_Z."; - pp " rewrite znz_to_Z_n."; - pp " rewrite <- (Zplus_0_l (znz_to_Z (make_op n) x))."; - pp " apply (f_equal2 Zplus); auto."; - pp " case n; auto."; - pp " intros n1; rewrite make_op_S; auto."; - pp " Qed."; - pp ""; - pp " Let spec_extend_tr: forall m n (w: word _ (S n)),"; - pp " [%sn (m + n) (extend_tr w m)] = [%sn n w]." c c; - pp " Proof."; - pp " induction m; auto."; - pp " intros n x; simpl extend_tr."; - pp " simpl plus; rewrite spec_extendn0_0; auto."; - pp " Qed."; - pp ""; - pp " Let spec_cast_l: forall n m x1,"; - pp " [%sn (Max.max n m)" c; - pp " (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))] ="; - pp " [%sn n x1]." c; - pp " Proof."; - pp " intros n m x1; case (diff_r n m); simpl castm."; - pp " rewrite spec_extend_tr; auto."; - pp " Qed."; - pp ""; - pp " Let spec_cast_r: forall n m x1,"; - pp " [%sn (Max.max n m)" c; - pp " (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))] ="; - pp " [%sn m x1]." c; - pp " Proof."; - pp " intros n m x1; case (diff_l n m); simpl castm."; - pp " rewrite spec_extend_tr; auto."; - pp " Qed."; - pp ""; - - - pr " Section LevelAndIter."; - pr ""; - pr " Variable res: Type."; - pr " Variable xxx: res."; - pr " Variable P: Z -> Z -> res -> Prop."; - pr " (* Abstraction function for each level *)"; - for i = 0 to size do - pr " Variable f%i: w%i -> w%i -> res." i i i; - pr " Variable f%in: forall n, w%i -> word w%i (S n) -> res." i i i; - pr " Variable fn%i: forall n, word w%i (S n) -> w%i -> res." i i i; - pp " Variable Pf%i: forall x y, P [%s%i x] [%s%i y] (f%i x y)." i c i c i i; - if i == size then - begin - pp " Variable Pf%in: forall n x y, P [%s%i x] (eval%in (S n) y) (f%in n x y)." i c i i i; - pp " Variable Pfn%i: forall n x y, P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i i c i i; - end - else - begin - pp " Variable Pf%in: forall n x y, Z_of_nat n <= %i -> P [%s%i x] (eval%in (S n) y) (f%in n x y)." i (size - i) c i i i; - pp " Variable Pfn%i: forall n x y, Z_of_nat n <= %i -> P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i (size - i) i c i i; - end; - pr ""; - done; - pr " Variable fnn: forall n, word w%i (S n) -> word w%i (S n) -> res." size size; - pp " Variable Pfnn: forall n x y, P [%sn n x] [%sn n y] (fnn n x y)." c c; - pr " Variable fnm: forall n m, word w%i (S n) -> word w%i (S m) -> res." size size; - pp " Variable Pfnm: forall n m x y, P [%sn n x] [%sn m y] (fnm n m x y)." c c; - pr ""; - pr " (* Special zero functions *)"; - pr " Variable f0t: t_ -> res."; - pp " Variable Pf0t: forall x, P 0 [x] (f0t x)."; - pr " Variable ft0: t_ -> res."; - pp " Variable Pft0: forall x, P [x] 0 (ft0 x)."; + pr " Tactic Notation \"do_size\" tactic(t) := do %i t." (size+1); pr ""; - - pr " (* We level the two arguments before applying *)"; - pr " (* the functions at each leval *)"; - pr " Definition same_level (x y: t_): res :="; - pr0 " Eval lazy zeta beta iota delta ["; - for i = 0 to size do - pr0 "extend%i " i; - done; - pr ""; - pr " DoubleBase.extend DoubleBase.extend_aux"; - pr " ] in"; - pr " match x, y with"; + pr " Definition dom_t n := match n with"; for i = 0 to size do - for j = 0 to i - 1 do - pr " | %s%i wx, %s%i wy => f%i wx (extend%i %i wy)" c i c j i j (i - j -1); - done; - pr " | %s%i wx, %s%i wy => f%i wx wy" c i c i i; - for j = i + 1 to size do - pr " | %s%i wx, %s%i wy => f%i (extend%i %i wx) wy" c i c j j i (j - i - 1); - done; - if i == size then - pr " | %s%i wx, %sn m wy => fnn m (extend%i m wx) wy" c size c size - else - pr " | %s%i wx, %sn m wy => fnn m (extend%i m (extend%i %i wx)) wy" c i c size i (size - i - 1); + pr " | %i => w%i" i i; done; - for i = 0 to size do - if i == size then - pr " | %sn n wx, %s%i wy => fnn n wx (extend%i n wy)" c c size size - else - pr " | %sn n wx, %s%i wy => fnn n wx (extend%i n (extend%i %i wy))" c c i size i (size - i - 1); - done; - pr " | %sn n wx, Nn m wy =>" c; - pr " let mn := Max.max n m in"; - pr " let d := diff n m in"; - pr " fnn mn"; - pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; - pr " (castm (diff_l n m) (extend_tr wy (fst d)))"; - pr " end."; + pr " | %sn => word w%i n" (if size=0 then "" else "SizePlus ") size; + pr " end."; pr ""; - pp " Lemma spec_same_level: forall x y, P [x] [y] (same_level x y)."; - pp " Proof."; - pp " intros x; case x; clear x; unfold same_level."; - for i = 0 to size do - pp " intros x y; case y; clear y."; - for j = 0 to i - 1 do - pp " intros y; rewrite spec_extend%in%i; apply Pf%i." j i i; - done; - pp " intros y; apply Pf%i." i; - for j = i + 1 to size do - pp " intros y; rewrite spec_extend%in%i; apply Pf%i." i j j; - done; - if i == size then - pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size - else - pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size; - done; - pp " intros n x y; case y; clear y."; - for i = 0 to size do - if i == size then - pp " intros y; rewrite (spec_extend%in n); apply Pfnn." size - else - pp " intros y; rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size; - done; - pp " intros m y; rewrite <- (spec_cast_l n m x);"; - pp " rewrite <- (spec_cast_r n m y); apply Pfnn."; - pp " Qed."; - pp ""; - - pr " (* We level the two arguments before applying *)"; - pr " (* the functions at each level (special zero case) *)"; - pr " Definition same_level0 (x y: t_): res :="; - pr0 " Eval lazy zeta beta iota delta ["; - for i = 0 to size do - pr0 "extend%i " i; - done; - pr ""; - pr " DoubleBase.extend DoubleBase.extend_aux"; - pr " ] in"; - pr " match x with"; - for i = 0 to size do - pr " | %s%i wx =>" c i; - if i == 0 then - pr " if w0_eq0 wx then f0t y else"; - pr " match y with"; - for j = 0 to i - 1 do - pr " | %s%i wy =>" c j; - if j == 0 then - pr " if w0_eq0 wy then ft0 x else"; - pr " f%i wx (extend%i %i wy)" i j (i - j -1); - done; - pr " | %s%i wy => f%i wx wy" c i i; - for j = i + 1 to size do - pr " | %s%i wy => f%i (extend%i %i wx) wy" c j j i (j - i - 1); - done; - if i == size then - pr " | %sn m wy => fnn m (extend%i m wx) wy" c size - else - pr " | %sn m wy => fnn m (extend%i m (extend%i %i wx)) wy" c size i (size - i - 1); - pr" end"; - done; - pr " | %sn n wx =>" c; - pr " match y with"; - for i = 0 to size do - pr " | %s%i wy =>" c i; - if i == 0 then - pr " if w0_eq0 wy then ft0 x else"; - if i == size then - pr " fnn n wx (extend%i n wy)" size - else - pr " fnn n wx (extend%i n (extend%i %i wy))" size i (size - i - 1); - done; - pr " | %sn m wy =>" c; - pr " let mn := Max.max n m in"; - pr " let d := diff n m in"; - pr " fnn mn"; - pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; - pr " (castm (diff_l n m) (extend_tr wy (fst d)))"; - pr " end"; - 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. +"; - pp " Lemma spec_same_level0: forall x y, P [x] [y] (same_level0 x y)."; - pp " Proof."; - pp " intros x; case x; clear x; unfold same_level0."; - for i = 0 to size do - pp " intros x."; - if i == 0 then - begin - pp " generalize (spec_w0_eq0 x); case w0_eq0; intros H."; - pp " intros y; rewrite H; apply Pf0t."; - pp " clear H."; - end; - pp " intros y; case y; clear y."; - for j = 0 to i - 1 do - pp " intros y."; - if j == 0 then - begin - pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; - pp " rewrite H; apply Pft0."; - pp " clear H."; - end; - pp " rewrite spec_extend%in%i; apply Pf%i." j i i; - done; - pp " intros y; apply Pf%i." i; - for j = i + 1 to size do - pp " intros y; rewrite spec_extend%in%i; apply Pf%i." i j j; - done; - if i == size then - pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size - else - pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size; - done; - pp " intros n x y; case y; clear y."; + pr " Definition iter_t {A:Type}(f : forall n, dom_t n -> A) : t -> A :="; for i = 0 to size do - pp " intros y."; - if i = 0 then - begin - pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; - pp " rewrite H; apply Pft0."; - pp " clear H."; - end; - if i == size then - pp " rewrite (spec_extend%in n); apply Pfnn." size - else - pp " rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size; + pr " let f%i := f %i in" i i; done; - pp " intros m y; rewrite <- (spec_cast_l n m x);"; - pp " rewrite <- (spec_cast_r n m y); apply Pfnn."; - pp " Qed."; - pp ""; - - pr " (* We iter the smaller argument with the bigger *)"; - pr " Definition iter (x y: t_): res :="; - pr0 " Eval lazy zeta beta iota delta ["; + pr " let fn n := f (SizePlus (S n)) in"; + pr " fun x => match x with"; for i = 0 to size do - pr0 "extend%i " i; + pr " | N%i wx => f%i wx" i i; done; - pr ""; - pr " DoubleBase.extend DoubleBase.extend_aux"; - pr " ] in"; - pr " match x, y with"; - for i = 0 to size do - for j = 0 to i - 1 do - pr " | %s%i wx, %s%i wy => fn%i %i wx wy" c i c j j (i - j - 1); - done; - pr " | %s%i wx, %s%i wy => f%i wx wy" c i c i i; - for j = i + 1 to size do - pr " | %s%i wx, %s%i wy => f%in %i wx wy" c i c j i (j - i - 1); - done; - if i == size then - pr " | %s%i wx, %sn m wy => f%in m wx wy" c size c size - else - pr " | %s%i wx, %sn m wy => f%in m (extend%i %i wx) wy" c i c size i (size - i - 1); - done; - for i = 0 to size do - if i == size then - pr " | %sn n wx, %s%i wy => fn%i n wx wy" c c size size - else - pr " | %sn n wx, %s%i wy => fn%i n wx (extend%i %i wy)" c c i size i (size - i - 1); - done; - pr " | %sn n wx, %sn m wy => fnm n m wx wy" c c; + pr " | Nn n wx => fn n wx"; pr " end."; pr ""; - pp " Ltac zg_tac := try"; - pp " (red; simpl Zcompare; auto;"; - pp " let t := fresh \"H\" in (intros t; discriminate t))."; - pp ""; - pp " Lemma spec_iter: forall x y, P [x] [y] (iter x y)."; - pp " Proof."; - pp " intros x; case x; clear x; unfold iter."; - for i = 0 to size do - pp " intros x y; case y; clear y."; - for j = 0 to i - 1 do - pp " intros y; rewrite spec_eval%in%i; apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1); - done; - pp " intros y; apply Pf%i." i; - for j = i + 1 to size do - pp " intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1); - done; - if i == size then - pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size - else - pp " intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size; - done; - pp " intros n x y; case y; clear y."; - for i = 0 to size do - if i == size then - pp " intros y; rewrite spec_eval%in; apply Pfn%i." size size - else - pp " intros y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size; - done; - pp " intros m y; apply Pfnm."; - pp " Qed."; - pp ""; - - - pr " (* We iter the smaller argument with the bigger (zero case) *)"; - pr " Definition iter0 (x y: t_): res :="; - pr0 " Eval lazy zeta beta iota delta ["; - for i = 0 to size do - pr0 "extend%i " i; - done; - pr ""; - pr " DoubleBase.extend DoubleBase.extend_aux"; - pr " ] in"; - pr " match x with"; - for i = 0 to size do - pr " | %s%i wx =>" c i; - if i == 0 then - pr " if w0_eq0 wx then f0t y else"; - pr " match y with"; - for j = 0 to i - 1 do - pr " | %s%i wy =>" c j; - if j == 0 then - pr " if w0_eq0 wy then ft0 x else"; - pr " fn%i %i wx wy" j (i - j - 1); - done; - pr " | %s%i wy => f%i wx wy" c i i; - for j = i + 1 to size do - pr " | %s%i wy => f%in %i wx wy" c j i (j - i - 1); - done; - if i == size then - pr " | %sn m wy => f%in m wx wy" c size - else - pr " | %sn m wy => f%in m (extend%i %i wx) wy" c size i (size - i - 1); - pr " end"; - done; - pr " | %sn n wx =>" c; - pr " match y with"; + 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 " | %s%i wy =>" c i; - if i == 0 then - pr " if w0_eq0 wy then ft0 x else"; - if i == size then - pr " fn%i n wx wy" size - else - pr " fn%i n wx (extend%i %i wy)" size i (size - i - 1); + pr " | %i => N%i" i i; done; - pr " | %sn m wy => fnm n m wx wy" c; - pr " end"; + pr " | %s(S n) => Nn n" (if size=0 then "" else "SizePlus "); pr " end."; pr ""; - pp " Lemma spec_iter0: forall x y, P [x] [y] (iter0 x y)."; - pp " Proof."; - pp " intros x; case x; clear x; unfold iter0."; - for i = 0 to size do - pp " intros x."; - if i == 0 then - begin - pp " generalize (spec_w0_eq0 x); case w0_eq0; intros H."; - pp " intros y; rewrite H; apply Pf0t."; - pp " clear H."; - end; - pp " intros y; case y; clear y."; - for j = 0 to i - 1 do - pp " intros y."; - if j == 0 then - begin - pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; - pp " rewrite H; apply Pft0."; - pp " clear H."; - end; - pp " rewrite spec_eval%in%i; apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1); - done; - pp " intros y; apply Pf%i." i; - for j = i + 1 to size do - pp " intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1); - done; - if i == size then - pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size - else - pp " intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size; - done; - pp " intros n x y; case y; clear y."; - for i = 0 to size do - pp " intros y."; - if i = 0 then - begin - pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; - pp " rewrite H; apply Pft0."; - pp " clear H."; - end; - if i == size then - pp " rewrite spec_eval%in; apply Pfn%i." size size - else - pp " rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size; - done; - pp " intros m y; apply Pfnm."; - pp " Qed."; - pp ""; - - - pr " End LevelAndIter."; - 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. + + Let 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; [exact ZnZ.spec_0|]). + destruct n; auto. simpl. rewrite make_op_S. exact ZnZ.spec_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 +" Let 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 +" Let 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 " (***************************************************************)"; - pr " (* *)"; - pr " (** * Reduction *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - pr " Definition reduce_0 (x:w) := %s0 x." c; - pr " Definition reduce_1 :="; - pr " Eval lazy beta iota delta[reduce_n1] in"; - pr " reduce_n1 _ _ zero w0_eq0 %s0 %s1." c c; - for i = 2 to size do - pr " Definition reduce_%i :=" i; - pr " Eval lazy beta iota delta[reduce_n1] in"; - pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i %s%i." - (i-1) (i-1) c i - done; pr " Definition reduce_%i :=" (size+1); - pr " Eval lazy beta iota delta[reduce_n1] in"; - pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i (%sn 0)." - size size c; + 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 _ _ zero reduce_%i %sn n." (size + 1) c; - pr ""; - - pp " Let spec_reduce_0: forall x, [reduce_0 x] = [%s0 x]." c; - pp " Proof."; - pp " intros x; unfold to_Z, reduce_0."; - pp " auto."; - pp " Qed."; - pp ""; - - for i = 1 to size + 1 do - if i == size + 1 then - pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%sn 0 x]." i i c - else - pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%s%i x]." i i c i; - pp " Proof."; - pp " intros x; case x; unfold reduce_%i." i; - pp " exact (spec_0 w0_spec)."; - pp " intros x1 y1."; - pp " generalize (spec_w%i_eq0 x1);" (i - 1); - pp " case w%i_eq0; intros H1; auto." (i - 1); - if i <> 1 then - pp " rewrite spec_reduce_%i." (i - 1); - pp " unfold to_Z; rewrite znz_to_Z_%i." i; - pp " unfold to_Z in H1; rewrite H1; auto."; - pp " Qed."; - pp ""; - done; - - pp " Let spec_reduce_n: forall n x, [reduce_n n x] = [%sn n x]." c; - pp " Proof."; - pp " intros n; elim n; simpl reduce_n."; - pp " intros x; rewrite <- spec_reduce_%i; auto." (size + 1); - pp " intros n1 Hrec x; case x."; - pp " unfold to_Z; rewrite make_op_S; auto."; - pp " exact (spec_0 w0_spec)."; - pp " intros x1 y1; case x1; auto."; - pp " rewrite Hrec."; - pp " rewrite spec_extendn0_0; auto."; - pp " Qed."; - pp ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Successor *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_succ_c := w%i_op.(znz_succ_c)." i i - done; - pr ""; - - for i = 0 to size do - pr " Definition w%i_succ := w%i_op.(znz_succ)." i i - done; - pr ""; - - pr " Definition succ x :="; - pr " match x with"; - for i = 0 to size-1 do - pr " | %s%i wx =>" c i; - pr " match w%i_succ_c wx with" i; - pr " | C0 r => %s%i r" c i; - pr " | C1 r => %s%i (WW one%i r)" c (i+1) i; - pr " end"; - done; - pr " | %s%i wx =>" c size; - pr " match w%i_succ_c wx with" size; - pr " | C0 r => %s%i r" c size; - pr " | C1 r => %sn 0 (WW one%i r)" c size ; - pr " end"; - pr " | %sn n wx =>" c; - pr " let op := make_op n in"; - pr " match op.(znz_succ_c) wx with"; - pr " | C0 r => %sn n r" c; - pr " | C1 r => %sn (S n) (WW op.(znz_1) r)" c; - pr " end"; - pr " end."; - pr ""; - - pr " Theorem spec_succ: forall n, [succ n] = [n] + 1."; - pa " Admitted."; - pp " Proof."; - pp " intros n; case n; unfold succ, to_Z."; - for i = 0 to size do - pp " intros n1; generalize (spec_succ_c w%i_spec n1);" i; - pp " unfold succ, to_Z, w%i_succ_c; case znz_succ_c; auto." i; - pp " intros ww H; rewrite <- H."; - pp " (rewrite znz_to_Z_%i; unfold interp_carry;" (i + 1); - pp " apply f_equal2 with (f := Zplus); auto;"; - pp " apply f_equal2 with (f := Zmult); auto;"; - pp " exact (spec_1 w%i_spec))." i; - done; - pp " intros k n1; generalize (spec_succ_c (wn_spec k) n1)."; - pp " unfold succ, to_Z; case znz_succ_c; auto."; - pp " intros ww H; rewrite <- H."; - pp " (rewrite (znz_to_Z_n k); unfold interp_carry;"; - pp " apply f_equal2 with (f := Zplus); auto;"; - pp " apply f_equal2 with (f := Zmult); auto;"; - pp " exact (spec_1 (wn_spec k)))."; - pp " Qed."; - pr ""; - - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Adddition *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_add_c := znz_add_c w%i_op." i i; - pr " Definition w%i_add x y :=" i; - pr " match w%i_add_c x y with" i; - pr " | C0 r => %s%i r" c i; - if i == size then - pr " | C1 r => %sn 0 (WW one%i r)" c size - else - pr " | C1 r => %s%i (WW one%i r)" c (i + 1) i; - pr " end."; - pr ""; - done ; - pr " Definition addn n (x y : word w%i (S n)) :=" size; - pr " let op := make_op n in"; - pr " match op.(znz_add_c) x y with"; - pr " | C0 r => %sn n r" c; - pr " | C1 r => %sn (S n) (WW op.(znz_1) r) end." c; - pr ""; - - - for i = 0 to size do - pp " Let spec_w%i_add: forall x y, [w%i_add x y] = [%s%i x] + [%s%i y]." i i c i c i; - pp " Proof."; - pp " intros n m; unfold to_Z, w%i_add, w%i_add_c." i i; - pp " generalize (spec_add_c w%i_spec n m); case znz_add_c; auto." i; - pp " intros ww H; rewrite <- H."; - pp " rewrite znz_to_Z_%i; unfold interp_carry;" (i + 1); - pp " apply f_equal2 with (f := Zplus); auto;"; - pp " apply f_equal2 with (f := Zmult); auto;"; - pp " exact (spec_1 w%i_spec)." i; - pp " Qed."; - pp ""; - done; - pp " Let spec_wn_add: forall n x y, [addn n x y] = [%sn n x] + [%sn n y]." c c; - pp " Proof."; - pp " intros k n m; unfold to_Z, addn."; - pp " generalize (spec_add_c (wn_spec k) n m); case znz_add_c; auto."; - pp " intros ww H; rewrite <- H."; - pp " rewrite (znz_to_Z_n k); unfold interp_carry;"; - pp " apply f_equal2 with (f := Zplus); auto;"; - pp " apply f_equal2 with (f := Zmult); auto;"; - pp " exact (spec_1 (wn_spec k))."; - pp " Qed."; - - pr " Definition add := Eval lazy beta delta [same_level] in"; - pr0 " (same_level t_ "; - for i = 0 to size do - pr0 "w%i_add " i; - done; - pr "addn)."; - pr ""; - - pr " Theorem spec_add: forall x y, [add x y] = [x] + [y]."; - pa " Admitted."; - pp " Proof."; - pp " unfold add."; - pp " generalize (spec_same_level t_ (fun x y res => [res] = x + y))."; - pp " unfold same_level; intros HH; apply HH; clear HH."; - for i = 0 to size do - pp " exact spec_w%i_add." i; - done; - pp " exact spec_wn_add."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Predecessor *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_pred_c := w%i_op.(znz_pred_c)." i i - done; - pr ""; - - pr " Definition pred x :="; - pr " match x with"; - for i = 0 to size do - pr " | %s%i wx =>" c i; - pr " match w%i_pred_c wx with" i; - pr " | C0 r => reduce_%i r" i; - pr " | C1 r => zero"; - pr " end"; - done; - pr " | %sn n wx =>" c; - pr " let op := make_op n in"; - pr " match op.(znz_pred_c) wx with"; - pr " | C0 r => reduce_n n r"; - pr " | C1 r => zero"; - pr " end"; - pr " end."; - pr ""; - - pr " Theorem spec_pred_pos : forall x, 0 < [x] -> [pred x] = [x] - 1."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold pred."; - for i = 0 to size do - pp " intros x1 H1; unfold w%i_pred_c;" i; - pp " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1." i; - pp " rewrite spec_reduce_%i; auto." i; - pp " unfold interp_carry; unfold to_Z."; - pp " case (spec_to_Z w%i_spec x1); intros HH1 HH2." i; - pp " case (spec_to_Z w%i_spec y1); intros HH3 HH4 HH5." i; - pp " assert (znz_to_Z w%i_op x1 - 1 < 0); auto with zarith." i; - pp " unfold to_Z in H1; auto with zarith."; - done; - pp " intros n x1 H1;"; - pp " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1."; - pp " rewrite spec_reduce_n; auto."; - pp " unfold interp_carry; unfold to_Z."; - pp " case (spec_to_Z (wn_spec n) x1); intros HH1 HH2."; - pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4 HH5."; - pp " assert (znz_to_Z (make_op n) x1 - 1 < 0); auto with zarith."; - pp " unfold to_Z in H1; auto with zarith."; - pp " Qed."; - pp ""; - - pp " Let spec_pred0: forall x, [x] = 0 -> [pred x] = 0."; - pp " Proof."; - pp " intros x; case x; unfold pred."; - for i = 0 to size do - pp " intros x1 H1; unfold w%i_pred_c;" i; - pp " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1." i; - pp " unfold interp_carry; unfold to_Z."; - pp " unfold to_Z in H1; auto with zarith."; - pp " case (spec_to_Z w%i_spec y1); intros HH3 HH4; auto with zarith." i; - pp " intros; exact (spec_0 w0_spec)."; - done; - pp " intros n x1 H1;"; - pp " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1."; - pp " unfold interp_carry; unfold to_Z."; - pp " unfold to_Z in H1; auto with zarith."; - pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4; auto with zarith."; - pp " intros; exact (spec_0 w0_spec)."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Subtraction *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_sub_c := w%i_op.(znz_sub_c)." i i - done; - pr ""; - - for i = 0 to size do - pr " Definition w%i_sub x y :=" i; - pr " match w%i_sub_c x y with" i; - pr " | C0 r => reduce_%i r" i; - pr " | C1 r => zero"; - pr " end." - done; - pr ""; - - pr " Definition subn n (x y : word w%i (S n)) :=" size; - pr " let op := make_op n in"; - pr " match op.(znz_sub_c) x y with"; - pr " | C0 r => %sn n r" c; - pr " | C1 r => N0 w_0"; - pr " end."; - pr ""; - - for i = 0 to size do - pp " Let spec_w%i_sub: forall x y, [%s%i y] <= [%s%i x] -> [w%i_sub x y] = [%s%i x] - [%s%i y]." i c i c i i c i c i; - pp " Proof."; - pp " intros n m; unfold w%i_sub, w%i_sub_c." i i; - pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c;" i; - if i == 0 then - pp " intros x; auto." - else - pp " intros x; try rewrite spec_reduce_%i; auto." i; - pp " unfold interp_carry; unfold zero, w_0, to_Z."; - pp " rewrite (spec_0 w0_spec)."; - pp " case (spec_to_Z w%i_spec x); intros; auto with zarith." i; - pp " Qed."; - pp ""; - done; - - pp " Let spec_wn_sub: forall n x y, [%sn n y] <= [%sn n x] -> [subn n x y] = [%sn n x] - [%sn n y]." c c c c; - pp " Proof."; - pp " intros k n m; unfold subn."; - pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c;"; - pp " intros x; auto."; - pp " unfold interp_carry, to_Z."; - pp " case (spec_to_Z (wn_spec k) x); intros; auto with zarith."; - pp " Qed."; - pp ""; - - pr " Definition sub := Eval lazy beta delta [same_level] in"; - pr0 " (same_level t_ "; - for i = 0 to size do - pr0 "w%i_sub " i; - done; - pr "subn)."; - pr ""; - - pr " Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y]."; - pa " Admitted."; - pp " Proof."; - pp " unfold sub."; - pp " generalize (spec_same_level t_ (fun x y res => y <= x -> [res] = x - y))."; - pp " unfold same_level; intros HH; apply HH; clear HH."; - for i = 0 to size do - pp " exact spec_w%i_sub." i; - done; - pp " exact spec_wn_sub."; - pp " Qed."; - pr ""; - - for i = 0 to size do - pp " Let spec_w%i_sub0: forall x y, [%s%i x] < [%s%i y] -> [w%i_sub x y] = 0." i c i c i i; - pp " Proof."; - pp " intros n m; unfold w%i_sub, w%i_sub_c." i i; - pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c;" i; - pp " intros x; unfold interp_carry."; - pp " unfold to_Z; case (spec_to_Z w%i_spec x); intros; auto with zarith." i; - pp " intros; unfold to_Z, zero, w_0; rewrite (spec_0 w0_spec); auto."; - pp " Qed."; - pp ""; - done; - - pp " Let spec_wn_sub0: forall n x y, [%sn n x] < [%sn n y] -> [subn n x y] = 0." c c; - pp " Proof."; - pp " intros k n m; unfold subn."; - pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c;"; - pp " intros x; unfold interp_carry."; - pp " unfold to_Z; case (spec_to_Z (wn_spec k) x); intros; auto with zarith."; - pp " intros; unfold to_Z, w_0; rewrite (spec_0 (w0_spec)); auto."; - pp " Qed."; - pp ""; - - pr " Theorem spec_sub0: forall x y, [x] < [y] -> [sub x y] = 0."; - pa " Admitted."; - pp " Proof."; - pp " unfold sub."; - pp " generalize (spec_same_level t_ (fun x y res => x < y -> [res] = 0))."; - pp " unfold same_level; intros HH; apply HH; clear HH."; - for i = 0 to size do - pp " exact spec_w%i_sub0." i; - done; - pp " exact spec_wn_sub0."; - pp " Qed."; - pr ""; - - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Comparison *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition compare_%i := w%i_op.(znz_compare)." i i; - pr " Definition comparen_%i :=" i; - pr " compare_mn_1 w%i w%i %s compare_%i (compare_%i %s) compare_%i." i i (pz i) i i (pz i) i - done; - pr ""; - - pr " Definition comparenm n m wx wy :="; - pr " let mn := Max.max n m in"; - pr " let d := diff n m in"; - pr " let op := make_op mn in"; - pr " op.(znz_compare)"; - pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; - pr " (castm (diff_l n m) (extend_tr wy (fst d)))."; - pr ""; - - pr " Definition compare := Eval lazy beta delta [iter] in"; - pr " (iter _"; - for i = 0 to size do - pr " compare_%i" i; - pr " (fun n x y => CompOpp (comparen_%i (S n) y x))" i; - pr " (fun n => comparen_%i (S n))" i; - done; - pr " comparenm)."; - pr ""; - - for i = 0 to size do - pp " Let spec_compare_%i: forall x y," i; - pp " match compare_%i x y with" i; - pp " Eq => [%s%i x] = [%s%i y]" c i c i; - pp " | Lt => [%s%i x] < [%s%i y]" c i c i; - pp " | Gt => [%s%i x] > [%s%i y]" c i c i; - pp " end."; - pp " Proof."; - pp " unfold compare_%i, to_Z; exact (spec_compare w%i_spec)." i i; - pp " Qed."; - pp ""; - - pp " Let spec_comparen_%i:" i; - pp " forall (n : nat) (x : word w%i n) (y : w%i)," i i; - pp " match comparen_%i n x y with" i; - pp " | Eq => eval%in n x = [%s%i y]" i c i; - pp " | Lt => eval%in n x < [%s%i y]" i c i; - pp " | Gt => eval%in n x > [%s%i y]" i c i; - pp " end."; - pp " intros n x y."; - pp " unfold comparen_%i, to_Z; rewrite spec_double_eval%in." i i; - pp " apply spec_compare_mn_1."; - pp " exact (spec_0 w%i_spec)." i; - pp " intros x1; exact (spec_compare w%i_spec %s x1)." i (pz i); - pp " exact (spec_to_Z w%i_spec)." i; - pp " exact (spec_compare w%i_spec)." i; - pp " exact (spec_compare w%i_spec)." i; - pp " exact (spec_to_Z w%i_spec)." i; - pp " Qed."; - pp ""; - done; - - pp " Let spec_opp_compare: forall c (u v: Z),"; - pp " match c with Eq => u = v | Lt => u < v | Gt => u > v end ->"; - pp " match CompOpp c with Eq => v = u | Lt => v < u | Gt => v > u end."; - pp " Proof."; - pp " intros c u v; case c; unfold CompOpp; auto with zarith."; - pp " Qed."; - pp ""; - - - pr " Theorem spec_compare_aux: forall x y,"; - pr " match compare x y with"; - pr " Eq => [x] = [y]"; - pr " | Lt => [x] < [y]"; - pr " | Gt => [x] > [y]"; - pr " end."; - pa " Admitted."; - pp " Proof."; - pp " refine (spec_iter _ (fun x y res =>"; - pp " match res with"; - pp " Eq => x = y"; - pp " | Lt => x < y"; - pp " | Gt => x > y"; - pp " end)"; - for i = 0 to size do - pp " compare_%i" i; - pp " (fun n x y => CompOpp (comparen_%i (S n) y x))" i; - pp " (fun n => comparen_%i (S n)) _ _ _" i; - done; - pp " comparenm _)."; - - for i = 0 to size - 1 do - pp " exact spec_compare_%i." i; - pp " intros n x y H;apply spec_opp_compare; apply spec_comparen_%i." i; - pp " intros n x y H; exact (spec_comparen_%i (S n) x y)." i; - done; - pp " exact spec_compare_%i." size; - pp " intros n x y;apply spec_opp_compare; apply spec_comparen_%i." size; - pp " intros n; exact (spec_comparen_%i (S n))." size; - pp " intros n m x y; unfold comparenm."; - pp " rewrite <- (spec_cast_l n m x); rewrite <- (spec_cast_r n m y)."; - pp " unfold to_Z; apply (spec_compare (wn_spec (Max.max n m)))."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Multiplication *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_mul_c := w%i_op.(znz_mul_c)." i i - done; - pr ""; - - for i = 0 to size do - pr " Definition w%i_mul_add :=" i; - pr " Eval lazy beta delta [w_mul_add] in"; - pr " @w_mul_add w%i %s w%i_succ w%i_add_c w%i_mul_c." i (pz i) i i i - done; - pr ""; - - for i = 0 to size do - pr " Definition w%i_0W := znz_0W w%i_op." i i - done; - pr ""; - - for i = 0 to size do - pr " Definition w%i_WW := znz_WW w%i_op." i i - done; - pr ""; - - for i = 0 to size do - pr " Definition w%i_mul_add_n1 :=" i; - pr " @double_mul_add_n1 w%i %s w%i_WW w%i_0W w%i_mul_add." i (pz i) i i i - done; - pr ""; - - for i = 0 to size - 1 do - pr " Let to_Z%i n :=" i; - pr " match n return word w%i (S n) -> t_ with" i; - for j = 0 to size - i do - if (i + j) == size then - begin - pr " | %i%s => fun x => %sn 0 x" j "%nat" c; - pr " | %i%s => fun x => %sn 1 x" (j + 1) "%nat" c - end - else - pr " | %i%s => fun x => %s%i x" j "%nat" c (i + j + 1) - done; - pr " | _ => fun _ => N0 w_0"; - pr " end."; - pr ""; - done; - - - for i = 0 to size - 1 do - pp "Theorem to_Z%i_spec:" i; - pp " forall n x, Z_of_nat n <= %i -> [to_Z%i n x] = znz_to_Z (nmake_op _ w%i_op (S n)) x." (size + 1 - i) i i; - for j = 1 to size + 2 - i do - pp " intros n; case n; clear n."; - pp " unfold to_Z%i." i; - pp " intros x H; rewrite spec_eval%in%i; auto." i j; - done; - pp " intros n x."; - pp " repeat rewrite inj_S; unfold Zsucc; auto with zarith."; - pp " Qed."; - pp ""; - done; - - - for i = 0 to size do - pr " Definition w%i_mul n x y :=" i; - pr " let (w,r) := w%i_mul_add_n1 (S n) x y %s in" i (pz i); - if i == size then - begin - pr " if w%i_eq0 w then %sn n r" i c; - pr " else %sn (S n) (WW (extend%i n w) r)." c i; - end - else - begin - pr " if w%i_eq0 w then to_Z%i n r" i i; - pr " else to_Z%i (S n) (WW (extend%i n w) r)." i i; - end; - pr ""; - done; - - pr " Definition mulnm n m x y :="; - pr " let mn := Max.max n m in"; - pr " let d := diff n m in"; - pr " let op := make_op mn in"; - pr " reduce_n (S mn) (op.(znz_mul_c)"; - pr " (castm (diff_r n m) (extend_tr x (snd d)))"; - pr " (castm (diff_l n m) (extend_tr y (fst d))))."; - pr ""; - - pr " Definition mul := Eval lazy beta delta [iter0] in"; - pr " (iter0 t_"; - for i = 0 to size do - pr " (fun x y => reduce_%i (w%i_mul_c x y))" (i + 1) i; - pr " (fun n x y => w%i_mul n y x)" i; - pr " w%i_mul" i; - done; - pr " mulnm"; - pr " (fun _ => N0 w_0)"; - pr " (fun _ => N0 w_0)"; - pr " )."; - pr ""; - for i = 0 to size do - pp " Let spec_w%i_mul_add: forall x y z," i; - pp " let (q,r) := w%i_mul_add x y z in" i; - pp " znz_to_Z w%i_op q * (base (znz_digits w%i_op)) + znz_to_Z w%i_op r =" i i i; - pp " znz_to_Z w%i_op x * znz_to_Z w%i_op y + znz_to_Z w%i_op z :=" i i i ; - pp " (spec_mul_add w%i_spec)." i; - pp ""; - done; - - for i = 0 to size do - pp " Theorem spec_w%i_mul_add_n1: forall n x y z," i; - pp " let (q,r) := w%i_mul_add_n1 n x y z in" i; - pp " znz_to_Z w%i_op q * (base (znz_digits (nmake_op _ w%i_op n))) +" i i; - pp " znz_to_Z (nmake_op _ w%i_op n) r =" i; - pp " znz_to_Z (nmake_op _ w%i_op n) x * znz_to_Z w%i_op y +" i i; - pp " znz_to_Z w%i_op z." i; - pp " Proof."; - pp " intros n x y z; unfold w%i_mul_add_n1." i; - pp " rewrite nmake_double."; - pp " rewrite digits_doubled."; - pp " change (base (DoubleBase.double_digits (znz_digits w%i_op) n)) with" i; - pp " (DoubleBase.double_wB (znz_digits w%i_op) n)." i; - pp " apply spec_double_mul_add_n1; auto."; - if i == 0 then pp " exact (spec_0 w%i_spec)." i; - pp " exact (spec_WW w%i_spec)." i; - pp " exact (spec_0W w%i_spec)." i; - pp " exact (spec_mul_add w%i_spec)." i; - pp " Qed."; - pp ""; - done; - - pp " Lemma nmake_op_WW: forall ww ww1 n x y,"; - pp " znz_to_Z (nmake_op ww ww1 (S n)) (WW x y) ="; - pp " znz_to_Z (nmake_op ww ww1 n) x * base (znz_digits (nmake_op ww ww1 n)) +"; - pp " znz_to_Z (nmake_op ww ww1 n) y."; - pp " auto."; - pp " Qed."; - pp ""; - - for i = 0 to size do - pp " Lemma extend%in_spec: forall n x1," i; - pp " znz_to_Z (nmake_op _ w%i_op (S n)) (extend%i n x1) =" i i; - pp " znz_to_Z w%i_op x1." i; - pp " Proof."; - pp " intros n1 x2; rewrite nmake_double."; - pp " unfold extend%i." i; - pp " rewrite DoubleBase.spec_extend; auto."; - if i == 0 then - pp " intros l; simpl; unfold w_0; rewrite (spec_0 w0_spec); ring."; - pp " Qed."; - pp ""; - done; - - pp " Lemma spec_muln:"; - pp " forall n (x: word _ (S n)) y,"; - pp " [%sn (S n) (znz_mul_c (make_op n) x y)] = [%sn n x] * [%sn n y]." c c c; - pp " Proof."; - pp " intros n x y; unfold to_Z."; - pp " rewrite <- (spec_mul_c (wn_spec n))."; - pp " rewrite make_op_S."; - pp " case znz_mul_c; auto."; - pp " Qed."; - pr ""; - - pr " Theorem spec_mul: forall x y, [mul x y] = [x] * [y]."; - pa " Admitted."; - pp " Proof."; - for i = 0 to size do - pp " assert(F%i:" i; - pp " forall n x y,"; - if i <> size then - pp0 " Z_of_nat n <= %i -> " (size - i); - pp " [w%i_mul n x y] = eval%in (S n) x * [%s%i y])." i i c i; - if i == size then - pp " intros n x y; unfold w%i_mul." i - else - pp " intros n x y H; unfold w%i_mul." i; - pp " generalize (spec_w%i_mul_add_n1 (S n) x y %s)." i (pz i); - pp " case w%i_mul_add_n1; intros x1 y1." i; - pp " change (znz_to_Z (nmake_op _ w%i_op (S n)) x) with (eval%in (S n) x)." i i; - pp " change (znz_to_Z w%i_op y) with ([%s%i y])." i c i; - if i == 0 then - pp " unfold w_0; rewrite (spec_0 w0_spec); rewrite Zplus_0_r." - else - pp " change (znz_to_Z w%i_op W0) with 0; rewrite Zplus_0_r." i; - pp " intros H1; rewrite <- H1; clear H1."; - pp " generalize (spec_w%i_eq0 x1); case w%i_eq0; intros HH." i i; - pp " unfold to_Z in HH; rewrite HH."; - if i == size then - begin - pp " rewrite spec_eval%in; unfold eval%in, nmake_op%i; auto." i i i; - pp " rewrite spec_eval%in; unfold eval%in, nmake_op%i." i i i - end - else - begin - pp " rewrite to_Z%i_spec; auto with zarith." i; - pp " rewrite to_Z%i_spec; try (rewrite inj_S; auto with zarith)." i - end; - pp " rewrite nmake_op_WW; rewrite extend%in_spec; auto." i; - done; - pp " refine (spec_iter0 t_ (fun x y res => [res] = x * y)"; - for i = 0 to size do - pp " (fun x y => reduce_%i (w%i_mul_c x y))" (i + 1) i; - pp " (fun n x y => w%i_mul n y x)" i; - pp " w%i_mul _ _ _" i; - done; - pp " mulnm _"; - pp " (fun _ => N0 w_0) _"; - pp " (fun _ => N0 w_0) _"; - pp " )."; - for i = 0 to size do - pp " intros x y; rewrite spec_reduce_%i." (i + 1); - pp " unfold w%i_mul_c, to_Z." i; - pp " generalize (spec_mul_c w%i_spec x y)." i; - pp " intros HH; rewrite <- HH; clear HH; auto."; - if i == size then - begin - pp " intros n x y; rewrite F%i; auto with zarith." i; - pp " intros n x y; rewrite F%i; auto with zarith." i; - end - else - begin - pp " intros n x y H; rewrite F%i; auto with zarith." i; - pp " intros n x y H; rewrite F%i; auto with zarith." i; - end; - done; - pp " intros n m x y; unfold mulnm."; - pp " rewrite spec_reduce_n."; - pp " rewrite <- (spec_cast_l n m x)."; - pp " rewrite <- (spec_cast_r n m y)."; - pp " rewrite spec_muln; rewrite spec_cast_l; rewrite spec_cast_r; auto."; - pp " intros x; unfold to_Z, w_0; rewrite (spec_0 w0_spec); ring."; - pp " intros x; unfold to_Z, w_0; rewrite (spec_0 w0_spec); ring."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Square *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_square_c := w%i_op.(znz_square_c)." i i - done; - pr ""; - - pr " Definition square x :="; - pr " match x with"; - pr " | %s0 wx => reduce_1 (w0_square_c wx)" c; - for i = 1 to size - 1 do - pr " | %s%i wx => %s%i (w%i_square_c wx)" c i c (i+1) i - done; - pr " | %s%i wx => %sn 0 (w%i_square_c wx)" c size c size; - pr " | %sn n wx =>" c; - pr " let op := make_op n in"; - pr " %sn (S n) (op.(znz_square_c) wx)" c; - pr " end."; - pr ""; - - pr " Theorem spec_square: forall x, [square x] = [x] * [x]."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold square; clear x."; - pp " intros x; rewrite spec_reduce_1; unfold to_Z."; - pp " exact (spec_square_c w%i_spec x)." 0; - for i = 1 to size do - pp " intros x; unfold to_Z."; - pp " exact (spec_square_c w%i_spec x)." i; - done; - pp " intros n x; unfold to_Z."; - pp " rewrite make_op_S."; - pp " exact (spec_square_c (wn_spec n) x)."; - pp "Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Square root *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_sqrt := w%i_op.(znz_sqrt)." i i - done; - pr ""; - - pr " Definition sqrt x :="; - pr " match x with"; - for i = 0 to size do - pr " | %s%i wx => reduce_%i (w%i_sqrt wx)" c i i i; - done; - pr " | %sn n wx =>" c; - pr " let op := make_op n in"; - pr " reduce_n n (op.(znz_sqrt) wx)"; - pr " end."; - pr ""; - - pr " Theorem spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2."; - pa " Admitted."; - pp " Proof."; - pp " intros x; unfold sqrt; case x; clear x."; - for i = 0 to size do - pp " intros x; rewrite spec_reduce_%i; exact (spec_sqrt w%i_spec x)." i i; - done; - pp " intros n x; rewrite spec_reduce_n; exact (spec_sqrt (wn_spec n) x)."; - pp " Qed."; - pr ""; - - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Division *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_div_gt := w%i_op.(znz_div_gt)." i i - done; - pr ""; - - pp " Let spec_divn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) :="; - pp " (spec_double_divn1"; - pp " ww_op.(znz_zdigits) ww_op.(znz_0)"; - pp " (znz_WW ww_op) ww_op.(znz_head0)"; - pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)"; - pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)"; - pp " (spec_to_Z ww_spec)"; - pp " (spec_zdigits ww_spec)"; - pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)"; - pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec)"; - pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec))."; - pp ""; - - for i = 0 to size do - pr " Definition w%i_divn1 n x y :=" i; - pr " let (u, v) :="; - pr " double_divn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i; - pr " (znz_WW w%i_op) w%i_op.(znz_head0)" i i; - pr " w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i; - pr " w%i_op.(znz_compare) w%i_op.(znz_sub) (S n) x y in" i i; - if i == size then - pr " (%sn _ u, %s%i v)." c c i - else - pr " (to_Z%i _ u, %s%i v)." i c i; - done; - pr ""; - - for i = 0 to size do - pp " Lemma spec_get_end%i: forall n x y," i; - pp " eval%in n x <= [%s%i y] ->" i c i; - pp " [%s%i (DoubleBase.get_low %s n x)] = eval%in n x." c i (pz i) i; - pp " Proof."; - pp " intros n x y H."; - pp " rewrite spec_double_eval%in; unfold to_Z." i; - pp " apply DoubleBase.spec_get_low."; - pp " exact (spec_0 w%i_spec)." i; - pp " exact (spec_to_Z w%i_spec)." i; - pp " apply Zle_lt_trans with [%s%i y]; auto." c i; - pp " rewrite <- spec_double_eval%in; auto." i; - pp " unfold to_Z; case (spec_to_Z w%i_spec y); auto." i; - pp " Qed."; - pp ""; - done; - - for i = 0 to size do - pr " Let div_gt%i x y := let (u,v) := (w%i_div_gt x y) in (reduce_%i u, reduce_%i v)." i i i i; - done; - pr ""; - - - pr " Let div_gtnm n m wx wy :="; - pr " let mn := Max.max n m in"; - pr " let d := diff n m in"; - pr " let op := make_op mn in"; - pr " let (q, r):= op.(znz_div_gt)"; - pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; - pr " (castm (diff_l n m) (extend_tr wy (fst d))) in"; - pr " (reduce_n mn q, reduce_n mn r)."; - pr ""; - - pr " Definition div_gt := Eval lazy beta delta [iter] in"; - pr " (iter _"; - for i = 0 to size do - pr " div_gt%i" i; - pr " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i); - pr " w%i_divn1" i; - done; - pr " div_gtnm)."; - pr ""; - - pr " Theorem spec_div_gt: forall x y,"; - pr " [x] > [y] -> 0 < [y] ->"; - pr " let (q,r) := div_gt x y in"; - pr " [q] = [x] / [y] /\\ [r] = [x] mod [y]."; - pa " Admitted."; - pp " Proof."; - pp " assert (FO:"; - pp " forall x y, [x] > [y] -> 0 < [y] ->"; - pp " let (q,r) := div_gt x y in"; - pp " [x] = [q] * [y] + [r] /\\ 0 <= [r] < [y])."; - pp " refine (spec_iter (t_*t_) (fun x y res => x > y -> 0 < y ->"; - pp " let (q,r) := res in"; - pp " x = [q] * y + [r] /\\ 0 <= [r] < y)"; - for i = 0 to size do - pp " div_gt%i" i; - pp " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i); - pp " w%i_divn1 _ _ _" i; - done; - pp " div_gtnm _)."; - for i = 0 to size do - pp " intros x y H1 H2; unfold div_gt%i, w%i_div_gt." i i; - pp " generalize (spec_div_gt w%i_spec x y H1 H2); case znz_div_gt." i; - pp " intros xx yy; repeat rewrite spec_reduce_%i; auto." i; - if i == size then - pp " intros n x y H2 H3; unfold div_gt%i, w%i_div_gt." i i - else - pp " intros n x y H1 H2 H3; unfold div_gt%i, w%i_div_gt." i i; - pp " generalize (spec_div_gt w%i_spec x" i; - pp " (DoubleBase.get_low %s (S n) y))." (pz i); - pp0 ""; - for j = 0 to i do - pp0 "unfold w%i; " (i-j); - done; - pp "case znz_div_gt."; - pp " intros xx yy H4; repeat rewrite spec_reduce_%i." i; - pp " generalize (spec_get_end%i (S n) y x); unfold to_Z; intros H5." i; - pp " unfold to_Z in H2; rewrite H5 in H4; auto with zarith."; - if i == size then - pp " intros n x y H2 H3." - else - pp " intros n x y H1 H2 H3."; - pp " generalize"; - pp " (spec_divn1 w%i w%i_op w%i_spec (S n) x y H3)." i i i; - pp0 " unfold w%i_divn1; " i; - for j = 0 to i do - pp0 "unfold w%i; " (i-j); - done; - pp "case double_divn1."; - pp " intros xx yy H4."; - if i == size then - begin - pp " repeat rewrite <- spec_double_eval%in in H4; auto." i; - pp " rewrite spec_eval%in; auto." i; - end - else - begin - pp " rewrite to_Z%i_spec; auto with zarith." i; - pp " repeat rewrite <- spec_double_eval%in in H4; auto." i; - end; - done; - pp " intros n m x y H1 H2; unfold div_gtnm."; - pp " generalize (spec_div_gt (wn_spec (Max.max n m))"; - pp " (castm (diff_r n m)"; - pp " (extend_tr x (snd (diff n m))))"; - pp " (castm (diff_l n m)"; - pp " (extend_tr y (fst (diff n m)))))."; - pp " case znz_div_gt."; - pp " intros xx yy HH."; - pp " repeat rewrite spec_reduce_n."; - pp " rewrite <- (spec_cast_l n m x)."; - pp " rewrite <- (spec_cast_r n m y)."; - pp " unfold to_Z; apply HH."; - pp " rewrite <- (spec_cast_l n m x) in H1; auto."; - pp " rewrite <- (spec_cast_r n m y) in H1; auto."; - pp " rewrite <- (spec_cast_r n m y) in H2; auto."; - pp " intros x y H1 H2; generalize (FO x y H1 H2); case div_gt."; - pp " intros q r (H3, H4); split."; - pp " apply (Zdiv_unique [x] [y] [q] [r]); auto."; - pp " rewrite Zmult_comm; auto."; - pp " apply (Zmod_unique [x] [y] [q] [r]); auto."; - pp " rewrite Zmult_comm; auto."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Modulo *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_mod_gt := w%i_op.(znz_mod_gt)." i i - done; - pr ""; - - for i = 0 to size do - pr " Definition w%i_modn1 :=" i; - pr " double_modn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i; - pr " w%i_op.(znz_head0) w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i i; - pr " w%i_op.(znz_compare) w%i_op.(znz_sub)." i i; - done; - pr ""; - - pr " Let mod_gtnm n m wx wy :="; - pr " let mn := Max.max n m in"; - pr " let d := diff n m in"; - pr " let op := make_op mn in"; - pr " reduce_n mn (op.(znz_mod_gt)"; - pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; - pr " (castm (diff_l n m) (extend_tr wy (fst d))))."; - pr ""; - - pr " Definition mod_gt := Eval lazy beta delta[iter] in"; - pr " (iter _"; - for i = 0 to size do - pr " (fun x y => reduce_%i (w%i_mod_gt x y))" i i; - pr " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i); - pr " (fun n x y => reduce_%i (w%i_modn1 (S n) x y))" i i; - done; - pr " mod_gtnm)."; - pr ""; - - pp " Let spec_modn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) :="; - pp " (spec_double_modn1"; - pp " ww_op.(znz_zdigits) ww_op.(znz_0)"; - pp " (znz_WW ww_op) ww_op.(znz_head0)"; - pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)"; - pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)"; - pp " (spec_to_Z ww_spec)"; - pp " (spec_zdigits ww_spec)"; - pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)"; - pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec)"; - pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec))."; - pp ""; - - pr " Theorem spec_mod_gt:"; - pr " forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y]."; - pa " Admitted."; - pp " Proof."; - pp " refine (spec_iter _ (fun x y res => x > y -> 0 < y ->"; - pp " [res] = x mod y)"; - for i = 0 to size do - pp " (fun x y => reduce_%i (w%i_mod_gt x y))" i i; - pp " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i); - pp " (fun n x y => reduce_%i (w%i_modn1 (S n) x y)) _ _ _" i i; - done; - pp " mod_gtnm _)."; - for i = 0 to size do - pp " intros x y H1 H2; rewrite spec_reduce_%i." i; - pp " exact (spec_mod_gt w%i_spec x y H1 H2)." i; - if i == size then - pp " intros n x y H2 H3; rewrite spec_reduce_%i." i - else - pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i; - pp " unfold w%i_mod_gt." i; - pp " rewrite <- (spec_get_end%i (S n) y x); auto with zarith." i; - pp " unfold to_Z; apply (spec_mod_gt w%i_spec); auto." i; - pp " rewrite <- (spec_get_end%i (S n) y x) in H2; auto with zarith." i; - pp " rewrite <- (spec_get_end%i (S n) y x) in H3; auto with zarith." i; - if i == size then - pp " intros n x y H2 H3; rewrite spec_reduce_%i." i - else - pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i; - pp " unfold w%i_modn1, to_Z; rewrite spec_double_eval%in." i i; - pp " apply (spec_modn1 _ _ w%i_spec); auto." i; - done; - pp " intros n m x y H1 H2; unfold mod_gtnm."; - pp " repeat rewrite spec_reduce_n."; - pp " rewrite <- (spec_cast_l n m x)."; - pp " rewrite <- (spec_cast_r n m y)."; - pp " unfold to_Z; apply (spec_mod_gt (wn_spec (Max.max n m)))."; - pp " rewrite <- (spec_cast_l n m x) in H1; auto."; - pp " rewrite <- (spec_cast_r n m y) in H1; auto."; - pp " rewrite <- (spec_cast_r n m y) in H2; auto."; - pp " Qed."; - pr ""; - - pr " (** digits: a measure for gcd *)"; - pr ""; - - pr " Definition digits x :="; - pr " match x with"; - for i = 0 to size do - pr " | %s%i _ => w%i_op.(znz_digits)" c i i; - done; - pr " | %sn n _ => (make_op n).(znz_digits)" c; - pr " end."; - pr ""; - - pr " Theorem spec_digits: forall x, 0 <= [x] < 2 ^ Zpos (digits x)."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; clear x."; - for i = 0 to size do - pp " intros x; unfold to_Z, digits;"; - pp " generalize (spec_to_Z w%i_spec x); unfold base; intros H; exact H." i; - done; - pp " intros n x; unfold to_Z, digits;"; - pp " generalize (spec_to_Z (wn_spec n) x); unfold base; intros H; exact H."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Conversion *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - pr " Definition pheight p :="; - pr " Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (plength p)))."; - pr ""; - - pr " Theorem pheight_correct: forall p,"; - pr " Zpos p < 2 ^ (Zpos (znz_digits w0_op) * 2 ^ (Z_of_nat (pheight p)))."; - pr " Proof."; - pr " intros p; unfold pheight."; - pr " assert (F1: forall x, Z_of_nat (Peano.pred (nat_of_P x)) = Zpos x - 1)."; - pr " intros x."; - pr " assert (Zsucc (Z_of_nat (Peano.pred (nat_of_P x))) = Zpos x); auto with zarith."; - pr " rewrite <- inj_S."; - pr " rewrite <- (fun x => S_pred x 0); auto with zarith."; - pr " rewrite Zpos_eq_Z_of_nat_o_nat_of_P; auto."; - pr " apply lt_le_trans with 1%snat; auto with zarith." "%"; - pr " exact (le_Pmult_nat x 1)."; - pr " rewrite F1; clear F1."; - pr " assert (F2:= (get_height_correct (znz_digits w0_op) (plength p)))."; - pr " apply Zlt_le_trans with (Zpos (Psucc p))."; - pr " rewrite Zpos_succ_morphism; auto with zarith."; - pr " apply Zle_trans with (1 := plength_pred_correct (Psucc p))."; - pr " rewrite Ppred_succ."; - pr " apply Zpower_le_monotone; auto with zarith."; - pr " Qed."; - pr ""; - - pr " Definition of_pos x :="; - pr " let h := pheight x in"; - pr " match h with"; - for i = 0 to size do - pr " | %i%snat => reduce_%i (snd (w%i_op.(znz_of_pos) x))" i "%" i i; - done; - pr " | _ =>"; - pr " let n := minus h %i in" (size + 1); - pr " reduce_n n (snd ((make_op n).(znz_of_pos) x))"; - pr " end."; - pr ""; - - pr " Theorem spec_of_pos: forall x,"; - pr " [of_pos x] = Zpos x."; - pa " Admitted."; - pp " Proof."; - pp " assert (F := spec_more_than_1_digit w0_spec)."; - pp " intros x; unfold of_pos; case_eq (pheight x)."; - for i = 0 to size do - if i <> 0 then - pp " intros n; case n; clear n."; - pp " intros H1; rewrite spec_reduce_%i; unfold to_Z." i; - pp " apply (znz_of_pos_correct w%i_spec)." i; - pp " apply Zlt_le_trans with (1 := pheight_correct x)."; - pp " rewrite H1; simpl Z_of_nat; change (2^%i) with (%s)." i (gen2 i); - pp " unfold base."; - pp " apply Zpower_le_monotone; split; auto with zarith."; - if i <> 0 then - begin - pp " rewrite Zmult_comm; repeat rewrite <- Zmult_assoc."; - pp " repeat rewrite <- Zpos_xO."; - pp " refine (Zle_refl _)."; - end; - done; - pp " intros n."; - pp " intros H1; rewrite spec_reduce_n; unfold to_Z."; - pp " simpl minus; rewrite <- minus_n_O."; - pp " apply (znz_of_pos_correct (wn_spec n))."; - pp " apply Zlt_le_trans with (1 := pheight_correct x)."; - pp " unfold base."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " split; auto with zarith."; - pp " rewrite H1."; - pp " elim n; clear n H1."; - pp " simpl Z_of_nat; change (2^%i) with (%s)." (size + 1) (gen2 (size + 1)); - pp " rewrite Zmult_comm; repeat rewrite <- Zmult_assoc."; - pp " repeat rewrite <- Zpos_xO."; - pp " refine (Zle_refl _)."; - pp " intros n Hrec."; - pp " rewrite make_op_S."; - pp " change (@znz_digits (word _ (S (S n))) (mk_zn2z_op_karatsuba (make_op n))) with"; - pp " (xO (znz_digits (make_op n)))."; - pp " rewrite (fun x y => (Zpos_xO (@znz_digits x y)))."; - pp " rewrite inj_S; unfold Zsucc."; - pp " rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith."; - pp " rewrite Zpower_1_r."; - pp " assert (tmp: forall x y z, x * (y * z) = y * (x * z));"; - pp " [intros; ring | rewrite tmp; clear tmp]."; - pp " apply Zmult_le_compat_l; auto with zarith."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Shift *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - (* Head0 *) - pr " Definition head0 w := match w with"; - for i = 0 to size do - pr " | %s%i w=> reduce_%i (w%i_op.(znz_head0) w)" c i i i; - done; - pr " | %sn n w=> reduce_n n ((make_op n).(znz_head0) w)" c; - pr " end."; - pr ""; - - pr " Theorem spec_head00: forall x, [x] = 0 ->[head0 x] = Zpos (digits x)."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold head0; clear x."; - for i = 0 to size do - pp " intros x; rewrite spec_reduce_%i; exact (spec_head00 w%i_spec x)." i i; - done; - pp " intros n x; rewrite spec_reduce_n; exact (spec_head00 (wn_spec n) x)."; - pp " Qed."; - pr ""; - - pr " Theorem spec_head0: forall x, 0 < [x] ->"; - pr " 2 ^ (Zpos (digits x) - 1) <= 2 ^ [head0 x] * [x] < 2 ^ Zpos (digits x)."; - pa " Admitted."; - pp " Proof."; - pp " assert (F0: forall x, (x - 1) + 1 = x)."; - pp " intros; ring."; - pp " intros x; case x; unfold digits, head0; clear x."; - for i = 0 to size do - pp " intros x Hx; rewrite spec_reduce_%i." i; - pp " assert (F1:= spec_more_than_1_digit w%i_spec)." i; - pp " generalize (spec_head0 w%i_spec x Hx)." i; - pp " unfold base."; - pp " pattern (Zpos (znz_digits w%i_op)) at 1;" i; - pp " rewrite <- (fun x => (F0 (Zpos x)))."; - pp " rewrite Zpower_exp; auto with zarith."; - pp " rewrite Zpower_1_r; rewrite Z_div_mult; auto with zarith."; - done; - pp " intros n x Hx; rewrite spec_reduce_n."; - pp " assert (F1:= spec_more_than_1_digit (wn_spec n))."; - pp " generalize (spec_head0 (wn_spec n) x Hx)."; - pp " unfold base."; - pp " pattern (Zpos (znz_digits (make_op n))) at 1;"; - pp " rewrite <- (fun x => (F0 (Zpos x)))."; - pp " rewrite Zpower_exp; auto with zarith."; - pp " rewrite Zpower_1_r; rewrite Z_div_mult; auto with zarith."; - pp " Qed."; - pr ""; - - - (* Tail0 *) - pr " Definition tail0 w := match w with"; - for i = 0 to size do - pr " | %s%i w=> reduce_%i (w%i_op.(znz_tail0) w)" c i i i; - done; - pr " | %sn n w=> reduce_n n ((make_op n).(znz_tail0) w)" c; - pr " end."; - pr ""; - - - pr " Theorem spec_tail00: forall x, [x] = 0 ->[tail0 x] = Zpos (digits x)."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold tail0; clear x."; - for i = 0 to size do - pp " intros x; rewrite spec_reduce_%i; exact (spec_tail00 w%i_spec x)." i i; - done; - pp " intros n x; rewrite spec_reduce_n; exact (spec_tail00 (wn_spec n) x)."; - pp " Qed."; - pr ""; - - - pr " Theorem spec_tail0: forall x,"; - pr " 0 < [x] -> exists y, 0 <= y /\\ [x] = (2 * y + 1) * 2 ^ [tail0 x]."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; clear x; unfold tail0."; - for i = 0 to size do - pp " intros x Hx; rewrite spec_reduce_%i; exact (spec_tail0 w%i_spec x Hx)." i i; - done; - pp " intros n x Hx; rewrite spec_reduce_n; exact (spec_tail0 (wn_spec n) x Hx)."; - pp " Qed."; - pr ""; - - - (* Number of digits *) - pr " Definition %sdigits x :=" c; - pr " match x with"; - pr " | %s0 _ => %s0 w0_op.(znz_zdigits)" c c; - for i = 1 to size do - pr " | %s%i _ => reduce_%i w%i_op.(znz_zdigits)" c i i i; - done; - pr " | %sn n _ => reduce_n n (make_op n).(znz_zdigits)" c; - pr " end."; - pr ""; - - pr " Theorem spec_Ndigits: forall x, [Ndigits x] = Zpos (digits x)."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; clear x; unfold Ndigits, digits."; - for i = 0 to size do - pp " intros _; try rewrite spec_reduce_%i; exact (spec_zdigits w%i_spec)." i i; - done; - pp " intros n _; try rewrite spec_reduce_n; exact (spec_zdigits (wn_spec n))."; - pp " Qed."; - pr ""; - - - (* Shiftr *) - for i = 0 to size do - pr " Definition unsafe_shiftr%i n x := w%i_op.(znz_add_mul_div) (w%i_op.(znz_sub) w%i_op.(znz_zdigits) n) w%i_op.(znz_0) x." i i i i i; - done; - pr " Definition unsafe_shiftrn n p x := (make_op n).(znz_add_mul_div) ((make_op n).(znz_sub) (make_op n).(znz_zdigits) p) (make_op n).(znz_0) x."; - pr ""; - - pr " Definition unsafe_shiftr := Eval lazy beta delta [same_level] in"; - pr " same_level _ (fun n x => %s0 (unsafe_shiftr0 n x))" c; - for i = 1 to size do - pr " (fun n x => reduce_%i (unsafe_shiftr%i n x))" i i; - done; - pr " (fun n p x => reduce_n n (unsafe_shiftrn n p x))."; - pr ""; - - - pr " Theorem spec_unsafe_shiftr: forall n x,"; - pr " [n] <= [Ndigits x] -> [unsafe_shiftr n x] = [x] / 2 ^ [n]."; - pa " Admitted."; - pp " Proof."; - pp " assert (F0: forall x y, x - (x - y) = y)."; - pp " intros; ring."; - pp " assert (F2: forall x y z, 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z)."; - pp " intros x y z HH HH1 HH2."; - pp " split; auto with zarith."; - pp " apply Zle_lt_trans with (2 := HH2); auto with zarith."; - pp " apply Zdiv_le_upper_bound; auto with zarith."; - pp " pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith."; - pp " apply Zmult_le_compat_l; auto."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " rewrite Zpower_0_r; ring."; - pp " assert (F3: forall x y, 0 <= y -> y <= x -> 0 <= x - y < 2 ^ x)."; - pp " intros xx y HH HH1."; - pp " split; auto with zarith."; - pp " apply Zle_lt_trans with xx; auto with zarith."; - pp " apply Zpower2_lt_lin; auto with zarith."; - pp " assert (F4: forall ww ww1 ww2"; - pp " (ww_op: znz_op ww) (ww1_op: znz_op ww1) (ww2_op: znz_op ww2)"; - pp " xx yy xx1 yy1,"; - pp " znz_to_Z ww2_op yy <= znz_to_Z ww1_op (znz_zdigits ww1_op) ->"; - pp " znz_to_Z ww1_op (znz_zdigits ww1_op) <= znz_to_Z ww_op (znz_zdigits ww_op) ->"; - pp " znz_spec ww_op -> znz_spec ww1_op -> znz_spec ww2_op ->"; - pp " znz_to_Z ww_op xx1 = znz_to_Z ww1_op xx ->"; - pp " znz_to_Z ww_op yy1 = znz_to_Z ww2_op yy ->"; - pp " znz_to_Z ww_op"; - pp " (znz_add_mul_div ww_op (znz_sub ww_op (znz_zdigits ww_op) yy1)"; - pp " (znz_0 ww_op) xx1) = znz_to_Z ww1_op xx / 2 ^ znz_to_Z ww2_op yy)."; - pp " intros ww ww1 ww2 ww_op ww1_op ww2_op xx yy xx1 yy1 Hl Hl1 Hw Hw1 Hw2 Hx Hy."; - pp " case (spec_to_Z Hw xx1); auto with zarith; intros HH1 HH2."; - pp " case (spec_to_Z Hw yy1); auto with zarith; intros HH3 HH4."; - pp " rewrite <- Hx."; - pp " rewrite <- Hy."; - pp " generalize (spec_add_mul_div Hw"; - pp " (znz_0 ww_op) xx1"; - pp " (znz_sub ww_op (znz_zdigits ww_op)"; - pp " yy1)"; - pp " )."; - pp " rewrite (spec_0 Hw)."; - pp " rewrite Zmult_0_l; rewrite Zplus_0_l."; - pp " rewrite (CyclicAxioms.spec_sub Hw)."; - pp " rewrite Zmod_small; auto with zarith."; - pp " rewrite (spec_zdigits Hw)."; - pp " rewrite F0."; - pp " rewrite Zmod_small; auto with zarith."; - pp " unfold base; rewrite (spec_zdigits Hw) in Hl1 |- *;"; - pp " auto with zarith."; - pp " assert (F5: forall n m, (n <= m)%snat ->" "%"; - pp " Zpos (znz_digits (make_op n)) <= Zpos (znz_digits (make_op m)))."; - pp " intros n m HH; elim HH; clear m HH; auto with zarith."; - pp " intros m HH Hrec; apply Zle_trans with (1 := Hrec)."; - pp " rewrite make_op_S."; - pp " match goal with |- Zpos ?Y <= ?X => change X with (Zpos (xO Y)) end."; - pp " rewrite Zpos_xO."; - pp " assert (0 <= Zpos (znz_digits (make_op n))); auto with zarith."; - pp " assert (F6: forall n, Zpos (znz_digits w%i_op) <= Zpos (znz_digits (make_op n)))." size; - pp " intros n ; apply Zle_trans with (Zpos (znz_digits (make_op 0)))."; - pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size; - pp " rewrite Zpos_xO."; - pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size; - pp " apply F5; auto with arith."; - pp " intros x; case x; clear x; unfold unsafe_shiftr, same_level."; - for i = 0 to size do - pp " intros x y; case y; clear y."; - for j = 0 to i - 1 do - pp " intros y; unfold unsafe_shiftr%i, Ndigits." i; - pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; - pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i; - pp " rewrite (spec_zdigits w%i_spec)." i; - pp " rewrite (spec_zdigits w%i_spec)." j; - pp " change (znz_digits w%i_op) with %s." i (genxO (i - j) (" (znz_digits w"^(string_of_int j)^"_op)")); - pp " repeat rewrite (fun x => Zpos_xO (xO x))."; - pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; - pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." j; - pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i; - - done; - pp " intros y; unfold unsafe_shiftr%i, Ndigits." i; - pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i; - pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i; - for j = i + 1 to size do - pp " intros y; unfold unsafe_shiftr%i, Ndigits." j; - pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; - pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i; - pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j; - done; - if i == size then - begin - pp " intros m y; unfold unsafe_shiftrn, Ndigits."; - pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; - pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size; - pp " try (apply sym_equal; exact (spec_extend%in m x))." size; - end - else - begin - pp " intros m y; unfold unsafe_shiftrn, Ndigits."; - pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; - pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i; - pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i; - pp " rewrite <- (spec_extend%in m); rewrite <- spec_extend%in%i; auto." size i size; - end - done; - pp " intros n x y; case y; clear y;"; - pp " intros y; unfold unsafe_shiftrn, Ndigits; try rewrite spec_reduce_n."; - for i = 0 to size do - pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i; - pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i; - pp " rewrite (spec_zdigits w%i_spec)." i; - pp " rewrite (spec_zdigits (wn_spec n))."; - pp " apply Zle_trans with (2 := F6 n)."; - pp " change (znz_digits w%i_op) with %s." size (genxO (size - i) ("(znz_digits w" ^ (string_of_int i) ^ "_op)")); - pp " repeat rewrite (fun x => Zpos_xO (xO x))."; - pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; - pp " assert (H: 0 <= Zpos (znz_digits w%i_op)); auto with zarith." i; - if i == size then - pp " change ([Nn n (extend%i n y)] = [N%i y])." size i - else - pp " change ([Nn n (extend%i n (extend%i %i y))] = [N%i y])." size i (size - i - 1) i; - pp " rewrite <- (spec_extend%in n); auto." size; - if i <> size then - pp " try (rewrite <- spec_extend%in%i; auto)." i size; - done; - pp " generalize y; clear y; intros m y."; - pp " rewrite spec_reduce_n; unfold to_Z; intros H1."; - pp " apply F4 with (3:=(wn_spec (Max.max n m)))(4:=wn_spec m)(5:=wn_spec n); auto with zarith."; - pp " rewrite (spec_zdigits (wn_spec m))."; - pp " rewrite (spec_zdigits (wn_spec (Max.max n m)))."; - pp " apply F5; auto with arith."; - pp " exact (spec_cast_r n m y)."; - pp " exact (spec_cast_l n m x)."; - pp " Qed."; - pr ""; - - (* Unsafe_Shiftl *) - for i = 0 to size do - pr " Definition unsafe_shiftl%i n x := w%i_op.(znz_add_mul_div) n x w%i_op.(znz_0)." i i i - done; - pr " Definition unsafe_shiftln n p x := (make_op n).(znz_add_mul_div) p x (make_op n).(znz_0)."; - pr " Definition unsafe_shiftl := Eval lazy beta delta [same_level] in"; - pr " same_level _ (fun n x => %s0 (unsafe_shiftl0 n x))" c; - for i = 1 to size do - pr " (fun n x => reduce_%i (unsafe_shiftl%i n x))" i i; - done; - pr " (fun n p x => reduce_n n (unsafe_shiftln n p x))."; - pr ""; - pr ""; - - - pr " Theorem spec_unsafe_shiftl: forall n x,"; - pr " [n] <= [head0 x] -> [unsafe_shiftl n x] = [x] * 2 ^ [n]."; - pa " Admitted."; - pp " Proof."; - pp " assert (F0: forall x y, x - (x - y) = y)."; - pp " intros; ring."; - pp " assert (F2: forall x y z, 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z)."; - pp " intros x y z HH HH1 HH2."; - pp " split; auto with zarith."; - pp " apply Zle_lt_trans with (2 := HH2); auto with zarith."; - pp " apply Zdiv_le_upper_bound; auto with zarith."; - pp " pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith."; - pp " apply Zmult_le_compat_l; auto."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " rewrite Zpower_0_r; ring."; - pp " assert (F3: forall x y, 0 <= y -> y <= x -> 0 <= x - y < 2 ^ x)."; - pp " intros xx y HH HH1."; - pp " split; auto with zarith."; - pp " apply Zle_lt_trans with xx; auto with zarith."; - pp " apply Zpower2_lt_lin; auto with zarith."; - pp " assert (F4: forall ww ww1 ww2"; - pp " (ww_op: znz_op ww) (ww1_op: znz_op ww1) (ww2_op: znz_op ww2)"; - pp " xx yy xx1 yy1,"; - pp " znz_to_Z ww2_op yy <= znz_to_Z ww1_op (znz_head0 ww1_op xx) ->"; - pp " znz_to_Z ww1_op (znz_zdigits ww1_op) <= znz_to_Z ww_op (znz_zdigits ww_op) ->"; - pp " znz_spec ww_op -> znz_spec ww1_op -> znz_spec ww2_op ->"; - pp " znz_to_Z ww_op xx1 = znz_to_Z ww1_op xx ->"; - pp " znz_to_Z ww_op yy1 = znz_to_Z ww2_op yy ->"; - pp " znz_to_Z ww_op"; - pp " (znz_add_mul_div ww_op yy1"; - pp " xx1 (znz_0 ww_op)) = znz_to_Z ww1_op xx * 2 ^ znz_to_Z ww2_op yy)."; - pp " intros ww ww1 ww2 ww_op ww1_op ww2_op xx yy xx1 yy1 Hl Hl1 Hw Hw1 Hw2 Hx Hy."; - pp " case (spec_to_Z Hw xx1); auto with zarith; intros HH1 HH2."; - pp " case (spec_to_Z Hw yy1); auto with zarith; intros HH3 HH4."; - pp " rewrite <- Hx."; - pp " rewrite <- Hy."; - pp " generalize (spec_add_mul_div Hw xx1 (znz_0 ww_op) yy1)."; - pp " rewrite (spec_0 Hw)."; - pp " assert (F1: znz_to_Z ww1_op (znz_head0 ww1_op xx) <= Zpos (znz_digits ww1_op))."; - pp " case (Zle_lt_or_eq _ _ HH1); intros HH5."; - pp " apply Zlt_le_weak."; - pp " case (CyclicAxioms.spec_head0 Hw1 xx)."; - pp " rewrite <- Hx; auto."; - pp " intros _ Hu; unfold base in Hu."; - pp " case (Zle_or_lt (Zpos (znz_digits ww1_op))"; - pp " (znz_to_Z ww1_op (znz_head0 ww1_op xx))); auto; intros H1."; - pp " absurd (2 ^ (Zpos (znz_digits ww1_op)) <= 2 ^ (znz_to_Z ww1_op (znz_head0 ww1_op xx)))."; - pp " apply Zlt_not_le."; - pp " case (spec_to_Z Hw1 xx); intros HHx3 HHx4."; - pp " rewrite <- (Zmult_1_r (2 ^ znz_to_Z ww1_op (znz_head0 ww1_op xx)))."; - pp " apply Zle_lt_trans with (2 := Hu)."; - pp " apply Zmult_le_compat_l; auto with zarith."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith."; - pp " rewrite Zdiv_0_l; auto with zarith."; - pp " rewrite Zplus_0_r."; - pp " case (Zle_lt_or_eq _ _ HH1); intros HH5."; - pp " rewrite Zmod_small; auto with zarith."; - pp " intros HH; apply HH."; - pp " rewrite Hy; apply Zle_trans with (1:= Hl)."; - pp " rewrite <- (spec_zdigits Hw)."; - pp " apply Zle_trans with (2 := Hl1); auto."; - pp " rewrite (spec_zdigits Hw1); auto with zarith."; - pp " split; auto with zarith ."; - pp " apply Zlt_le_trans with (base (znz_digits ww1_op))."; - pp " rewrite Hx."; - pp " case (CyclicAxioms.spec_head0 Hw1 xx); auto."; - pp " rewrite <- Hx; auto."; - pp " intros _ Hu; rewrite Zmult_comm in Hu."; - pp " apply Zle_lt_trans with (2 := Hu)."; - pp " apply Zmult_le_compat_l; auto with zarith."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " unfold base; apply Zpower_le_monotone; auto with zarith."; - pp " split; auto with zarith."; - pp " rewrite <- (spec_zdigits Hw); auto with zarith."; - pp " rewrite <- (spec_zdigits Hw1); auto with zarith."; - pp " rewrite <- HH5."; - pp " rewrite Zmult_0_l."; - pp " rewrite Zmod_small; auto with zarith."; - pp " intros HH; apply HH."; - pp " rewrite Hy; apply Zle_trans with (1 := Hl)."; - pp " rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith."; - pp " rewrite <- (spec_zdigits Hw); auto with zarith."; - pp " rewrite <- (spec_zdigits Hw1); auto with zarith."; - pp " assert (F5: forall n m, (n <= m)%snat ->" "%"; - pp " Zpos (znz_digits (make_op n)) <= Zpos (znz_digits (make_op m)))."; - pp " intros n m HH; elim HH; clear m HH; auto with zarith."; - pp " intros m HH Hrec; apply Zle_trans with (1 := Hrec)."; - pp " rewrite make_op_S."; - pp " match goal with |- Zpos ?Y <= ?X => change X with (Zpos (xO Y)) end."; - pp " rewrite Zpos_xO."; - pp " assert (0 <= Zpos (znz_digits (make_op n))); auto with zarith."; - pp " assert (F6: forall n, Zpos (znz_digits w%i_op) <= Zpos (znz_digits (make_op n)))." size; - pp " intros n ; apply Zle_trans with (Zpos (znz_digits (make_op 0)))."; - pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size; - pp " rewrite Zpos_xO."; - pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size; - pp " apply F5; auto with arith."; - pp " intros x; case x; clear x; unfold unsafe_shiftl, same_level."; - for i = 0 to size do - pp " intros x y; case y; clear y."; - for j = 0 to i - 1 do - pp " intros y; unfold unsafe_shiftl%i, head0." i; - pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; - pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i; - pp " rewrite (spec_zdigits w%i_spec)." i; - pp " rewrite (spec_zdigits w%i_spec)." j; - pp " change (znz_digits w%i_op) with %s." i (genxO (i - j) (" (znz_digits w"^(string_of_int j)^"_op)")); - pp " repeat rewrite (fun x => Zpos_xO (xO x))."; - pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; - pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." j; - pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i; - done; - pp " intros y; unfold unsafe_shiftl%i, head0." i; - pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i; - pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i; - for j = i + 1 to size do - pp " intros y; unfold unsafe_shiftl%i, head0." j; - pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; - pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i; - pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j; - done; - if i == size then - begin - pp " intros m y; unfold unsafe_shiftln, head0."; - pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; - pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size; - pp " try (apply sym_equal; exact (spec_extend%in m x))." size; - end - else - begin - pp " intros m y; unfold unsafe_shiftln, head0."; - pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; - pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i; - pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i; - pp " rewrite <- (spec_extend%in m); rewrite <- spec_extend%in%i; auto." size i size; - end - done; - pp " intros n x y; case y; clear y;"; - pp " intros y; unfold unsafe_shiftln, head0; try rewrite spec_reduce_n."; - for i = 0 to size do - pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i; - pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i; - pp " rewrite (spec_zdigits w%i_spec)." i; - pp " rewrite (spec_zdigits (wn_spec n))."; - pp " apply Zle_trans with (2 := F6 n)."; - pp " change (znz_digits w%i_op) with %s." size (genxO (size - i) ("(znz_digits w" ^ (string_of_int i) ^ "_op)")); - pp " repeat rewrite (fun x => Zpos_xO (xO x))."; - pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; - pp " assert (H: 0 <= Zpos (znz_digits w%i_op)); auto with zarith." i; - if i == size then - pp " change ([Nn n (extend%i n y)] = [N%i y])." size i - else - pp " change ([Nn n (extend%i n (extend%i %i y))] = [N%i y])." size i (size - i - 1) i; - pp " rewrite <- (spec_extend%in n); auto." size; - if i <> size then - pp " try (rewrite <- spec_extend%in%i; auto)." i size; - done; - pp " generalize y; clear y; intros m y."; - pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; - pp " apply F4 with (3:=(wn_spec (Max.max n m)))(4:=wn_spec m)(5:=wn_spec n); auto with zarith."; - pp " rewrite (spec_zdigits (wn_spec m))."; - pp " rewrite (spec_zdigits (wn_spec (Max.max n m)))."; - pp " apply F5; auto with arith."; - pp " exact (spec_cast_r n m y)."; - pp " exact (spec_cast_l n m x)."; - pp " Qed."; - pr ""; - - (* Double size *) - pr " Definition double_size w := match w with"; - for i = 0 to size-1 do - pr " | %s%i x => %s%i (WW (znz_0 w%i_op) x)" c i c (i + 1) i; - done; - pr " | %s%i x => %sn 0 (WW (znz_0 w%i_op) x)" c size c size; - pr " | %sn n x => %sn (S n) (WW (znz_0 (make_op n)) x)" c c; - pr " end."; - pr ""; - - pr " Theorem spec_double_size_digits:"; - pr " forall x, digits (double_size x) = xO (digits x)."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold double_size, digits; clear x; auto."; - pp " intros n x; rewrite make_op_S; auto."; - pp " Qed."; - pr ""; - - - pr " Theorem spec_double_size: forall x, [double_size x] = [x]."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold double_size; clear x."; - for i = 0 to size do - pp " intros x; unfold to_Z, make_op;"; - pp " rewrite znz_to_Z_%i; rewrite (spec_0 w%i_spec); auto with zarith." (i + 1) i; - done; - pp " intros n x; unfold to_Z;"; - pp " generalize (znz_to_Z_n n); simpl word."; - pp " intros HH; rewrite HH; clear HH."; - pp " generalize (spec_0 (wn_spec n)); simpl word."; - pp " intros HH; rewrite HH; clear HH; auto with zarith."; - pp " Qed."; - pr ""; - - - pr " Theorem spec_double_size_head0:"; - pr " forall x, 2 * [head0 x] <= [head0 (double_size x)]."; - pa " Admitted."; - pp " Proof."; - pp " intros x."; - pp " assert (F1:= spec_pos (head0 x))."; - pp " assert (F2: 0 < Zpos (digits x))."; - pp " red; auto."; - pp " case (Zle_lt_or_eq _ _ (spec_pos x)); intros HH."; - pp " generalize HH; rewrite <- (spec_double_size x); intros HH1."; - pp " case (spec_head0 x HH); intros _ HH2."; - pp " case (spec_head0 _ HH1)."; - pp " rewrite (spec_double_size x); rewrite (spec_double_size_digits x)."; - pp " intros HH3 _."; - pp " case (Zle_or_lt ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4."; - pp " absurd (2 ^ (2 * [head0 x] )* [x] < 2 ^ [head0 (double_size x)] * [x]); auto."; - pp " apply Zle_not_lt."; - pp " apply Zmult_le_compat_r; auto with zarith."; - pp " apply Zpower_le_monotone; auto; auto with zarith."; - pp " generalize (spec_pos (head0 (double_size x))); auto with zarith."; - pp " assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1))."; - pp " case (Zle_lt_or_eq 1 [x]); auto with zarith; intros HH5."; - pp " apply Zmult_le_reg_r with (2 ^ 1); auto with zarith."; - pp " rewrite <- (fun x y z => Zpower_exp x (y - z)); auto with zarith."; - pp " assert (tmp: forall x, x - 1 + 1 = x); [intros; ring | rewrite tmp; clear tmp]."; - pp " apply Zle_trans with (2 := Zlt_le_weak _ _ HH2)."; - pp " apply Zmult_le_compat_l; auto with zarith."; - pp " rewrite Zpower_1_r; auto with zarith."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " split; auto with zarith."; - pp " case (Zle_or_lt (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6."; - pp " absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith."; - pp " rewrite <- HH5; rewrite Zmult_1_r."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " rewrite (Zmult_comm 2)."; - pp " rewrite Zpower_mult; auto with zarith."; - pp " rewrite Zpower_2."; - pp " apply Zlt_le_trans with (2 := HH3)."; - pp " rewrite <- Zmult_assoc."; - pp " replace (Zpos (xO (digits x)) - 1) with"; - pp " ((Zpos (digits x) - 1) + (Zpos (digits x)))."; - pp " rewrite Zpower_exp; auto with zarith."; - pp " apply Zmult_lt_compat2; auto with zarith."; - pp " split; auto with zarith."; - pp " apply Zmult_lt_0_compat; auto with zarith."; - pp " rewrite Zpos_xO; ring."; - pp " apply Zlt_le_weak; auto."; - pp " repeat rewrite spec_head00; auto."; - pp " rewrite spec_double_size_digits."; - pp " rewrite Zpos_xO; auto with zarith."; - pp " rewrite spec_double_size; auto."; - pp " Qed."; - pr ""; - - pr " Theorem spec_double_size_head0_pos:"; - pr " forall x, 0 < [head0 (double_size x)]."; - pa " Admitted."; - pp " Proof."; - pp " intros x."; - pp " assert (F: 0 < Zpos (digits x))."; - pp " red; auto."; - pp " case (Zle_lt_or_eq _ _ (spec_pos (head0 (double_size x)))); auto; intros F0."; - pp " case (Zle_lt_or_eq _ _ (spec_pos (head0 x))); intros F1."; - pp " apply Zlt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith."; - pp " case (Zle_lt_or_eq _ _ (spec_pos x)); intros F3."; - pp " generalize F3; rewrite <- (spec_double_size x); intros F4."; - pp " absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x)))."; - pp " apply Zle_not_lt."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " split; auto with zarith."; - pp " rewrite Zpos_xO; auto with zarith."; - pp " case (spec_head0 x F3)."; - pp " rewrite <- F1; rewrite Zpower_0_r; rewrite Zmult_1_l; intros _ HH."; - pp " apply Zle_lt_trans with (2 := HH)."; - pp " case (spec_head0 _ F4)."; - pp " rewrite (spec_double_size x); rewrite (spec_double_size_digits x)."; - pp " rewrite <- F0; rewrite Zpower_0_r; rewrite Zmult_1_l; auto."; - pp " generalize F1; rewrite (spec_head00 _ (sym_equal F3)); auto with zarith."; - pp " Qed."; - pr ""; - - (* even *) - pr " Definition is_even x :="; - pr " match x with"; - for i = 0 to size do - pr " | %s%i wx => w%i_op.(znz_is_even) wx" c i i - done; - pr " | %sn n wx => (make_op n).(znz_is_even) wx" c; - pr " end."; - pr ""; - - - pr " Theorem spec_is_even: forall x,"; - pr " if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold is_even, to_Z; clear x."; - for i = 0 to size do - pp " intros x; exact (spec_is_even w%i_spec x)." i; - done; - pp " intros n x; exact (spec_is_even (wn_spec n) x)."; - pp " Qed."; - pr ""; - - pr "End Make."; - pr ""; - + 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 " + 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 index cdd41647..5bde1008 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,9 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: Nbasic.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - -Require Import ZArith. +Require Import ZArith Ndigits. Require Import BigNumPrelude. Require Import Max. Require Import DoubleType. @@ -18,44 +16,64 @@ 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 => Psucc (plength p1) - | xI p1 => Psucc (plength p1) + | 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 (Psucc p)) = 2 * 2 ^ Zpos p)%Z). -intros p; replace (Zpos (Psucc p)) with (1 + Zpos 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 Zpos_succ_morphism; unfold Zsucc; 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 Zpos_xI. +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 (Zpos_xO p1). +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 Zpower_1_r; auto with zarith. +rewrite Z.pow_1_r; auto with zarith. Qed. -Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))%Z. -intros p; case (Psucc_pred p); intros H1. +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 Zpower_1_r; auto with zarith. +rewrite Z.pow_1_r; auto with zarith. pattern p at 1; rewrite <- H1. -rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith. -generalize (plength_correct (Ppred p)); auto with zarith. +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 Zdiv (Zpos p) (Zpos q) with + match Z.div (Zpos p) (Zpos q) with Zpos q1 => match (Zpos p) - (Zpos q) * (Zpos q1) with Z0 => q1 - | _ => (Psucc q1) + | _ => (Pos.succ q1) end | _ => xH end. @@ -67,20 +85,20 @@ 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 Zdiv. - intros HH _; rewrite HH; rewrite Zmult_0_r; rewrite Zmult_1_r; simpl. +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 Zmod. + case Z.modulo. intros HH _; rewrite HH; auto with zarith. - intros r1 HH (_,HH1); rewrite HH; rewrite Zpos_succ_morphism. - unfold Zsucc; rewrite Zmult_plus_distr_r; 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 Zge; simpl Zcompare; intros HH1; case HH1; auto. +unfold Z.ge; simpl Z.compare; intros HH1; case HH1; auto. Qed. Definition is_one p := match p with xH => true | _ => false end. @@ -91,7 +109,7 @@ Qed. Definition get_height digits p := let r := Pdiv p digits in - if is_one r then xH else Psucc (plength (Ppred r)). + if is_one r then xH else Pos.succ (plength (Pos.pred r)). Theorem get_height_correct: forall digits N, @@ -101,13 +119,13 @@ 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 Zmult_1_r in H1. -change (2^(1-1))%Z with 1; rewrite Zmult_1_r; auto. +rewrite Z.mul_1_r in H1. +change (2^(1-1))%Z with 1; rewrite Z.mul_1_r; auto. clear H2. -apply Zle_trans with (1 := H1). -apply Zmult_le_compat_l; auto with zarith. -rewrite Zpos_succ_morphism; unfold Zsucc. -rewrite Zplus_comm; rewrite Zminus_plus. +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. @@ -134,18 +152,18 @@ 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 => refl_equal (S m) + | 0 => eq_refl (S m) | S n1 => let v := S (S n1 + m) in - eq_ind_r (fun n => S n = v) (refl_equal v) (plusnS n1 m) + 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 => refl_equal 0 + | 0 => eq_refl 0 | S n1 => let v := S n1 in - eq_ind_r (fun n : nat => S n = v) (refl_equal v) (plusn0 n1) + eq_ind_r (fun n : nat => S n = v) (eq_refl v) (plusn0 n1) end. Fixpoint diff (m n: nat) {struct m}: nat * nat := @@ -159,8 +177,8 @@ 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 => refl_equal _ - | S n0 => refl_equal _ + | 0 => eq_refl _ + | S n0 => eq_refl _ end | S m1 => match n return (fst (diff (S m1) n) + n = max (S m1) n) @@ -170,7 +188,7 @@ Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n := 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) (refl_equal v1) (S v) (plusnS _ _)) + (eq_ind v1 (fun n => v1 = n) (eq_refl v1) (S v) (plusnS _ _)) _ (diff_l _ _) end end. @@ -179,17 +197,17 @@ 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 => refl_equal _ + | 0 => eq_refl _ | S _ => plusn0 _ end | S m => match n return (snd (diff (S m) n) + S m = max (S m) n) with - | 0 => refl_equal (snd (diff (S m) 0) + S m) + | 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) - (refl_equal v) (diff_r _ _)) (plusnS _ _) + (eq_refl v) (diff_r _ _)) (plusnS _ _) end end. @@ -198,7 +216,7 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n := 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 - | refl_equal => x + | eq_refl => x end. Variable m: nat. @@ -212,8 +230,8 @@ Fixpoint extend_tr (n : nat) {struct n}: (word w (S (n + m))) := End ExtendMax. -Implicit Arguments extend_tr[w m]. -Implicit Arguments castm[w m n]. +Arguments extend_tr [w m] v n. +Arguments castm [w m n] H x. @@ -287,11 +305,7 @@ Section CompareRec. Variable w_to_Z: w -> Z. Variable w_to_Z_0: w_to_Z w_0 = 0. Variable spec_compare0_m: forall x, - match compare0_m x with - Eq => w_to_Z w_0 = wm_to_Z x - | Lt => w_to_Z w_0 < wm_to_Z x - | Gt => w_to_Z w_0 > wm_to_Z x - end. + 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. @@ -300,7 +314,7 @@ Section CompareRec. Lemma base_xO: forall n, base (xO n) = (base n)^2. Proof. intros n1; unfold base. - rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith. + 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 := @@ -308,29 +322,25 @@ Section CompareRec. Lemma spec_compare0_mn: forall n x, - match compare0_mn n x with - Eq => 0 = double_to_Z n x - | Lt => 0 < double_to_Z n x - | Gt => 0 > double_to_Z n x - end. - Proof. + compare0_mn n x = (0 ?= double_to_Z n x). + Proof. intros n; elim n; clear n; auto. - intros x; generalize (spec_compare0_m x); rewrite w_to_Z_0; 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. - generalize (Hrec xh); case compare0_mn; auto. - generalize (Hrec xl); case compare0_mn; auto. - simpl double_to_Z; intros H1 H2; rewrite H1; rewrite <- H2; auto. - simpl double_to_Z; intros H1 H2; rewrite <- H2; auto. + 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. - intros H1; simpl double_to_Z. - set (u := DoubleBase.double_wB wm_base n). - case (double_to_Z_pos n xl); intros H2 H3. - assert (0 < u); auto with zarith. - unfold u, DoubleBase.double_wB, base; auto with zarith. - change 0 with (0 + 0); apply Zplus_lt_le_compat; auto with zarith. - apply Zmult_lt_0_compat; auto with zarith. - case (double_to_Z_pos n xh); 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 := @@ -348,17 +358,9 @@ Section CompareRec. end. Variable spec_compare: forall x y, - match compare x y with - Eq => w_to_Z x = w_to_Z y - | Lt => w_to_Z x < w_to_Z y - | Gt => w_to_Z x > w_to_Z y - end. + compare x y = Z.compare (w_to_Z x) (w_to_Z y). Variable spec_compare_m: forall x y, - match compare_m x y with - Eq => wm_to_Z x = w_to_Z y - | Lt => wm_to_Z x < w_to_Z y - | Gt => wm_to_Z x > w_to_Z y - end. + 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). @@ -367,39 +369,36 @@ Section CompareRec. Proof. intros n x; elim n; simpl; auto; clear n. intros n (H0, H); split; auto. - apply Zlt_le_trans with (1:= H). + apply Z.lt_le_trans with (1:= H). unfold double_wB, DoubleBase.double_wB; simpl. - rewrite base_xO. - set (u := base (double_digits wm_base n)). + rewrite Pshiftl_nat_S, 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 Zle_trans with (1 * u); auto with zarith. - unfold Zpower_pos; simpl; ring. + 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, - match compare_mn_1 n x y with - Eq => double_to_Z n x = w_to_Z y - | Lt => double_to_Z n x < w_to_Z y - | Gt => double_to_Z n x > w_to_Z y - end. + 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; generalize (spec_compare w_0 y); rewrite w_to_Z_0; case compare; auto. - intros xh xl y; simpl; generalize (spec_compare0_mn n xh); case compare0_mn; intros H1b. - rewrite <- H1b; rewrite Zmult_0_l; rewrite Zplus_0_l; auto. - apply Hrec. - apply Zlt_gt. + 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 Zlt_le_trans with (1:= H0). + apply Z.lt_le_trans with (1:= H0). fold double_wB. case (double_to_Z_pos n xl); intros H1 H2. - apply Zle_trans with (double_to_Z n xh * double_wB n); auto with zarith. - apply Zle_trans with (1 * double_wB n); auto with zarith. - case (double_to_Z_pos n xh); auto with zarith. + 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. @@ -433,22 +432,6 @@ Section AddS. End AddS. - - Lemma spec_opp: forall u x y, - match u with - | Eq => y = x - | Lt => y < x - | Gt => y > x - end -> - match CompOpp u with - | Eq => x = y - | Lt => x < y - | Gt => x > y - end. - Proof. - intros u x y; case u; simpl; auto with zarith. - Qed. - Fixpoint length_pos x := match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end. @@ -457,8 +440,8 @@ End AddS. 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 (Zpos_xI x1) || rewrite (Zpos_xO x1)); - try (rewrite (Zpos_xI y1) || rewrite (Zpos_xO y1)); + 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. @@ -474,34 +457,112 @@ End AddS. Variable w: Type. - Theorem digits_zop: forall w (x: znz_op w), - znz_digits (mk_zn2z_op x) = xO (znz_digits x). + 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 w (x: znz_op w), - znz_digits (mk_zn2z_op_karatsuba x) = xO (znz_digits x). + 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 w (x: znz_op w), - znz_to_Z (mk_zn2z_op x) = + 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 x xh * base (znz_digits x) - + znz_to_Z x xl + | 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 w (x: znz_op w), - znz_to_Z (mk_zn2z_op_karatsuba x) = + 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 x xh * base (znz_digits x) - + znz_to_Z x xl + | 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. |