From 2ad6bd9724bfaffd8257fabc20a8ffdad55b4d4d Mon Sep 17 00:00:00 2001 From: thery Date: Tue, 21 Jan 2025 14:16:20 +0100 Subject: [PATCH] Add Zfloor/Zceil to Reals --- doc/changelog/01-added/89-Zfloor.rst | 10 +++ theories/Reals/Reals.v | 1 + theories/Reals/Zfloor.v | 129 +++++++++++++++++++++++++++ 3 files changed, 140 insertions(+) create mode 100644 doc/changelog/01-added/89-Zfloor.rst create mode 100644 theories/Reals/Zfloor.v diff --git a/doc/changelog/01-added/89-Zfloor.rst b/doc/changelog/01-added/89-Zfloor.rst new file mode 100644 index 0000000000..87e2044885 --- /dev/null +++ b/doc/changelog/01-added/89-Zfloor.rst @@ -0,0 +1,10 @@ +- 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 8b532922d8..ac4c425229 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -26,6 +26,7 @@ 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 new file mode 100644 index 0000000000..973471ca88 --- /dev/null +++ b/theories/Reals/Zfloor.v @@ -0,0 +1,129 @@ +(******************************************************************************) +(* *) +(* 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.