From 049912a69df1fdea44d3037de06d69f235acd569 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 23 Jan 2025 14:52:58 +0100 Subject: [PATCH] Revert "Add Zfloor/Zceil to Reals" This reverts commit e11e3d438a4c03f90e35976ff619083472bdd366. --- doc/changelog/01-added/89-Zfloor.rst | 10 --- theories/Reals/Reals.v | 1 - theories/Reals/Zfloor.v | 129 --------------------------- 3 files changed, 140 deletions(-) delete mode 100644 doc/changelog/01-added/89-Zfloor.rst delete mode 100644 theories/Reals/Zfloor.v diff --git a/doc/changelog/01-added/89-Zfloor.rst b/doc/changelog/01-added/89-Zfloor.rst deleted file mode 100644 index 87e2044885..0000000000 --- a/doc/changelog/01-added/89-Zfloor.rst +++ /dev/null @@ -1,10 +0,0 @@ -- in `Reals` - - + new file `Zfloor.v` with definitions of `Zfloor` and `Zceil` - and corresponding lemmas `up_Zfloor`, `IZR_up_Zfloor`, - `Zfloor_bound`, `Zfloor_lub`, `Zfloor_eq`, `Zfloor_le`, - `Zfloor_addz`, `ZfloorZ`, `ZfloorNZ`, `ZfloorD_cond`, `Zceil_eq`, - `Zceil_le`, `Zceil_addz`, `ZceilD_cond`, `ZfloorB_cond`, - `ZceilB_cond` - (`#89 `_, - by Laurent Théry). diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index ac4c425229..8b532922d8 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -26,7 +26,6 @@ Require Export Rbase. Require Export Rfunctions. -Require Export Zfloor. Require Export SeqSeries. Require Export Rtrigo. Require Export Ranalysis. diff --git a/theories/Reals/Zfloor.v b/theories/Reals/Zfloor.v deleted file mode 100644 index 973471ca88..0000000000 --- a/theories/Reals/Zfloor.v +++ /dev/null @@ -1,129 +0,0 @@ -(******************************************************************************) -(* *) -(* Zfloor x == floor function : R -> Z *) -(* Zceil x == ceil function : R -> Z *) -(* *) -(******************************************************************************) - -Require Import Rbase Rfunctions Lra Lia. - -Open Scope R_scope. - -Definition Zfloor (x : R) := (up x - 1)%Z. - -Lemma up_Zfloor x : up x = (Zfloor x + 1)%Z. -Proof. unfold Zfloor; lia. Qed. - -Lemma IZR_up_Zfloor x : IZR (up x) = IZR (Zfloor x) + 1. -Proof. now rewrite up_Zfloor, plus_IZR. Qed. - -Lemma Zfloor_bound x : IZR (Zfloor x) <= x < IZR (Zfloor x) + 1. -Proof. -unfold Zfloor; rewrite minus_IZR. -generalize (archimed x); lra. -Qed. - -Lemma Zfloor_lub (z : Z) x : IZR z <= x -> (z <= Zfloor x)%Z. -Proof. -intro H. -assert (H1 : (z < Zfloor x + 1)%Z);[| lia]. -apply lt_IZR; rewrite plus_IZR. -now generalize (Zfloor_bound x); lra. -Qed. - -Lemma Zfloor_eq (z : Z) x : IZR z <= x < IZR z + 1 -> Zfloor x = z. -Proof. -intro xB. -assert (ZxB := Zfloor_bound x). -assert (B : (Zfloor x < z + 1 /\ z <= Zfloor x)%Z) ; [| lia]. -split; [|apply Zfloor_lub; lra]. -apply lt_IZR; rewrite plus_IZR; lra. -Qed. - -Lemma Zfloor_le x y : x <= y -> (Zfloor x <= Zfloor y)%Z. -Proof. -intro H; apply Zfloor_lub; generalize (Zfloor_bound x); lra. -Qed. - -Lemma Zfloor_addz (z: Z) x : Zfloor (x + IZR z) = (Zfloor x + z)%Z. -Proof. -assert (ZB := Zfloor_bound x). -now apply Zfloor_eq; rewrite plus_IZR; lra. -Qed. - -Lemma ZfloorZ (z : Z) : Zfloor (IZR z) = z. -Proof. now apply Zfloor_eq; lra. Qed. - - -Lemma ZfloorNZ (z : Z) : Zfloor (- IZR z) = (- z)%Z. -Proof. now rewrite <- opp_IZR, ZfloorZ. Qed. - -Lemma ZfloorD_cond r1 r2 : - if Rle_dec (IZR (Zfloor r1) + IZR (Zfloor r2) + 1) (r1 + r2) - then Zfloor (r1 + r2) = (Zfloor r1 + Zfloor r2 + 1)%Z - else Zfloor (r1 + r2) = (Zfloor r1 + Zfloor r2)%Z. -Proof. -destruct (Zfloor_bound r1, Zfloor_bound r2) as [H1 H2]. -case Rle_dec; intro H. - now apply Zfloor_eq; rewrite plus_IZR, plus_IZR; lra. -now apply Zfloor_eq; rewrite plus_IZR; lra. -Qed. - -Definition Zceil (x : R) := (- Zfloor (- x))%Z. - -Theorem Zceil_bound x : (IZR (Zceil x) - 1 < x <= IZR (Zceil x))%R. -Proof. -now unfold Zceil; generalize (Zfloor_bound (- x)); rewrite !opp_IZR; lra. -Qed. - -Theorem Zfloor_ceil_bound x : (IZR (Zfloor x) <= x <= IZR (Zceil x))%R. -Proof. now generalize (Zfloor_bound x) (Zceil_bound x); lra. Qed. - -Theorem ZceilN x : (Zceil (- x) = - Zfloor x)%Z. -Proof. now unfold Zceil; rewrite Ropp_involutive. Qed. - -Theorem ZfloorN x : (Zfloor (- x) = - Zceil x)%Z. -Proof. unfold Zceil; lia. Qed. - -Lemma Zceil_eq (z : Z) x : IZR z - 1 < x <= IZR z -> Zceil x = z. -Proof. -intro xB; assert (H : Zfloor (- x) = (- z)%Z); [|unfold Zceil; lia]. -now apply Zfloor_eq; rewrite opp_IZR; lra. -Qed. - -Lemma Zceil_le x y : x <= y -> (Zceil x <= Zceil y)%Z. -Proof. -intro xLy; apply Z.opp_le_mono; unfold Zceil; rewrite !Z.opp_involutive. -now apply Zfloor_le; lra. -Qed. - -Lemma Zceil_addz (z: Z) x : Zceil (x + IZR z) = (Zceil x + z)%Z. -Proof. -now unfold Zceil; rewrite Ropp_plus_distr, <- opp_IZR, Zfloor_addz; lia. -Qed. - -Lemma ZceilD_cond r1 r2 : - if Rle_dec (r1 + r2) (IZR (Zceil r1) + IZR (Zceil r2) - 1) - then Zceil (r1 + r2) = (Zceil r1 + Zceil r2 - 1)%Z - else Zceil (r1 + r2) = (Zceil r1 + Zceil r2)%Z. -Proof. -generalize (ZfloorD_cond (- r1) (- r2)). -now unfold Zceil; rewrite !opp_IZR; do 2 case Rle_dec; try lra; - rewrite Ropp_plus_distr; lia. -Qed. - -Lemma ZfloorB_cond r1 r2 : - if Rle_dec (IZR (Zfloor r1) - IZR (Zceil r2) + 1) (r1 - r2) - then Zfloor (r1 - r2) = (Zfloor r1 - Zceil r2 + 1)%Z - else Zfloor (r1 - r2) = (Zfloor r1 - Zceil r2)%Z. -Proof. -now generalize (ZfloorD_cond r1 (- r2)); rewrite !ZfloorN, !opp_IZR. -Qed. - -Lemma ZceilB_cond r1 r2 : - if Rle_dec (r1 - r2) (IZR (Zceil r1) - IZR (Zfloor r2) - 1) - then Zceil (r1 - r2) = (Zceil r1 - Zfloor r2 - 1)%Z - else Zceil (r1 - r2) = (Zceil r1 - Zfloor r2)%Z. -Proof. -now generalize (ZceilD_cond r1 (- r2)); rewrite !ZceilN, !opp_IZR. -Qed.