diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN/Nbasic.v')
| -rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 323 |
1 files changed, 192 insertions, 131 deletions
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. |