diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Int63.v | 33 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 58 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_calc.v | 8 | ||||
| -rw-r--r-- | theories/ZArith/ZArith.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/Zlogarithm.v | 273 | ||||
| -rw-r--r-- | theories/ZArith/Zsqrt_compat.v | 234 |
6 files changed, 26 insertions, 581 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. diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 5ed60b0a0f..2428fc495d 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -178,7 +178,7 @@ Proof. change (cos (PI / 4) <> 0); rewrite cos_PI4; apply R1_sqrt2_neq_0. Qed. -Lemma cos3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2. +Lemma cos_3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2. Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4. @@ -186,12 +186,16 @@ Proof. ring. Qed. -Lemma sin3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2. +#[deprecated(since="8.10",note="Use cos_3PI4 instead.")] Notation cos3PI4 := cos_3PI4. + +Lemma sin_3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2. Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. now rewrite sin_shift, cos_neg, cos_PI4. Qed. +#[deprecated(since="8.10",note="Use sin_3PI4 instead.")] Notation sin3PI4 := sin_3PI4. + Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2. Proof with trivial. apply Rsqr_inj... diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index c2c97fca4f..b0744caa7b 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -21,6 +21,5 @@ Require Export Zpow_def. Require Export Zcomplements. Require Export Zpower. Require Export Zdiv. -Require Export Zlogarithm. Export ZArithRing. diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v deleted file mode 100644 index edbd3a18fe..0000000000 --- a/theories/ZArith/Zlogarithm.v +++ /dev/null @@ -1,273 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(**********************************************************************) - -(** The integer logarithms with base 2. *) - -(** THIS FILE IS DEPRECATED. - Please rather use [Z.log2] (or [Z.log2_up]), which - are defined in [BinIntDef], and whose properties can - be found in [BinInt.Z]. *) - -(* There are three logarithms defined here, - depending on the rounding of the real 2-based logarithm: - - [Log_inf]: [y = (Log_inf x) iff 2^y <= x < 2^(y+1)] - i.e. [Log_inf x] is the biggest integer that is smaller than [Log x] - - [Log_sup]: [y = (Log_sup x) iff 2^(y-1) < x <= 2^y] - i.e. [Log_inf x] is the smallest integer that is bigger than [Log x] - - [Log_nearest]: [y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)] - i.e. [Log_nearest x] is the integer nearest from [Log x] *) - -Require Import ZArith_base Omega Zcomplements Zpower. -Local Open Scope Z_scope. - -Section Log_pos. (* Log of positive integers *) - - (** First we build [log_inf] and [log_sup] *) - - Fixpoint log_inf (p:positive) : Z := - match p with - | xH => 0 (* 1 *) - | xO q => Z.succ (log_inf q) (* 2n *) - | xI q => Z.succ (log_inf q) (* 2n+1 *) - end. - - Fixpoint log_sup (p:positive) : Z := - match p with - | xH => 0 (* 1 *) - | xO n => Z.succ (log_sup n) (* 2n *) - | xI n => Z.succ (Z.succ (log_inf n)) (* 2n+1 *) - end. - - Hint Unfold log_inf log_sup : core. - - Lemma Psize_log_inf : forall p, Zpos (Pos.size p) = Z.succ (log_inf p). - Proof. - induction p; simpl; now rewrite ?Pos2Z.inj_succ, ?IHp. - Qed. - - Lemma Zlog2_log_inf : forall p, Z.log2 (Zpos p) = log_inf p. - Proof. - unfold Z.log2. destruct p; simpl; trivial; apply Psize_log_inf. - Qed. - - Lemma Zlog2_up_log_sup : forall p, Z.log2_up (Zpos p) = log_sup p. - Proof. - induction p; simpl log_sup. - - change (Zpos p~1) with (2*(Zpos p)+1). - rewrite Z.log2_up_succ_double, Zlog2_log_inf; try easy. - unfold Z.succ. now rewrite !(Z.add_comm _ 1), Z.add_assoc. - - change (Zpos p~0) with (2*Zpos p). - now rewrite Z.log2_up_double, IHp. - - reflexivity. - Qed. - - (** Then we give the specifications of [log_inf] and [log_sup] - and prove their validity *) - - Hint Resolve Z.le_trans: zarith. - - Theorem log_inf_correct : - forall x:positive, - 0 <= log_inf x /\ two_p (log_inf x) <= Zpos x < two_p (Z.succ (log_inf x)). - Proof. - simple induction x; intros; simpl; - [ elim H; intros Hp HR; clear H; split; - [ auto with zarith - | rewrite two_p_S with (x := Z.succ (log_inf p)) by (apply Z.le_le_succ_r; trivial); - rewrite two_p_S by trivial; - rewrite two_p_S in HR by trivial; rewrite (BinInt.Pos2Z.inj_xI p); - omega ] - | elim H; intros Hp HR; clear H; split; - [ auto with zarith - | rewrite two_p_S with (x := Z.succ (log_inf p)) by (apply Z.le_le_succ_r; trivial); - rewrite two_p_S by trivial; - rewrite two_p_S in HR by trivial; rewrite (BinInt.Pos2Z.inj_xO p); - omega ] - | unfold two_power_pos; unfold shift_pos; simpl; - omega ]. - Qed. - - Definition log_inf_correct1 (p:positive) := proj1 (log_inf_correct p). - Definition log_inf_correct2 (p:positive) := proj2 (log_inf_correct p). - - Opaque log_inf_correct1 log_inf_correct2. - - Hint Resolve log_inf_correct1 log_inf_correct2: zarith. - - Lemma log_sup_correct1 : forall p:positive, 0 <= log_sup p. - Proof. - simple induction p; intros; simpl; auto with zarith. - Qed. - - (** For every [p], either [p] is a power of two and [(log_inf p)=(log_sup p)] - either [(log_sup p)=(log_inf p)+1] *) - - Theorem log_sup_log_inf : - forall p:positive, - IF Zpos p = two_p (log_inf p) then Zpos p = two_p (log_sup p) - else log_sup p = Z.succ (log_inf p). - Proof. - simple induction p; intros; - [ elim H; right; simpl; - rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - rewrite BinInt.Pos2Z.inj_xI; unfold Z.succ; omega - | elim H; clear H; intro Hif; - [ left; simpl; - rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - rewrite (two_p_S (log_sup p0) (log_sup_correct1 p0)); - rewrite <- (proj1 Hif); rewrite <- (proj2 Hif); - auto - | right; simpl; - rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - rewrite BinInt.Pos2Z.inj_xO; unfold Z.succ; - omega ] - | left; auto ]. - Qed. - - Theorem log_sup_correct2 : - forall x:positive, two_p (Z.pred (log_sup x)) < Zpos x <= two_p (log_sup x). - Proof. - intro. - elim (log_sup_log_inf x). - (* x is a power of two and [log_sup = log_inf] *) - intros [E1 E2]; rewrite E2. - split; [ apply two_p_pred; apply log_sup_correct1 | apply Z.le_refl ]. - intros [E1 E2]; rewrite E2. - rewrite (Z.pred_succ (log_inf x)). - generalize (log_inf_correct2 x); omega. - Qed. - - Lemma log_inf_le_log_sup : forall p:positive, log_inf p <= log_sup p. - Proof. - simple induction p; simpl; intros; omega. - Qed. - - Lemma log_sup_le_Slog_inf : forall p:positive, log_sup p <= Z.succ (log_inf p). - Proof. - simple induction p; simpl; intros; omega. - Qed. - - (** Now it's possible to specify and build the [Log] rounded to the nearest *) - - Fixpoint log_near (x:positive) : Z := - match x with - | xH => 0 - | xO xH => 1 - | xI xH => 2 - | xO y => Z.succ (log_near y) - | xI y => Z.succ (log_near y) - end. - - Theorem log_near_correct1 : forall p:positive, 0 <= log_near p. - Proof. - simple induction p; simpl; intros; - [ elim p0; auto with zarith - | elim p0; auto with zarith - | trivial with zarith ]. - intros; apply Z.le_le_succ_r. - generalize H0; now elim p1. - intros; apply Z.le_le_succ_r. - generalize H0; now elim p1. - Qed. - - Theorem log_near_correct2 : - forall p:positive, log_near p = log_inf p \/ log_near p = log_sup p. - Proof. - simple induction p. - intros p0 [Einf| Esup]. - simpl. rewrite Einf. - case p0; [ left | left | right ]; reflexivity. - simpl; rewrite Esup. - elim (log_sup_log_inf p0). - generalize (log_inf_le_log_sup p0). - generalize (log_sup_le_Slog_inf p0). - case p0; auto with zarith. - intros; omega. - case p0; intros; auto with zarith. - intros p0 [Einf| Esup]. - simpl. - repeat rewrite Einf. - case p0; intros; auto with zarith. - simpl. - repeat rewrite Esup. - case p0; intros; auto with zarith. - auto. - Qed. - -End Log_pos. - -Section divers. - - (** Number of significative digits. *) - - Definition N_digits (x:Z) := - match x with - | Zpos p => log_inf p - | Zneg p => log_inf p - | Z0 => 0 - end. - - Lemma ZERO_le_N_digits : forall x:Z, 0 <= N_digits x. - Proof. - simple induction x; simpl; - [ apply Z.le_refl | exact log_inf_correct1 | exact log_inf_correct1 ]. - Qed. - - Lemma log_inf_shift_nat : forall n:nat, log_inf (shift_nat n 1) = Z.of_nat n. - Proof. - simple induction n; intros; - [ try trivial | rewrite Nat2Z.inj_succ; rewrite <- H; reflexivity ]. - Qed. - - Lemma log_sup_shift_nat : forall n:nat, log_sup (shift_nat n 1) = Z.of_nat n. - Proof. - simple induction n; intros; - [ try trivial | rewrite Nat2Z.inj_succ; rewrite <- H; reflexivity ]. - Qed. - - (** [Is_power p] means that p is a power of two *) - Fixpoint Is_power (p:positive) : Prop := - match p with - | xH => True - | xO q => Is_power q - | xI q => False - end. - - Lemma Is_power_correct : - forall p:positive, Is_power p <-> (exists y : nat, p = shift_nat y 1). - Proof. - split; - [ elim p; - [ simpl; tauto - | simpl; intros; generalize (H H0); intro H1; elim H1; - intros y0 Hy0; exists (S y0); rewrite Hy0; reflexivity - | intro; exists 0%nat; reflexivity ] - | intros; elim H; intros; rewrite H0; elim x; intros; simpl; trivial ]. - Qed. - - Lemma Is_power_or : forall p:positive, Is_power p \/ ~ Is_power p. - Proof. - simple induction p; - [ intros; right; simpl; tauto - | intros; elim H; - [ intros; left; simpl; exact H0 - | intros; right; simpl; exact H0 ] - | left; simpl; trivial ]. - Qed. - -End divers. - - - - - - diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v deleted file mode 100644 index 6873c737a7..0000000000 --- a/theories/ZArith/Zsqrt_compat.v +++ /dev/null @@ -1,234 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -Require Import ZArithRing. -Require Import Omega. -Require Export ZArith_base. -Local Open Scope Z_scope. - -(** THIS FILE IS DEPRECATED - - Instead of the various [Zsqrt] defined here, please use rather - [Z.sqrt] (or [Z.sqrtrem]). The latter are pure functions without - proof parts, and more results are available about them. - Some equivalence proofs between the old and the new versions - can be found below. Importing ZArith will provides by default - the new versions. - -*) - -(**********************************************************************) -(** Definition and properties of square root on Z *) - -(** The following tactic replaces all instances of (POS (xI ...)) by - `2*(POS ...)+1`, but only when ... is not made only with xO, XI, or xH. *) -Ltac compute_POS := - match goal with - | |- context [(Zpos (xI ?X1))] => - match constr:(X1) with - | context [1%positive] => fail 1 - | _ => rewrite (Pos2Z.inj_xI X1) - end - | |- context [(Zpos (xO ?X1))] => - match constr:(X1) with - | context [1%positive] => fail 1 - | _ => rewrite (Pos2Z.inj_xO X1) - end - end. - -Inductive sqrt_data (n:Z) : Set := - c_sqrt : forall s r:Z, n = s * s + r -> 0 <= r <= 2 * s -> sqrt_data n. - -Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p). - refine - (fix sqrtrempos (p:positive) : sqrt_data (Zpos p) := - match p return sqrt_data (Zpos p) with - | xH => c_sqrt 1 1 0 _ _ - | xO xH => c_sqrt 2 1 1 _ _ - | xI xH => c_sqrt 3 1 2 _ _ - | xO (xO p') => - match sqrtrempos p' with - | c_sqrt _ s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r') with - | left Hle => - c_sqrt (Zpos (xO (xO p'))) (2 * s' + 1) - (4 * r' - (4 * s' + 1)) _ _ - | right Hgt => c_sqrt (Zpos (xO (xO p'))) (2 * s') (4 * r') _ _ - end - end - | xO (xI p') => - match sqrtrempos p' with - | c_sqrt _ s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r' + 2) with - | left Hle => - c_sqrt (Zpos (xO (xI p'))) (2 * s' + 1) - (4 * r' + 2 - (4 * s' + 1)) _ _ - | right Hgt => - c_sqrt (Zpos (xO (xI p'))) (2 * s') (4 * r' + 2) _ _ - end - end - | xI (xO p') => - match sqrtrempos p' with - | c_sqrt _ s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r' + 1) with - | left Hle => - c_sqrt (Zpos (xI (xO p'))) (2 * s' + 1) - (4 * r' + 1 - (4 * s' + 1)) _ _ - | right Hgt => - c_sqrt (Zpos (xI (xO p'))) (2 * s') (4 * r' + 1) _ _ - end - end - | xI (xI p') => - match sqrtrempos p' with - | c_sqrt _ s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r' + 3) with - | left Hle => - c_sqrt (Zpos (xI (xI p'))) (2 * s' + 1) - (4 * r' + 3 - (4 * s' + 1)) _ _ - | right Hgt => - c_sqrt (Zpos (xI (xI p'))) (2 * s') (4 * r' + 3) _ _ - end - end - end); clear sqrtrempos; repeat compute_POS; - try (try rewrite Heq; ring); try omega. -Defined. - -(** Define with integer input, but with a strong (readable) specification. *) -Definition Zsqrt : - forall x:Z, - 0 <= x -> - {s : Z & {r : Z | x = s * s + r /\ s * s <= x < (s + 1) * (s + 1)}}. - refine - (fun x => - match - x - return - 0 <= x -> - {s : Z & {r : Z | x = s * s + r /\ s * s <= x < (s + 1) * (s + 1)}} - with - | Zpos p => - fun h => - match sqrtrempos p with - | c_sqrt _ s r Heq Hint => - existT - (fun s:Z => - {r : Z | - Zpos p = s * s + r /\ s * s <= Zpos p < (s + 1) * (s + 1)}) - s - (exist - (fun r:Z => - Zpos p = s * s + r /\ - s * s <= Zpos p < (s + 1) * (s + 1)) r _) - end - | Zneg p => - fun h => - False_rec - {s : Z & - {r : Z | - Zneg p = s * s + r /\ s * s <= Zneg p < (s + 1) * (s + 1)}} - (h (eq_refl Datatypes.Gt)) - | Z0 => - fun h => - existT - (fun s:Z => - {r : Z | 0 = s * s + r /\ s * s <= 0 < (s + 1) * (s + 1)}) 0 - (exist - (fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0 - _) - end); try omega. - split; [ omega | rewrite Heq; ring_simplify (s*s) ((s + 1) * (s + 1)); omega ]. -Defined. - -(** Define a function of type Z->Z that computes the integer square root, - but only for positive numbers, and 0 for others. *) -Definition Zsqrt_plain (x:Z) : Z := - match x with - | Zpos p => - match Zsqrt (Zpos p) (Pos2Z.is_nonneg p) with - | existT _ s _ => s - end - | Zneg p => 0 - | Z0 => 0 - end. - -(** A basic theorem about Zsqrt_plain *) - -Theorem Zsqrt_interval : - forall n:Z, - 0 <= n -> - Zsqrt_plain n * Zsqrt_plain n <= n < - (Zsqrt_plain n + 1) * (Zsqrt_plain n + 1). -Proof. - intros [|p|p] Hp. - - now compute. - - unfold Zsqrt_plain. - now destruct Zsqrt as (s & r & Heq & Hint). - - now elim Hp. -Qed. - -(** Positivity *) - -Theorem Zsqrt_plain_is_pos: forall n, 0 <= n -> 0 <= Zsqrt_plain n. -Proof. - intros n m; case (Zsqrt_interval n); auto with zarith. - intros H1 H2; case (Z.le_gt_cases 0 (Zsqrt_plain n)); auto. - intros H3; contradict H2; auto; apply Z.le_ngt. - apply Z.le_trans with ( 2 := H1 ). - replace ((Zsqrt_plain n + 1) * (Zsqrt_plain n + 1)) - with (Zsqrt_plain n * Zsqrt_plain n + (2 * Zsqrt_plain n + 1)); - auto with zarith. - ring. -Qed. - -(** Direct correctness on squares. *) - -Theorem Zsqrt_square_id: forall a, 0 <= a -> Zsqrt_plain (a * a) = a. -Proof. - intros a H. - generalize (Zsqrt_plain_is_pos (a * a)); auto with zarith; intros Haa. - case (Zsqrt_interval (a * a)); auto with zarith. - intros H1 H2. - case (Z.le_gt_cases a (Zsqrt_plain (a * a))); intros H3. - - Z.le_elim H3; auto. - contradict H1; auto; apply Z.lt_nge; auto with zarith. - apply Z.le_lt_trans with (a * Zsqrt_plain (a * a)); auto with zarith. - apply Z.mul_lt_mono_pos_r; auto with zarith. - - contradict H2; auto; apply Z.le_ngt; auto with zarith. - apply Z.mul_le_mono_nonneg; auto with zarith. -Qed. - -(** [Zsqrt_plain] is increasing *) - -Theorem Zsqrt_le: - forall p q, 0 <= p <= q -> Zsqrt_plain p <= Zsqrt_plain q. -Proof. - intros p q [H1 H2]. - Z.le_elim H2; [ | subst q; auto with zarith]. - case (Z.le_gt_cases (Zsqrt_plain p) (Zsqrt_plain q)); auto; intros H3. - assert (Hp: (0 <= Zsqrt_plain q)). - { apply Zsqrt_plain_is_pos; auto with zarith. } - absurd (q <= p); auto with zarith. - apply Z.le_trans with ((Zsqrt_plain q + 1) * (Zsqrt_plain q + 1)). - case (Zsqrt_interval q); auto with zarith. - apply Z.le_trans with (Zsqrt_plain p * Zsqrt_plain p); auto with zarith. - apply Z.mul_le_mono_nonneg; auto with zarith. - case (Zsqrt_interval p); auto with zarith. -Qed. - - -(** Equivalence between Zsqrt_plain and [Z.sqrt] *) - -Lemma Zsqrt_equiv : forall n, Zsqrt_plain n = Z.sqrt n. -Proof. - intros. destruct (Z_le_gt_dec 0 n). - symmetry. apply Z.sqrt_unique; trivial. - now apply Zsqrt_interval. - now destruct n. -Qed. |