diff options
Diffstat (limited to 'theories/Numbers/Cyclic')
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Int63.v | 33 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 58 |
2 files changed, 20 insertions, 71 deletions
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 9bb16b97e2..9e9481341f 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -388,7 +388,7 @@ Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y. Axiom diveucl_21_spec : forall a1 a2 b, let (q,r) := diveucl_21 a1 a2 b in let (q',r') := Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|] in - [|q|] = Z.modulo q' wB /\ [|r|] = r'. + [|a1|] < [|b|] -> [|q|] = q' /\ [|r|] = r'. Axiom addmuldiv_def_spec : forall p x y, addmuldiv p x y = addmuldiv_def p x y. @@ -812,14 +812,6 @@ Proof. eapply Z.lt_le_trans; [ | apply Zpower2_le_lin ]; auto with zarith. Qed. -Lemma lsr_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63. -Proof. - apply to_Z_inj. - rewrite -> add_spec, !lsl_spec, add_spec. - rewrite -> Zmult_mod_idemp_l, <-Zplus_mod. - apply f_equal2 with (f := Zmod); auto with zarith. -Qed. - (* LSL *) Lemma lsl0 i: 0 << i = 0%int63. Proof. @@ -1119,7 +1111,7 @@ Proof. generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb. generalize Heq; rewrite (bit_split x) at 1; rewrite (bit_split y )at 1; clear Heq. rewrite (fun y => add_comm y (bit x 0)), <-!add_assoc, add_comm, - <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsr_add_distr. + <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsl_add_distr. rewrite (bit_split (x lor y)), lor_spec. intros Heq. assert (F: (bit x 0 + bit y 0)%int63 = (bit x 0 || bit y 0)). @@ -1429,26 +1421,9 @@ Proof. generalize (Z_div_mod ([|a1|]*wB+[|a2|]) [|b|] H). revert W. destruct (diveucl_21 a1 a2 b); destruct (Z.div_eucl ([|a1|]*wB+[|a2|]) [|b|]). - intros (H', H''); rewrite H', H''; clear H' H''. + intros (H', H''); auto; rewrite H', H''; clear H' H''. intros (H', H''); split; [ |exact H'']. - rewrite H', Zmult_comm, Z.mod_small; [reflexivity| ]. - split. - { revert H'; case z; [now simpl..|intros p H']. - exfalso; apply (Z.lt_irrefl 0), (Z.le_lt_trans _ ([|a1|] * wB + [|a2|])). - { now apply Z.add_nonneg_nonneg; [apply Z.mul_nonneg_nonneg| ]. } - rewrite H'; apply (Zplus_lt_reg_r _ _ (- z0)); ring_simplify. - apply (Z.le_lt_trans _ (- [|b|])); [ |now auto with zarith]. - rewrite Z.opp_eq_mul_m1; apply Zmult_le_compat_l; [ |now apply Wb]. - rewrite <-!Pos2Z.opp_pos, <-Z.opp_le_mono. - now change 1 with (Z.succ 0); apply Zlt_le_succ. } - rewrite <-Z.nle_gt; intro Hz; revert H2; apply Zle_not_lt. - rewrite (Z.div_unique_pos (wB * [|a1|] + [|a2|]) wB [|a1|] [|a2|]); - [ |now simpl..]. - rewrite Z.mul_comm, H'. - rewrite (Z.div_unique_pos (wB * [|b|] + z0) wB [|b|] z0) at 1; - [ |split; [ |apply (Z.lt_trans _ [|b|])]; now simpl|reflexivity]. - apply Z_div_le; [now simpl| ]; rewrite Z.mul_comm; apply Zplus_le_compat_r. - now apply Zmult_le_compat_l. + now rewrite H', Zmult_comm. Qed. Lemma div2_phi ih il j: (2^62 <= [|j|] -> [|ih|] < [|j|] -> diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 28565b2fe3..2785e89c5d 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -648,40 +648,15 @@ Section ZModulo. apply two_power_pos_correct. Qed. - Definition head0 x := match [|x|] with + Definition head0 x := + match [| x |] with | Z0 => zdigits - | Zpos p => zdigits - log_inf p - 1 - | _ => 0 - end. + | Zneg _ => 0 + | (Zpos _) as p => zdigits - Z.log2 p - 1 + end. Lemma spec_head00: forall x, [|x|] = 0 -> [|head0 x|] = Zpos digits. - Proof. - unfold head0; intros. - rewrite H; simpl. - apply spec_zdigits. - Qed. - - Lemma log_inf_bounded : forall x p, Zpos x < 2^p -> log_inf x < p. - Proof. - induction x; simpl; intros. - - assert (0 < p) by (destruct p; compute; auto with zarith; discriminate). - cut (log_inf x < p - 1); [omega| ]. - apply IHx. - change (Zpos x~1) with (2*(Zpos x)+1) in H. - replace p with (Z.succ (p-1)) in H; auto with zarith. - rewrite Z.pow_succ_r in H; auto with zarith. - - assert (0 < p) by (destruct p; compute; auto with zarith; discriminate). - cut (log_inf x < p - 1); [omega| ]. - apply IHx. - change (Zpos x~0) with (2*(Zpos x)) in H. - replace p with (Z.succ (p-1)) in H; auto with zarith. - rewrite Z.pow_succ_r in H; auto with zarith. - - simpl; intros; destruct p; compute; auto with zarith. - Qed. - + Proof. unfold head0; intros x ->; apply spec_zdigits. Qed. Lemma spec_head0 : forall x, 0 < [|x|] -> wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB. @@ -689,36 +664,35 @@ Section ZModulo. intros; unfold head0. generalize (spec_to_Z x). destruct [|x|]; try discriminate. + pose proof (Z.log2_nonneg (Zpos p)). + destruct (Z.log2_spec (Zpos p)); auto. intros. - destruct (log_inf_correct p). - rewrite 2 two_p_power2 in H2; auto with zarith. - assert (0 <= zdigits - log_inf p - 1 < wB). + assert (0 <= zdigits - Z.log2 (Zpos p) - 1 < wB) as Hrange. split. - cut (log_inf p < zdigits); try omega. + cut (Z.log2 (Zpos p) < zdigits). omega. unfold zdigits. unfold wB, base in *. - apply log_inf_bounded; auto with zarith. + apply Z.log2_lt_pow2; intuition. apply Z.lt_trans with zdigits. omega. unfold zdigits, wB, base; apply Zpower2_lt_lin; auto with zarith. - unfold to_Z; rewrite (Zmod_small _ _ H3). - destruct H2. + unfold to_Z; rewrite (Zmod_small _ _ Hrange). split. - apply Z.le_trans with (2^(zdigits - log_inf p - 1)*(2^log_inf p)). + apply Z.le_trans with (2^(zdigits - Z.log2 (Zpos p) - 1)*(2^Z.log2 (Zpos p))). apply Zdiv_le_upper_bound; auto with zarith. rewrite <- Zpower_exp; auto with zarith. rewrite Z.mul_comm; rewrite <- Z.pow_succ_r; auto with zarith. - replace (Z.succ (zdigits - log_inf p -1 +log_inf p)) with zdigits + replace (Z.succ (zdigits - Z.log2 (Zpos p) -1 + Z.log2 (Zpos p))) with zdigits by ring. unfold wB, base, zdigits; auto with zarith. apply Z.mul_le_mono_nonneg; auto with zarith. apply Z.lt_le_trans - with (2^(zdigits - log_inf p - 1)*(2^(Z.succ (log_inf p)))). + with (2^(zdigits - Z.log2 (Zpos p) - 1)*(2^(Z.succ (Z.log2 (Zpos p))))). apply Z.mul_lt_mono_pos_l; auto with zarith. rewrite <- Zpower_exp; auto with zarith. - replace (zdigits - log_inf p -1 +Z.succ (log_inf p)) with zdigits + replace (zdigits - Z.log2 (Zpos p) -1 +Z.succ (Z.log2 (Zpos p))) with zdigits by ring. unfold wB, base, zdigits; auto with zarith. Qed. |