From 56cc02a39a52485a732b3dc443e102a3511f8021 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 21 Mar 2019 15:59:52 +0000 Subject: [stdlib] Remove deprecated module Zsqrt_compat --- .../09811-remove-zlogarithm.rst | 3 +- doc/stdlib/index-list.html.template | 1 - theories/ZArith/Zsqrt_compat.v | 234 --------------------- 3 files changed, 2 insertions(+), 236 deletions(-) delete mode 100644 theories/ZArith/Zsqrt_compat.v diff --git a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst index 3533764964..ab625b9e03 100644 --- a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst +++ b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst @@ -1,3 +1,4 @@ -- Removes deprecated module `Coq.ZArith.Zlogarithm` +- Removes deprecated modules `Coq.ZArith.Zlogarithm` + and `Coq.ZArith.Zsqrt_compat` (#9881 by Vincent Laporte). diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 8d481b7f03..8b5ede7036 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -181,7 +181,6 @@ through the Require Import command.

theories/ZArith/Zhints.v (theories/ZArith/ZArith_base.v) theories/ZArith/Zcomplements.v - theories/ZArith/Zsqrt_compat.v theories/ZArith/Zpow_def.v theories/ZArith/Zpow_alt.v theories/ZArith/Zpower.v 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 *) -(* - 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. -- cgit v1.2.3