diff options
Diffstat (limited to 'coqprime/num/Mod_op.v')
| -rw-r--r-- | coqprime/num/Mod_op.v | 1200 |
1 files changed, 1200 insertions, 0 deletions
diff --git a/coqprime/num/Mod_op.v b/coqprime/num/Mod_op.v new file mode 100644 index 000000000..a8f25bd2d --- /dev/null +++ b/coqprime/num/Mod_op.v @@ -0,0 +1,1200 @@ + +(*************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(*************************************************************) +(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) +(*************************************************************) + +Set Implicit Arguments. + +Require Import DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv. +Require Import CyclicAxioms DoubleCyclic BigN Cyclic31. +Require Import ZArith ZCAux. +Import CyclicAxioms DoubleType DoubleBase. + +Theorem Zpos_pos: forall x, 0 < Zpos x. +red; simpl; auto. +Qed. +Hint Resolve Zpos_pos: zarith. + +Section Mod_op. + + Variable w : Type. + + Record mod_op : Type := mk_mod_op { + succ_mod : w -> w; + add_mod : w -> w -> w; + pred_mod : w -> w; + sub_mod : w -> w -> w; + mul_mod : w -> w -> w; + square_mod : w -> w; + power_mod : w -> positive -> w + }. + + Variable w_op : ZnZ.Ops w. + + Let w_digits := w_op.(ZnZ.digits). + Let w_zdigits := w_op.(ZnZ.zdigits). + Let w_to_Z := (@ZnZ.to_Z _ w_op). + Let w_of_pos := (@ZnZ.of_pos _ w_op). + Let w_head0 := (@ZnZ.head0 _ w_op). + Let w0 := (@ZnZ.zero _ w_op). + Let w1 := (@ZnZ.one _ w_op). + Let wBm1 := (@ZnZ.minus_one _ w_op). + + Let wWW := (@ZnZ.WW _ w_op). + Let wW0 := (@ZnZ.WO _ w_op). + Let w0W := (@ZnZ.OW _ w_op). + + Let w_compare := (@ZnZ.compare _ w_op). + Let w_opp_c := (@ZnZ.opp_c _ w_op). + Let w_opp := (@ZnZ.opp _ w_op). + Let w_opp_carry := (@ZnZ.opp_carry _ w_op). + + Let w_succ := (@ZnZ.succ _ w_op). + Let w_succ_c := (@ZnZ.succ_c _ w_op). + Let w_add_c := (@ZnZ.add_c _ w_op). + Let w_add_carry_c := (@ZnZ.add_carry_c _ w_op). + Let w_add := (@ZnZ.add _ w_op). + + + Let w_pred_c := (@ZnZ.pred_c _ w_op). + Let w_sub_c := (@ZnZ.sub_c _ w_op). + Let w_sub_carry := (@ZnZ.sub_carry _ w_op). + Let w_sub_carry_c := (@ZnZ.sub_carry_c _ w_op). + Let w_sub := (@ZnZ.sub _ w_op). + Let w_pred := (@ZnZ.pred _ w_op). + + Let w_mul_c := (@ZnZ.mul_c _ w_op). + Let w_mul := (@ZnZ.mul _ w_op). + Let w_square_c := (@ZnZ.square_c _ w_op). + + Let w_div21 := (@ZnZ.div21 _ w_op). + Let w_add_mul_div := (@ZnZ.add_mul_div _ w_op). + + Variable b : w. + (* b should be > 1 *) + Let n := w_head0 b. + + Let b2n := w_add_mul_div n b w0. + + Let bm1 := w_sub b w1. + + Let mb := w_opp b. + + Let wwb := WW w0 b. + + Let low x := match x with WW _ x => x | W0 => w0 end. + + Let w_add2 x y := match w_add_c x y with + C0 n => WW w0 n + |C1 n => WW w1 n + end. + Let ww_zdigits := w_add2 w_zdigits w_zdigits. + + Let ww_compare := + Eval lazy beta delta [ww_compare] in ww_compare w0 w_compare. + + Let ww_sub := + Eval lazy beta delta [ww_sub] in + ww_sub w0 wWW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry. + + Let ww_add_mul_div := + Eval lazy beta delta [ww_add_mul_div] in + ww_add_mul_div w0 wWW wW0 w0W + ww_compare w_add_mul_div + ww_sub w_zdigits low (w0W n). + + Let ww_lsl_n := + Eval lazy beta delta [ww_add_mul_div] in + fun ww => ww_add_mul_div ww W0. + + Let w_lsr_n w := + w_add_mul_div (w_sub w_zdigits n) w0 w. + + Open Scope Z_scope. + Notation "[| x |]" := + (@ZnZ.to_Z _ w_op x) (at level 0, x at level 99). + +Notation "[[ x ]]" := + (@ww_to_Z _ w_digits w_to_Z x) (at level 0, x at level 99). + + Section Mod_spec. + + Variable m_op : mod_op. + + Record mod_spec : Prop := mk_mod_spec { + succ_mod_spec : + forall w t, [|w|]= t mod [|b|] -> + [|succ_mod m_op w|] = ([|w|] + 1) mod [|b|]; + add_mod_spec : + forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] -> + [|add_mod m_op w1 w2|] = ([|w1|] + [|w2|]) mod [|b|]; + pred_mod_spec : + forall w t, [|w|]= t mod [|b|] -> + [|pred_mod m_op w|] = ([|w|] - 1) mod [|b|]; + sub_mod_spec : + forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] -> + [|sub_mod m_op w1 w2|] = ([|w1|] - [|w2|]) mod [|b|]; + mul_mod_spec : + forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] -> + [|mul_mod m_op w1 w2|] = ([|w1|] * [|w2|]) mod [|b|]; + square_mod_spec : + forall w t, [|w|]= t mod [|b|] -> + [|square_mod m_op w|] = ([|w|] * [|w|]) mod [|b|]; + power_mod_spec : + forall w t p, [|w|]= t mod [|b|] -> + [|power_mod m_op w p|] = (Zpower_pos [|w|] p) mod [|b|] +(* + shift_spec : + forall w p, wf w -> + [|shift m_op w p|] = ([|w|] / (Zpower_pos 2 p)) mod [|b|]; + trunc_spec : + forall w p, wf w -> + [|power_mod m_op w p|] = ([|w1|] mod (Zpower_pos 2 p)) mod [|b|] +*) + }. + + End Mod_spec. + + Hypothesis b_pos: 1 < [|b|]. + Variable op_spec: ZnZ.Specs w_op. + + + Lemma Zpower_n: 0 < 2 ^ [|n|]. + apply Zpower_gt_0; auto with zarith. + case (ZnZ.spec_to_Z n); auto with zarith. + Qed. + + Hint Resolve Zpower_n Zmult_lt_0_compat Zpower_gt_0. + + Variable m_op : mod_op. + + Hint Rewrite + ZnZ.spec_0 + ZnZ.spec_1 + ZnZ.spec_m1 + ZnZ.spec_WW + ZnZ.spec_opp_c + ZnZ.spec_opp + ZnZ.spec_opp_carry + ZnZ.spec_succ_c + ZnZ.spec_add_c + ZnZ.spec_add_carry_c + ZnZ.spec_add + ZnZ.spec_pred_c + ZnZ.spec_sub_c + ZnZ.spec_sub_carry_c + ZnZ.spec_sub + ZnZ.spec_mul_c + ZnZ.spec_mul + : w_rewrite. + + Let _succ_mod x := + let res :=w_succ x in + match w_compare res b with + | Lt => res + | _ => w0 + end. + + Let split x := + match x with + | W0 => (w0,w0) + | WW h l => (h,l) + end. + + Let _w0_is_0: [|w0|] = 0. + unfold ZnZ.to_Z; rewrite <- ZnZ.spec_0; auto. + Qed. + + Let _w1_is_1: [|w1|] = 1. + unfold ZnZ.to_Z; rewrite <-ZnZ.spec_1; simpl; auto. + Qed. + + Theorem Zmod_plus_one: forall a1 b1, 0 < b1 -> (a1 + b1) mod b1 = a1 mod b1. + intros a1 b1 H; rewrite Zplus_mod; auto with zarith. + rewrite Z_mod_same; try rewrite Zplus_0_r; auto with zarith. + apply Zmod_mod; auto. + Qed. + + Theorem Zmod_minus_one: forall a1 b1, 0 < b1 -> (a1 - b1) mod b1 = a1 mod b1. + intros a1 b1 H; rewrite Zminus_mod; auto with zarith. + rewrite Z_mod_same; try rewrite Zminus_0_r; auto with zarith. + apply Zmod_mod; auto. + Qed. + + Lemma without_c_b: forall w2, [|w2|] < [|b|] -> + [|w_succ w2|] = [|w2|] + 1. + intros w2 H. + unfold w_succ;rewrite ZnZ.spec_succ. + rewrite Zmod_small;auto. + assert (HH := ZnZ.spec_to_Z w2). + assert (HH' := ZnZ.spec_to_Z b);auto with zarith. + Qed. + + Lemma _succ_mod_spec: forall w t, [|w|]= t mod [|b|] -> + [|_succ_mod w|] = ([|w|] + 1) mod [|b|]. + intros w2 t H; unfold _succ_mod, w_compare; simpl. + assert (F: [|w2|] < [|b|]). + case (Z_mod_lt t [|b|]); auto with zarith. + rewrite ZnZ.spec_compare; case Zcompare_spec; intros H1; + match goal with H: context[w_succ _] |- _ => + generalize H; clear H; rewrite (without_c_b _ F); intros H1; + auto with zarith + end. + rewrite H1, Z_mod_same, _w0_is_0; auto with zarith. + rewrite Zmod_small; auto with zarith. + case (ZnZ.spec_to_Z w2); auto with zarith. + Qed. + + Let _add_mod x y := + match w_add_c x y with + | C0 z => + match w_compare z b with + | Lt => z + | Eq => w0 + | Gt => w_sub z b + end + | C1 z => w_add mb z + end. + + Lemma _add_mod_correct: forall w1 w2, [|w1|] + [|w2|] < 2 * [|b|] -> + [|_add_mod w1 w2|] = ([|w1|] + [|w2|]) mod [|b|]. + intros w2 w3; unfold _add_mod, w_compare, w_add_c; intros H. + match goal with |- context[ZnZ.add_c ?x ?y] => + generalize (ZnZ.spec_add_c x y); unfold interp_carry; + case (ZnZ.add_c x y); autorewrite with w_rewrite + end; auto with zarith. + intros w4 H2. + rewrite ZnZ.spec_compare; case Zcompare_spec; intros H1; + match goal with H: context[b] |- _ => + generalize H; clear H; intros H1; rewrite <-H2; + auto with zarith + end. + rewrite H1, Z_mod_same; auto with zarith. + rewrite Zmod_small; auto with zarith. + case (ZnZ.spec_to_Z w4); auto with zarith. + assert (F1: 0 < [|w4|] - [|b|]); auto with zarith. + assert (F2: [|w4|] < [|b|] + [|b|]); auto with zarith. + autorewrite with w_rewrite; auto. + rewrite (fun x y => Zmod_small (x - y)); auto with zarith. + rewrite <- (Zmod_minus_one [|w4|]); auto with zarith. + apply sym_equal; apply Zmod_small; auto with zarith. + split; auto with zarith. + apply Zlt_trans with [|b|]; auto with zarith. + case (ZnZ.spec_to_Z b); unfold base; auto with zarith. + rewrite Zmult_1_l; intros w4 H2; rewrite <- H2. + unfold mb, w_add; rewrite ZnZ.spec_add; auto with zarith. + assert (F1: [|w4|] < [|b|]). + assert (F2: base (ZnZ.digits w_op) + [|w4|] < base (ZnZ.digits w_op) + [|b|]); + auto with zarith. + rewrite H2. + apply Zlt_trans with ([|b|] +[|b|]); auto with zarith. + apply Zplus_lt_compat_r; auto with zarith. + case (ZnZ.spec_to_Z b); auto with zarith. + assert (F2: [|b|] < base (ZnZ.digits w_op) + [|w4|]); auto with zarith. + apply Zlt_le_trans with (base (ZnZ.digits w_op)); auto with zarith. + case (ZnZ.spec_to_Z b); auto with zarith. + case (ZnZ.spec_to_Z w4); auto with zarith. + assert (F3: base (ZnZ.digits w_op) + [|w4|] < [|b|] + [|b|]); auto with zarith. + rewrite <- (fun x => Zmod_minus_one (base x + [|w4|])); auto with zarith. + rewrite (fun x y => Zmod_small (x - y)); auto with zarith. + unfold w_opp;rewrite (ZnZ.spec_opp b). + rewrite <- (fun x => Zmod_plus_one (-x)); auto with zarith. + rewrite (Zmod_small (- [|b|] + base (ZnZ.digits w_op)));auto with zarith. + 2 : assert (HHH := ZnZ.spec_to_Z b);auto with zarith. + repeat rewrite Zmod_small; auto with zarith. + Qed. + + Lemma _add_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] -> + [|_add_mod w1 w2|] = ([|w1|] + [|w2|]) mod [|b|]. + intros w2 w3 t1 t2 H H1. + apply _add_mod_correct; auto with zarith. + assert (F: [|w2|] < [|b|]). + case (Z_mod_lt t1 [|b|]); auto with zarith. + assert (F': [|w3|] < [|b|]). + case (Z_mod_lt t2 [|b|]); auto with zarith. + assert (tmp: forall x, 2 * x = x + x); auto with zarith. + Qed. + + Let _pred_mod x := + match w_compare w0 x with + | Eq => bm1 + | _ => w_pred x + end. + + Lemma _pred_mod_spec: forall w t, [|w|] = t mod [|b|] -> + [|_pred_mod w|] = ([|w|] - 1) mod [|b|]. + intros w2 t H; unfold _pred_mod, w_compare, bm1; simpl. + assert (F: [|w2|] < [|b|]). + case (Z_mod_lt t [|b|]); auto with zarith. + rewrite ZnZ.spec_compare; case Zcompare_spec; intros H1; + match goal with H: context[w2] |- _ => + generalize H; clear H; intros H1; autorewrite with w_rewrite; + auto with zarith + end; try rewrite _w0_is_0; try rewrite _w1_is_1; auto with zarith. + rewrite <- H1, _w0_is_0; simpl. + rewrite <- (Zmod_plus_one (-1)); auto with zarith. + repeat rewrite Zmod_small; auto with zarith. + case (ZnZ.spec_to_Z b); auto with zarith. + unfold w_pred;rewrite ZnZ.spec_pred; auto. + assert (HHH := ZnZ.spec_to_Z b);repeat rewrite Zmod_small;auto with + zarith. + intros;assert (HHH := ZnZ.spec_to_Z w2);auto with zarith. + Qed. + + Let _sub_mod x y := + match w_sub_c x y with + | C0 z => z + | C1 z => w_add z b + end. + + Lemma _sub_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] -> + [|_sub_mod w1 w2|] = ([|w1|] - [|w2|]) mod [|b|]. + intros w2 w3 t1 t2; unfold _sub_mod, w_compare, w_sub_c; intros H H1. + assert (F: [|w2|] < [|b|]). + case (Z_mod_lt t1 [|b|]); auto with zarith. + assert (F': [|w3|] < [|b|]). + case (Z_mod_lt t2 [|b|]); auto with zarith. + match goal with |- context[ZnZ.sub_c ?x ?y] => + generalize (ZnZ.spec_sub_c x y); unfold interp_carry; + case (ZnZ.sub_c x y); autorewrite with w_rewrite + end; auto with zarith. + intros w4 H2. + rewrite Zmod_small; auto with zarith. + split; auto with zarith. + rewrite <- H2; case (ZnZ.spec_to_Z w4); auto with zarith. + apply Zle_lt_trans with [|w2|]; auto with zarith. + case (ZnZ.spec_to_Z w3); auto with zarith. + intros w4 H2; rewrite <- H2. + unfold w_add; rewrite ZnZ.spec_add; auto with zarith. + case (ZnZ.spec_to_Z w4); intros F1 F2. + assert (F3: 0 <= - 1 * base (ZnZ.digits w_op) + [|w4|] + [|b|]); auto with zarith. + rewrite H2. + case (ZnZ.spec_to_Z w3); case (ZnZ.spec_to_Z w2); auto with zarith. + rewrite <- (fun x => Zmod_minus_one ([|w4|] + x)); auto with zarith. + rewrite <- (fun x y => Zmod_plus_one (-y + x)); auto with zarith. + repeat rewrite Zmod_small; auto with zarith. + case (ZnZ.spec_to_Z b); auto with zarith. + Qed. + + Let _mul_mod x y := + let xy := w_mul_c x y in + match ww_compare xy wwb with + | Lt => snd (split xy) + | Eq => w0 + | Gt => + let xy2n := ww_lsl_n xy in + let (h,l) := split xy2n in + let (q,r) := w_div21 h l b2n in + w_lsr_n r + end. + + Theorem high_zero:forall x, [[x]] < base w_digits -> [|fst (split x)|] = 0. + intros x; case x; simpl; auto. + intros xh xl H; case (Zle_lt_or_eq 0 [|xh|]); auto with zarith. + case (ZnZ.spec_to_Z xh); auto with zarith. + intros H1; contradict H; apply Zle_not_lt. + assert (HHHH := wB_pos w_digits). + unfold w_to_Z. + match goal with |- ?X <= ?Y + ?Z => + pattern X at 1; rewrite <- (Zmult_1_l X); auto with zarith; + apply Zle_trans with Y; auto with zarith + end. + case (ZnZ.spec_to_Z xl); auto with zarith. + Qed. + + Theorem n_spec: base (ZnZ.digits w_op) / 2 <= 2 ^ [|n|] * [|b|] + < base (ZnZ.digits w_op). + unfold n, w_head0; apply (ZnZ.spec_head0); auto with zarith. + Qed. + + Theorem b2n_spec: [|b2n|] = 2 ^ [|n|] * [|b|]. + unfold b2n, w_add_mul_div; case n_spec; intros Hp Hp1. + assert (F1: [|n|] < Zpos (ZnZ.digits w_op)). + case (Zle_or_lt (Zpos (ZnZ.digits w_op)) [|n|]); auto with zarith. + intros H1; contradict Hp1; apply Zle_not_lt; unfold base. + apply Zle_trans with (2 ^ [|n|] * 1); auto with zarith. + rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith. + rewrite ZnZ.spec_add_mul_div; auto with zarith. + rewrite _w0_is_0; rewrite Zdiv_0_l; auto with zarith. + rewrite Zplus_0_r; rewrite Zmult_comm; apply Zmod_small; auto with zarith. + Qed. + + Theorem ww_lsl_n_spec: forall w, [[w]] < [|b|] * [|b|] -> + [[ww_lsl_n w]] = 2 ^ [|n|] * [[w]]. + intros w2 H; unfold ww_lsl_n. + case n_spec; intros Hp Hp1. + assert (F0: forall x, 2 * x = x + x); auto with zarith. + assert (F1: [|n|] < Zpos (ZnZ.digits w_op)). + case (Zle_or_lt (Zpos (ZnZ.digits w_op)) [|n|]); auto. + intros H1; contradict Hp1; apply Zle_not_lt; unfold base. + apply Zle_trans with (2 ^ [|n|] * 1); auto with zarith. + rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith. + assert (F2: [|n|] < Zpos (xO (ZnZ.digits w_op))). + rewrite (Zpos_xO (ZnZ.digits w_op)); rewrite F0; auto with zarith. + pattern [|n|]; rewrite <- Zplus_0_r; auto with zarith. + apply Zplus_lt_compat; auto with zarith. + change + ([[DoubleLift.ww_add_mul_div w0 wWW wW0 w0W + ww_compare w_add_mul_div + ww_sub w_zdigits low (w0W n) w2 W0]] = 2 ^ [|n|] * [[w2]]). + rewrite (DoubleLift.spec_ww_add_mul_div ); auto with zarith. + 2: apply ZnZ.spec_to_Z; auto. + 2: refine (spec_ww_to_Z _ _ _); auto. + 2: apply ZnZ.spec_to_Z; auto. + 2: apply ZnZ.spec_WW; auto. + 2: apply ZnZ.spec_WO; auto. + 2: apply ZnZ.spec_OW; auto. + 2: refine (spec_ww_compare _ _ _ _ _ _ _); auto. + 2: apply ZnZ.spec_to_Z; auto. + 2: apply ZnZ.spec_compare; auto. + 2: apply ZnZ.spec_add_mul_div; auto. + 2: refine (spec_ww_sub _ _ _ _ _ _ _ _ _ _ + _ _ _ _ _ _ _ _ _ _ _); auto. + 2: apply ZnZ.spec_to_Z; auto. + 2: apply ZnZ.spec_WW; auto. + 2: apply ZnZ.spec_opp_c; auto. + 2: apply ZnZ.spec_opp; auto. + 2: apply ZnZ.spec_opp_carry; auto. + 2: apply ZnZ.spec_sub_c; auto. + 2: apply ZnZ.spec_sub; auto. + 2: apply ZnZ.spec_sub_carry; auto. + 2: apply ZnZ.spec_zdigits; auto. + replace ([[w0W n]]) with [|n|]. + change [[W0]] with 0. rewrite Zdiv_0_l; auto with zarith. + rewrite Zplus_0_r; rewrite Zmod_small; auto with zarith. + split; auto with zarith. + case spec_ww_to_Z with (w_digits := w_digits) (w_to_Z := w_to_Z) (x:=w2); auto with zarith. + apply ZnZ.spec_to_Z; auto. + apply Zlt_trans with ([|b|] * [|b|] * 2 ^ [|n|]); auto with zarith. + apply Zmult_lt_compat_r; auto with zarith. + rewrite <- Zmult_assoc. + unfold base; unfold base in Hp. + unfold ww_digits,w_digits;rewrite (Zpos_xO (ZnZ.digits w_op)); rewrite F0; auto with zarith. + rewrite Zpower_exp; auto with zarith. + apply Zmult_lt_compat; auto with zarith. + case (ZnZ.spec_to_Z b); auto with zarith. + split; auto with zarith. + rewrite Zmult_comm; auto with zarith. + unfold w_digits;auto with zarith. + generalize (ZnZ.spec_OW n). + unfold ww_to_Z, w_digits; auto. + intros x; case x; simpl. + unfold w_to_Z, w_digits, w0; rewrite ZnZ.spec_0; auto. + intros w3 w4; rewrite Zplus_comm. + rewrite Z_mod_plus; auto with zarith. + rewrite Zmod_small; auto with zarith. + case (ZnZ.spec_to_Z w4); auto with zarith. + unfold base; auto with zarith. + unfold ww_to_Z, w_digits, w_to_Z, w0W; auto. + rewrite ZnZ.spec_OW; auto with zarith. + Qed. + + Theorem w_lsr_n_spec: forall w, [|w|] < 2 ^ [|n|] * [|b|]-> + [|w_lsr_n w|] = [|w|] / 2 ^ [|n|]. + intros w2 H. + case (ZnZ.spec_to_Z w2); intros U1 U2. + unfold w_lsr_n, w_add_mul_div. + rewrite ZnZ.spec_add_mul_div; auto with zarith. + rewrite _w0_is_0; rewrite Zmult_0_l; auto with zarith. + rewrite Zplus_0_l. + autorewrite with w_rewrite; auto. + rewrite (fun x y => Zmod_small (x - y)); auto with zarith. + unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto. + assert (tmp: forall p q, p - (p - q) = q); intros; try ring; + rewrite tmp; clear tmp; auto. + rewrite Zmod_small; auto with zarith. + split; auto with zarith. + apply Zle_lt_trans with (2 := U2); auto with zarith. + apply Zdiv_le_upper_bound; auto with zarith. + apply Zle_trans with ([|w2|] * (2 ^ 0)); auto with zarith. + simpl Zpower; rewrite Zmult_1_r; auto with zarith. + apply Zmult_le_compat_l; auto with zarith. + apply Zpower_le_monotone; auto with zarith. + case (ZnZ.spec_to_Z n); auto with zarith. + unfold n. + assert (HH: 0 < [|b|]); auto with zarith. + split. + case (Zle_or_lt [|w_head0 b|] [|w_zdigits|]); auto with zarith. + unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto; intros H1. + case (ZnZ.spec_head0 b HH); intros _ H2; contradict H2. + apply Zle_not_lt; unfold base. + apply Zle_trans with (2^[|ZnZ.head0 b|] * 1); auto with zarith. + rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith. + unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto. + apply Zle_lt_trans with (Zpos (ZnZ.digits w_op)); auto with zarith. + case (ZnZ.spec_to_Z (w_head0 b)); auto with zarith. + unfold base; apply Zpower2_lt_lin; auto with zarith. + autorewrite with w_rewrite; auto. + rewrite Zmod_small; auto with zarith. + unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto with zarith. + case (ZnZ.spec_to_Z n); auto with zarith. + unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto. + split; auto with zarith. + case (Zle_or_lt [|n|] (Zpos (ZnZ.digits w_op))); auto with zarith; intros H1. + case (ZnZ.spec_head0 b); auto with zarith; intros _ H2. + contradict H2; apply Zle_not_lt; auto with zarith. + unfold base; apply Zle_trans with (2 ^ [|ZnZ.head0 b|] * 1); + auto with zarith. + rewrite Zmult_1_r; unfold base; apply Zpower_le_monotone; auto with zarith. + apply Zle_lt_trans with (Zpos (ZnZ.digits w_op)); auto with zarith. + case (ZnZ.spec_to_Z n); auto with zarith. + unfold base; apply Zpower2_lt_lin; auto with zarith. + Qed. + + Lemma split_correct: forall x, let (xh, xl) := split x in [[WW xh xl]] = [[x]]. + intros x; case x; simpl; unfold w0, w_to_Z;try rewrite ZnZ.spec_0; auto with zarith. + Qed. + + Lemma _mul_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] -> + [|_mul_mod w1 w2|] = ([|w1|] * [|w2|]) mod [|b|]. + intros w2 w3 t1 t2 H H1; unfold _mul_mod, wwb. + assert (F: [|w2|] < [|b|]). + case (Z_mod_lt t1 [|b|]); auto with zarith. + assert (F': [|w3|] < [|b|]). + case (Z_mod_lt t2 [|b|]); auto with zarith. + match goal with |- context[ww_compare ?x ?y] => + change (ww_compare x y) with (DoubleBase.ww_compare w0 w_compare x y) + end. + rewrite (@spec_ww_compare w w0 w_digits w_to_Z w_compare + ZnZ.spec_0 ZnZ.spec_to_Z ZnZ.spec_compare + (w_mul_c w2 w3) (WW w0 b)); case Zcompare_spec; intros H2; + match goal with H: context[w_mul_c] |- _ => + generalize H; clear H + end; try rewrite _w0_is_0; try rewrite !_w1_is_1; auto with zarith. + unfold w_mul_c, ww_to_Z, w_to_Z, w_digits; rewrite ZnZ.spec_mul_c; auto with zarith. + simpl; rewrite _w0_is_0, Zmult_0_l, Zplus_0_l. + intros H2; rewrite H2; simpl. + rewrite Z_mod_same; auto with zarith. + generalize (high_zero (w_mul_c w2 w3)). + unfold w_mul_c; generalize (ZnZ.spec_mul_c w2 w3); + case (ZnZ.mul_c w2 w3); simpl; auto with zarith. + intros H3 _ _; rewrite <- H3; autorewrite with w_rewrite; auto. +(* rewrite Zmod_small; auto with zarith. *) + intros w4 w5. + change (w_to_Z w0) with [|w0|]; rewrite _w0_is_0. + change (w_to_Z w4) with [|w4|]. + change (w_to_Z w5) with [|w5|]. + simpl. + intros H2 H3 H4. + assert (E1: [|w4|] = 0). + apply H3; auto with zarith. + apply Zlt_trans with (1 := H4). + case (ZnZ.spec_to_Z b); auto with zarith. + generalize H4 H2; rewrite E1; rewrite Zmult_0_l; rewrite Zplus_0_l; + clear H4 H2; intros H4 H2. + rewrite <- H2; rewrite Zmod_small; auto with zarith. + case (ZnZ.spec_to_Z w5); auto with zarith. + intros H2. + match goal with |- context[split ?x] => + generalize (split_correct x); + case (split x); auto with zarith + end. + assert (F1: [[w_mul_c w2 w3]] < [|b|] * [|b|]). + unfold w_to_Z, w_mul_c, ww_to_Z,w_digits; + rewrite ZnZ.spec_mul_c; auto with zarith. + apply Zmult_lt_compat; auto with zarith. + case (ZnZ.spec_to_Z w2); auto with zarith. + case (ZnZ.spec_to_Z w3); auto with zarith. + intros w4 w5; rewrite ww_lsl_n_spec; auto with zarith. + intros H3. + unfold w_div21; match goal with |- context[ZnZ.div21 ?y ?z ?t] => + generalize (ZnZ.spec_div21 y z t); + case (ZnZ.div21 y z t) + end. + rewrite b2n_spec; case (n_spec); auto. + intros H4 H5 w6 w7 H6. + case H6; auto with zarith. + case (Zle_or_lt (2 ^ [|n|] * [|b|]) [|w4|]); auto; intros H7. + match type of H3 with ?X = ?Y => + absurd (Y < X) + end. + apply Zle_not_lt; rewrite H3; auto with zarith. + simpl ww_to_Z. + match goal with |- ?X < ?Y + _ => + apply Zlt_le_trans with Y; auto with zarith + end. + apply Zlt_trans with (2 ^ [|n|] * ([|b|] * [|b|])); + auto with zarith. + apply Zmult_lt_compat_l; auto with zarith. + rewrite Zmult_assoc. + apply Zmult_lt_compat2; auto with zarith. + case (ZnZ.spec_to_Z b); auto with zarith. + case (ZnZ.spec_to_Z w5); unfold w_to_Z;auto with zarith. + clear H6; intros H7 H8. + rewrite w_lsr_n_spec; auto with zarith. + rewrite <- (Z_div_mult ([|w2|] * [|w3|]) (2 ^ [|n|])); + auto with zarith; rewrite Zmult_comm. + rewrite <- ZnZ.spec_mul_c; auto with zarith. + unfold w_mul_c in H3; unfold ww_to_Z in H3;simpl H3. + unfold w_digits,w_to_Z in H3. rewrite <- H3; simpl. + rewrite H7; rewrite (fun x => Zmult_comm (2 ^ x)); + rewrite Zmult_assoc; rewrite BigNumPrelude.Z_div_plus_l; auto with zarith. + rewrite Zplus_mod; auto with zarith. + rewrite Z_mod_mult; auto with zarith. + rewrite Zplus_0_l; auto with zarith. + rewrite Zmod_mod; auto with zarith. + rewrite Zmod_small; auto with zarith. + split; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + rewrite Zmult_comm; auto with zarith. + Qed. + + Let _square_mod x := + let x2 := w_square_c x in + match ww_compare x2 wwb with + | Lt => snd (split x2) + | Eq => w0 + | Gt => + let x2_2n := ww_lsl_n x2 in + let (h,l) := split x2_2n in + let (q,r) := w_div21 h l b2n in + w_lsr_n r + end. + + Lemma _square_mod_spec: forall w t, [|w|] = t mod [|b|] -> + [|_square_mod w|] = ([|w|] * [|w|]) mod [|b|]. + intros w2 t2 H; unfold _square_mod, wwb. + assert (F: [|w2|] < [|b|]). + case (Z_mod_lt t2 [|b|]); auto with zarith. + match goal with |- context[ww_compare ?x ?y] => + change (ww_compare x y) with (DoubleBase.ww_compare w0 w_compare x y) + end. + rewrite (@spec_ww_compare w w0 w_digits w_to_Z w_compare + ZnZ.spec_0 ZnZ.spec_to_Z ZnZ.spec_compare); case Zcompare_spec; + intros H2; + match goal with H: context[w_square_c] |- _ => + generalize H; clear H + end; autorewrite with w_rewrite; try rewrite _w0_is_0; try rewrite !_w1_is_1; auto with zarith. + unfold w_square_c, ww_to_Z, w_to_Z, w_digits; rewrite ZnZ.spec_square_c; auto with zarith. + intros H2;rewrite H2; simpl. + rewrite _w0_is_0; simpl. + rewrite Z_mod_same; auto with zarith. + generalize (high_zero (w_square_c w2)). + unfold w_square_c; generalize (ZnZ.spec_square_c w2); + case (ZnZ.square_c w2); simpl; auto with zarith. + intros H3 _ _; rewrite <- H3; autorewrite with w_rewrite; auto. + intros w4 w5. + change (w_to_Z w0) with [|w0|]; rewrite _w0_is_0; simpl. + change (w_to_Z w4) with [|w4|]. + change (w_to_Z w5) with [|w5|]. + intros H2 H3 H4. + assert (E1: [|w4|] = 0). + apply H3; auto with zarith. + apply Zlt_trans with (1 := H4). + case (ZnZ.spec_to_Z b); auto with zarith. + generalize H4 H2; rewrite E1; rewrite Zmult_0_l; rewrite Zplus_0_l; + clear H4 H2; intros H4 H2. + rewrite <- H2; rewrite Zmod_small; auto with zarith. + case (ZnZ.spec_to_Z w5); auto with zarith. + intros H2. + match goal with |- context[split ?x] => + generalize (split_correct x); + case (split x); auto with zarith + end. + assert (F1: [[w_square_c w2]] < [|b|] * [|b|]). + unfold w_square_c, ww_to_Z, w_digits, w_to_Z. + rewrite ZnZ.spec_square_c; auto with zarith. + apply Zmult_lt_compat; auto with zarith. + case (ZnZ.spec_to_Z w2); auto with zarith. + case (ZnZ.spec_to_Z w2); auto with zarith. + intros w4 w5; rewrite ww_lsl_n_spec; auto with zarith. + intros H3. + unfold w_div21; match goal with |- context[ZnZ.div21 ?y ?z ?t] => + generalize (ZnZ.spec_div21 y z t); + case (ZnZ.div21 y z t) + end. + rewrite b2n_spec; case (n_spec); auto. + intros H4 H5 w6 w7 H6. + case H6; auto with zarith. + case (Zle_or_lt (2 ^ [|n|] * [|b|]) [|w4|]); auto; intros H7. + match type of H3 with ?X = ?Y => + absurd (Y < X) + end. + apply Zle_not_lt; rewrite H3; auto with zarith. + simpl ww_to_Z. + match goal with |- ?X < ?Y + _ => + apply Zlt_le_trans with Y; auto with zarith + end. + apply Zlt_trans with (2 ^ [|n|] * ([|b|] * [|b|])); + auto with zarith. + apply Zmult_lt_compat_l; auto with zarith. + rewrite Zmult_assoc. + apply Zmult_lt_compat2; auto with zarith. + case (ZnZ.spec_to_Z b); auto with zarith. + unfold w_to_Z,w_digits;case (ZnZ.spec_to_Z w5); auto with zarith. + clear H6; intros H7 H8. + rewrite w_lsr_n_spec; auto with zarith. + rewrite <- (Z_div_mult ([|w2|] * [|w2|]) (2 ^ [|n|])); + auto with zarith; rewrite Zmult_comm. + rewrite <- ZnZ.spec_square_c; auto with zarith. + unfold w_square_c, ww_to_Z in H3; unfold w_digits,w_to_Z in H3. + rewrite <- H3; simpl. + rewrite H7; rewrite (fun x => Zmult_comm (2 ^ x)); + rewrite Zmult_assoc; rewrite BigNumPrelude.Z_div_plus_l; auto with zarith. + rewrite Zplus_mod; auto with zarith. + rewrite Z_mod_mult; auto with zarith. + rewrite Zplus_0_l; auto with zarith. + rewrite Zmod_mod; auto with zarith. + rewrite Zmod_small; auto with zarith. + split; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + rewrite Zmult_comm; auto with zarith. + Qed. + + Let _power_mod := + fix pow_mod (x:w) (p:positive) {struct p} : w := + match p with + | xH => x + | xO p' => + let pow := pow_mod x p' in + _square_mod pow + | xI p' => + let pow := pow_mod x p' in + _mul_mod (_square_mod pow) x + end. + + Lemma _power_mod_spec: forall w t p, [|w|] = t mod [|b|] -> + [|_power_mod w p|] = (Zpower_pos [|w|] p) mod [|b|]. + intros w2 t p; elim p; simpl; auto with zarith. + intros p' Rec H. + assert (F: [|w2|] < [|b|]). + case (Z_mod_lt t [|b|]); auto with zarith. + replace (xI p') with (p' + p' + 1)%positive. + repeat rewrite Zpower_pos_is_exp; auto with zarith. + pose (t1 := [|_power_mod w2 p'|]). + rewrite _mul_mod_spec with (t1 := t1 * t1) + (t2 := t); auto with zarith. + rewrite _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith. + rewrite Rec; auto with zarith. + assert (tmp: forall p, Zpower_pos p 1 = p); try (rewrite tmp; clear tmp). + intros p1; unfold Zpower_pos; simpl; ring. + rewrite <- Zmult_mod; auto with zarith. + rewrite Zmult_mod; auto with zarith. + rewrite Zmod_mod; auto with zarith. + rewrite <- Zmult_mod; auto with zarith. + simpl; unfold t1; apply _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith. + rewrite xI_succ_xO; rewrite <- Pplus_diag. + rewrite Pplus_one_succ_r; auto. + intros p' Rec H. + replace (xO p') with (p' + p')%positive. + repeat rewrite Zpower_pos_is_exp; auto with zarith. + rewrite _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith. + rewrite Rec; auto with zarith. + rewrite <- Zmult_mod; auto with zarith. + rewrite <- Pplus_diag; auto. + intros H. + assert (tmp: forall p, Zpower_pos p 1 = p); try (rewrite tmp; clear tmp). + intros p1; unfold Zpower_pos; simpl; ring. + rewrite Zmod_small; auto with zarith. + assert (F: [|w2|] < [|b|]). + case (Z_mod_lt t [|b|]); auto with zarith. + case (ZnZ.spec_to_Z w2); auto with zarith. + Qed. + + Definition make_mod_op := + mk_mod_op + _succ_mod _add_mod + _pred_mod _sub_mod + _mul_mod _square_mod _power_mod. + + Definition make_mod_spec: mod_spec make_mod_op. + apply mk_mod_spec. + exact _succ_mod_spec. + exact _add_mod_spec. + exact _pred_mod_spec. + exact _sub_mod_spec. + exact _mul_mod_spec. + exact _square_mod_spec. + exact _power_mod_spec. + Defined. + +(*********** Mersenne special **********) + + Variable p: positive. + Variable zp: w. + + Hypothesis zp_b: [|zp|] = Zpos p. + Hypothesis p_lt_w_digits: Zpos p <= Zpos w_digits. + + Let p1 := Pminus (xO w_digits) p. + + Theorem p_p1: Zpos p + Zpos p1 = Zpos (xO w_digits). + unfold p1. + rewrite Zpos_minus; auto with zarith. + rewrite Zmax_right; auto with zarith. + rewrite Zpos_xO; auto with zarith. + assert (0 < Zpos w_digits); auto with zarith. + Qed. + + Let zp1 := ww_sub ww_zdigits (WW w0 zp). + + Let spec_add2: forall x y, + [[w_add2 x y]] = [|x|] + [|y|]. + unfold w_add2. + intros xh xl; generalize (ZnZ.spec_add_c xh xl). + unfold w_add_c; case ZnZ.add_c; unfold interp_carry; simpl ww_to_Z. + intros w2 Hw2; simpl; unfold w_to_Z; rewrite Hw2. + unfold w0; rewrite ZnZ.spec_0; simpl; auto with zarith. + intros w2; rewrite Zmult_1_l; simpl. + unfold w_to_Z, w1; rewrite ZnZ.spec_1; auto with zarith. + rewrite Zmult_1_l; auto. + Qed. + + Let spec_ww_digits: + [[ww_zdigits]] = Zpos (xO w_digits). + Proof. + unfold w_to_Z, ww_zdigits. + rewrite spec_add2. + unfold w_to_Z, w_zdigits, w_digits. + rewrite ZnZ.spec_zdigits; auto. + rewrite Zpos_xO; auto with zarith. + Qed. + + Let spec_ww_to_Z := (spec_ww_to_Z _ _ ZnZ.spec_to_Z). + Let spec_ww_compare := spec_ww_compare _ _ _ _ ZnZ.spec_0 + ZnZ.spec_to_Z ZnZ.spec_compare. + Let spec_ww_sub := + spec_ww_sub w0 zp wWW zp1 w_opp_c w_opp_carry + w_sub_c w_opp w_sub w_sub_carry w_digits w_to_Z + ZnZ.spec_0 + ZnZ.spec_to_Z + ZnZ.spec_WW + ZnZ.spec_opp_c + ZnZ.spec_opp + ZnZ.spec_opp_carry + ZnZ.spec_sub_c + ZnZ.spec_sub + ZnZ.spec_sub_carry. + + Theorem zp1_b: [[zp1]] = Zpos p1. + change ([[DoubleSub.ww_sub w0 wWW w_opp_c w_opp_carry w_sub_c w_opp w_sub + w_sub_carry ww_zdigits (WW w0 zp)]] = + Zpos p1). + rewrite spec_ww_sub; auto with zarith. + rewrite spec_ww_digits; simpl ww_to_Z. + change (w_to_Z w0) with [|w0|]. + unfold w0; rewrite ZnZ.spec_0; autorewrite with rm10; auto. + change (w_to_Z zp) with [|zp|]. + rewrite zp_b. + rewrite Zmod_small; auto with zarith. + rewrite <- p_p1; auto with zarith. + unfold ww_digits; split; auto with zarith. + rewrite <- p_p1; auto with zarith. + assert (0 < Zpos p1); auto with zarith. + apply Zle_lt_trans with (Zpos (xO w_digits)); auto with zarith. + assert (0 < Zpos p); auto with zarith. + unfold base; apply Zpower2_lt_lin; auto with zarith. + Qed. + + Hypothesis p_b: [|b|] = 2 ^ (Zpos p) - 1. + + + Let w_pos_mod := ZnZ.pos_mod. + + Let add_mul_div := + DoubleLift.ww_add_mul_div w0 wWW wW0 w0W + ww_compare w_add_mul_div + ww_sub w_zdigits low. + + Let _mmul_mod x y := + let xy := w_mul_c x y in + match xy with + W0 => w0 + | WW xh xl => + let xl1 := w_pos_mod zp xl in + match add_mul_div zp1 W0 xy with + W0 => match w_compare xl1 b with + | Lt => xl1 + | Eq => w0 + | Gt => w1 + end + | WW _ xl2 => _add_mod xl1 xl2 + end + end. + + Hint Unfold w_digits. + + Lemma WW_0: forall x y, [[WW x y]] = 0 -> [|x|] = 0 /\ [|y|] =0. + intros x y; simpl; case (ZnZ.spec_to_Z x); intros H1 H2; + case (ZnZ.spec_to_Z y); intros H3 H4 H5. + case Zle_lt_or_eq with (1 := H1); clear H1; intros H1; auto with zarith. + absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]); auto with zarith. + unfold w_to_Z, w_digits in H5;auto with zarith. + match goal with |- _ < ?X + _ => + apply Zlt_le_trans with X; auto with zarith + end. + case Zle_lt_or_eq with (1 := H3); clear H3; intros H3; auto with zarith. + absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]); auto with zarith. + unfold w_to_Z, w_digits in H5;auto with zarith. + rewrite <- H1; rewrite Zmult_0_l; auto with zarith. + Qed. + + Theorem WW0_is_0: [[W0]] = 0. + simpl; auto. + Qed. + Hint Rewrite WW0_is_0: w_rewrite. + + Theorem mmul_aux0: Zpos (xO w_digits) - Zpos p1 = Zpos p. + unfold w_digits. + apply trans_equal with (Zpos p + Zpos p1 - Zpos p1); auto with zarith. + rewrite p_p1; auto with zarith. + Qed. + + Theorem mmul_aux1: 2 ^ Zpos w_digits = + 2 ^ (Zpos w_digits - Zpos p) * 2 ^ Zpos p. + rewrite <- Zpower_exp; auto with zarith. + eq_tac; auto with zarith. + Qed. + + Theorem mmul_aux2:forall x, + x mod (2 ^ Zpos p - 1) = + ((x / 2 ^ Zpos p) + (x mod 2 ^ Zpos p)) mod (2 ^ Zpos p - 1). + intros x; pattern x at 1; rewrite Z_div_mod_eq with (b := 2 ^ Zpos p); auto with zarith. + match goal with |- (?X * ?Y + ?Z) mod (?X - 1) = ?T => + replace (X * Y + Z) with (Y * (X - 1) + (Y + Z)); try ring + end. + rewrite Zplus_mod; auto with zarith. + rewrite Z_mod_mult; auto with zarith. + rewrite Zplus_0_l. + rewrite Zmod_mod; auto with zarith. + Qed. + + Theorem mmul_aux3:forall xh xl, + [[WW xh xl]] mod (2 ^ Zpos p) = [|xl|] mod (2 ^ Zpos p). + intros xh xl; simpl ww_to_Z; unfold base. + rewrite Zplus_mod; auto with zarith. + generalize mmul_aux1; unfold w_digits; intros tmp; rewrite tmp; + clear tmp. + rewrite Zmult_assoc. + rewrite Z_mod_mult; auto with zarith. + rewrite Zplus_0_l; apply Zmod_mod; auto with zarith. + Qed. + + Let spec_low: forall x, + [|low x|] = [[x]] mod base w_digits. + intros x; case x; simpl low; auto with zarith. + intros xh xl; simpl. + rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith. + rewrite Zmod_small; auto with zarith. + case (ZnZ.spec_to_Z xl); auto with zarith. + unfold base; auto with zarith. + Qed. + + Theorem mmul_aux4:forall x, + [[x]] < [|b|] * 2 ^ Zpos p -> + match add_mul_div zp1 W0 x with + W0 => 0 + | WW _ xl2 => [|xl2|] + end = [[x]] / 2 ^ Zpos p. + intros x Hx. + assert (Hp: [[zp1]] <= Zpos (xO w_digits)); auto with zarith. + rewrite zp1_b; rewrite <- p_p1; auto with zarith. + assert (0 <= Zpos p); auto with zarith. + generalize (@DoubleLift.spec_ww_add_mul_div w w0 wWW wW0 w0W + ww_compare w_add_mul_div ww_sub w_digits w_zdigits low w_to_Z + ZnZ.spec_0 ZnZ.spec_to_Z spec_ww_to_Z + ZnZ.spec_WW ZnZ.spec_WO ZnZ.spec_OW + spec_ww_compare ZnZ.spec_add_mul_div spec_ww_sub + ZnZ.spec_zdigits spec_low W0 x zp1 Hp). + unfold add_mul_div; + case DoubleLift.ww_add_mul_div; autorewrite with w_rewrite; auto. + rewrite Zmult_0_l; rewrite Zplus_0_l. + rewrite zp1_b. + generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp. + rewrite Zmod_small; auto with zarith. + split; auto with zarith. + apply Z_div_pos; auto with zarith. + case (spec_ww_to_Z x); auto with zarith. + unfold base. + apply Zdiv_lt_upper_bound; auto with zarith. + rewrite <- Zpower_exp; auto with zarith. + apply Zlt_le_trans with (base (ww_digits (ZnZ.digits w_op))); auto with zarith. + case (spec_ww_to_Z x); auto with zarith. + unfold base; apply Zpower_le_monotone; auto with zarith. + split; auto with zarith. + assert (0 < Zpos p); auto with zarith. + intros w2 w3; rewrite Zmult_0_l; rewrite Zplus_0_l. + rewrite zp1_b. + generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; + clear tmp. + simpl ww_to_Z; rewrite Zmod_small; auto with zarith. + intros H1; + generalize (high_zero (WW w2 w3)); unfold w_digits;intros tmp; + simpl fst in tmp; simpl ww_to_Z in tmp;auto with zarith. + unfold w_to_Z in *. + rewrite tmp in H1; auto with zarith. clear tmp. + simpl ww_to_Z; rewrite H1; apply Zdiv_lt_upper_bound; auto with zarith. + unfold base; rewrite <- Zpower_exp; auto with zarith. + apply Zlt_le_trans with (1 := Hx). + apply Zle_trans with (2 ^ Zpos p * 2 ^ Zpos p). + rewrite p_b; apply Zmult_le_compat_r; auto with zarith. + rewrite <- Zpower_exp; auto with zarith. + apply Zpower_le_monotone; auto with zarith. + split; auto with zarith. + apply Z_div_pos; auto with zarith. + case (spec_ww_to_Z x); auto with zarith. + unfold base. + apply Zdiv_lt_upper_bound; auto with zarith. + rewrite <- Zpower_exp; auto with zarith. + apply Zlt_le_trans with (base (ww_digits (ZnZ.digits w_op))); auto with zarith. + case (spec_ww_to_Z x); auto with zarith. + unfold base; apply Zpower_le_monotone; auto with zarith. + split; auto with zarith. + assert (0 < Zpos p); auto with zarith. + Qed. + + Theorem mmul_aux5:forall xh xl, + [[WW xh xl]] < [|b|] * 2 ^ Zpos p -> + let xl1 := w_pos_mod zp xl in + let r := + match add_mul_div zp1 W0 (WW xh xl) with + W0 => match w_compare xl1 b with + | Lt => xl1 + | Eq => w0 + | Gt => w1 + end + | WW _ xl2 => _add_mod xl1 xl2 + end in + [|r|] = [[WW xh xl]] mod [|b|]. + intros xh xl Hx xl1 r; unfold r; clear r. + generalize (mmul_aux4 _ Hx). + simpl ww_to_Z; rewrite p_b. + rewrite mmul_aux2. + assert (Hp: [[zp1]] <= Zpos (xO w_digits)); auto with zarith. + rewrite zp1_b; rewrite <- p_p1; auto with zarith. + assert (0 <= Zpos p); auto with zarith. + generalize (@DoubleLift.spec_ww_add_mul_div w w0 wWW wW0 w0W + ww_compare w_add_mul_div ww_sub w_digits w_zdigits low w_to_Z + ZnZ.spec_0 ZnZ.spec_to_Z spec_ww_to_Z + ZnZ.spec_WW ZnZ.spec_WO ZnZ.spec_OW + spec_ww_compare ZnZ.spec_add_mul_div spec_ww_sub + ZnZ.spec_zdigits spec_low W0 (WW xh xl) zp1 Hp). + unfold add_mul_div; + case DoubleLift.ww_add_mul_div; autorewrite with w_rewrite; auto. + rewrite Zmult_0_l; rewrite Zplus_0_l. + rewrite zp1_b. + generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; clear tmp. + intros H1 H2. + rewrite <- H2. + rewrite Zplus_0_l. + generalize mmul_aux3; simpl ww_to_Z; intros tmp; rewrite tmp; clear tmp; + auto with zarith. + unfold xl1; unfold w_pos_mod. + rewrite <- p_b; rewrite <- zp_b. + rewrite <- ZnZ.spec_pos_mod; auto with zarith. + unfold w_compare; rewrite ZnZ.spec_compare; + case Zcompare_spec; intros Hc; + match goal with H: context[b] |- _ => + generalize H; clear H + end; try rewrite _w0_is_0. + intros H3; rewrite H3. + rewrite Z_mod_same; auto with zarith. + intros H3; rewrite Zmod_small; auto with zarith. + case (ZnZ.spec_to_Z (ZnZ.pos_mod zp xl)); unfold w_to_Z; auto with zarith. + rewrite p_b; rewrite ZnZ.spec_pos_mod; auto with zarith. + intros H3; assert (HH: [|xl|] mod 2 ^ Zpos p = 2 ^ Zpos p). + apply Zle_antisym; auto with zarith. + case (Z_mod_lt ([|xl|]) (2 ^ Zpos p)); auto with zarith. + rewrite zp_b in H3; auto with zarith. + rewrite zp_b; rewrite HH. + rewrite <- Zmod_minus_one; auto with zarith. + rewrite _w1_is_1; rewrite Zmod_small; auto with zarith. + rewrite Zmult_0_l; rewrite Zplus_0_l. + rewrite zp1_b. + generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; clear tmp. + intros w2 w3 H1 H2; rewrite <- H2. + generalize mmul_aux3; simpl ww_to_Z; intros tmp; rewrite tmp; clear tmp; + auto with zarith. + rewrite <- p_b; rewrite <- zp_b. + rewrite <- ZnZ.spec_pos_mod; auto with zarith. + unfold xl1; unfold w_pos_mod. + rewrite Zplus_comm. + apply _add_mod_correct; auto with zarith. + assert (tmp: forall x, 2 * x = x + x); auto with zarith; + rewrite tmp; apply Zplus_le_lt_compat; clear tmp; auto with zarith. + rewrite ZnZ.spec_pos_mod; auto with zarith. + rewrite p_b; case (Z_mod_lt [|xl|] (2 ^ Zpos p)); auto with zarith. + rewrite zp_b; auto with zarith. + rewrite H2; apply Zdiv_lt_upper_bound; auto with zarith. + Qed. + + Lemma _mmul_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] -> + [|_mmul_mod w1 w2|] = ([|w1|] * [|w2|]) mod [|b|]. + intros w2 w3 t1 t2; unfold _mmul_mod, w_mul_c; intros H H1. + assert (F: [|w2|] < [|b|]). + case (Z_mod_lt t1 [|b|]); auto with zarith. + assert (F': [|w3|] < [|b|]). + case (Z_mod_lt t2 [|b|]); auto with zarith. + match goal with |- context[ZnZ.mul_c ?x ?y] => + generalize (ZnZ.spec_mul_c x y); unfold interp_carry; + case (ZnZ.mul_c x y); autorewrite with w_rewrite + end; auto with zarith. + simpl; intros H2; rewrite <- H2; rewrite Zmod_small; + auto with zarith. + intros w4 w5 H2. + rewrite mmul_aux5; auto with zarith. + rewrite <- H2; auto. + unfold ww_to_Z,w_digits,w_to_Z; rewrite H2. + apply Zmult_lt_compat; auto with zarith. + case (ZnZ.spec_to_Z w2); auto with zarith. + case (ZnZ.spec_to_Z w3); auto with zarith. + Qed. + + Let _msquare_mod x := + let xy := w_square_c x in + match xy with + W0 => w0 + | WW xh xl => + let xl1 := w_pos_mod zp xl in + match add_mul_div zp1 W0 xy with + W0 => match w_compare xl1 b with + | Lt => xl1 + | Eq => w0 + | Gt => w1 + end + | WW _ xl2 => _add_mod xl1 xl2 + end + end. + + Lemma _msquare_mod_spec: forall w1 t1, [|w1|] = t1 mod [|b|] -> + [|_msquare_mod w1|] = ([|w1|] * [|w1|]) mod [|b|]. + intros w2 t2; unfold _msquare_mod, w_square_c; intros H. + assert (F: [|w2|] < [|b|]). + case (Z_mod_lt t2 [|b|]); auto with zarith. + match goal with |- context[ZnZ.square_c ?x] => + generalize (ZnZ.spec_square_c x); unfold interp_carry; + case (ZnZ.square_c x); autorewrite with w_rewrite + end; auto with zarith. + simpl; intros H2; rewrite <- H2; rewrite Zmod_small; + auto with zarith. + intros w4 w5 H2. + rewrite mmul_aux5; auto with zarith. + unfold ww_to_Z, w_to_Z ,w_digits; rewrite <- H2; auto. + unfold ww_to_Z,w_to_Z ,w_digits; rewrite H2. + apply Zmult_lt_compat; auto with zarith. + case (ZnZ.spec_to_Z w2); auto with zarith. + case (ZnZ.spec_to_Z w2); auto with zarith. + Qed. + + Definition mmake_mod_op := + mk_mod_op + _succ_mod _add_mod + _pred_mod _sub_mod + _mmul_mod _msquare_mod _power_mod. + + Definition mmake_mod_spec: mod_spec mmake_mod_op. + apply mk_mod_spec. + exact _succ_mod_spec. + exact _add_mod_spec. + exact _pred_mod_spec. + exact _sub_mod_spec. + exact _mmul_mod_spec. + exact _msquare_mod_spec. + exact _power_mod_spec. + Defined. + +End Mod_op. + |