From ed89078e766b50628166dbdf84101941316cde64 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Mon, 8 May 2023 16:44:52 -0600
Subject: [PATCH] Apostol. Begin working through floor/ceiling exercises.

Also discovered the basic interval module so replaced custom
interval syntax with it.
---
 Bookshelf/Apostol/Chapter_1_11.lean | 33 +++++++++++++++++-------
 Common/Real.lean                    |  1 -
 Common/Real/Function/Step.lean      |  4 +--
 Common/Real/Int.lean                | 15 -----------
 Common/Real/Set.lean                |  1 -
 Common/Real/Set/Interval.lean       | 39 -----------------------------
 Common/Real/Set/Partition.lean      |  2 +-
 7 files changed, 27 insertions(+), 68 deletions(-)
 delete mode 100644 Common/Real/Int.lean
 delete mode 100644 Common/Real/Set/Interval.lean

diff --git a/Bookshelf/Apostol/Chapter_1_11.lean b/Bookshelf/Apostol/Chapter_1_11.lean
index 31b2387..61b4cef 100644
--- a/Bookshelf/Apostol/Chapter_1_11.lean
+++ b/Bookshelf/Apostol/Chapter_1_11.lean
@@ -1,7 +1,5 @@
 import Mathlib.Data.Real.Basic
 
-import Common.Real.Int
-
 /-! # Apostol.Chapter_1_11 -/
 
 namespace Apostol.Chapter_1_11
@@ -15,18 +13,35 @@ Prove that the greatest-integer function has the properties indicated.
 
 `⌊x + n⌋ = ⌊x⌋ + n` for every integer `n`.
 -/
-theorem exercise_4a (x : ℝ) (n : ℤ) : ⌊x + n⌋ = ⌊x⌋ + n := by
-  sorry
+theorem exercise_4a (x : ℝ) (n : ℤ) : ⌊x + n⌋ = ⌊x⌋ + n :=
+  Int.floor_add_int x n
 
-/-- ### Exercise 4b
+/-- ### Exercise 4b.1
 
 `⌊-x⌋ = -⌊x⌋` if `x` is an integer.
+-/
+theorem exercise_4b_1 (x : ℤ) : ⌊-x⌋ = -⌊x⌋ := by
+  simp only [Int.floor_int, id_eq]
+
+/-- ### Exercise 4b.2
+
 `⌊-x⌋ = -⌊x⌋ - 1` otherwise.
 -/
-theorem exercise_4b (x : ℝ)
-  : (Real.isInt x → ⌊-x⌋ = -⌊x⌋)
-  ∨ (¬Real.isInt x → ⌊-x⌋ = -⌊x⌋ - 1) := by
-  sorry
+theorem exercise_4b_2 (x : ℝ) (h : ∃ n : ℤ, x ∈ Set.Ioo ↑n (↑n + (1 : ℝ)))
+  : ⌊-x⌋ = -⌊x⌋ - 1 := by
+  rw [Int.floor_neg]
+  suffices ⌈x⌉ = ⌊x⌋ + 1 by
+    have := congrArg (HMul.hMul (-1)) this
+    simp only [neg_mul, one_mul, neg_add_rev, add_comm] at this
+    exact this
+  have ⟨n, hn⟩ := h
+  have hn' : x ∈ Set.Ico ↑n (↑n + (1 : ℝ)) :=
+    Set.mem_of_subset_of_mem Set.Ioo_subset_Ico_self hn
+  rw [Int.ceil_eq_iff, Int.floor_eq_on_Ico n x hn']
+  simp only [Int.cast_add, Int.cast_one, add_sub_cancel]
+  apply And.intro
+  · exact (Set.mem_Ioo.mp hn).left
+  · exact le_of_lt (Set.mem_Ico.mp hn').right
 
 /-- ### Exercise 4c
 
diff --git a/Common/Real.lean b/Common/Real.lean
index 170f320..7448338 100644
--- a/Common/Real.lean
+++ b/Common/Real.lean
@@ -1,7 +1,6 @@
 import Common.Real.Basic
 import Common.Real.Function
 import Common.Real.Geometry
-import Common.Real.Int
 import Common.Real.Rational
 import Common.Real.Sequence
 import Common.Real.Set
diff --git a/Common/Real/Function/Step.lean b/Common/Real/Function/Step.lean
index e718edd..2166881 100644
--- a/Common/Real/Function/Step.lean
+++ b/Common/Real/Function/Step.lean
@@ -14,7 +14,7 @@ open Partition
 Any member of a subinterval of a partition `P` must also be a member of `P`.
 -/
 lemma mem_open_subinterval_imp_mem_partition {p : Partition}
-  (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => i(x₁, x₂)))
+  (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => Set.Ioo x₁ x₂))
   (hy : y ∈ I) : y ∈ p := by
   cases h : p.xs with
   | nil =>
@@ -50,7 +50,7 @@ structure Step where
   p : Partition
   f : ∀ x ∈ p, ℝ
   const_open_subintervals :
-    ∀ (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => i(x₁, x₂))),
+    ∀ (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => Set.Ioo x₁ x₂)),
       ∃ c : ℝ, ∀ (hy : y ∈ I),
         f y (mem_open_subinterval_imp_mem_partition hI hy) = c
 
diff --git a/Common/Real/Int.lean b/Common/Real/Int.lean
deleted file mode 100644
index 446db2b..0000000
--- a/Common/Real/Int.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-import Mathlib.Data.Real.Basic
-
-/-! # Common.Real.Int
-
-Additional theorems and definitions useful in the context of integers.
--/
-
-namespace Real
-
-/--
-Check whether a real number is an integer.
--/
-def isInt (x : ℝ) := x = Int.floor x
-
-end Real
\ No newline at end of file
diff --git a/Common/Real/Set.lean b/Common/Real/Set.lean
index e7b2fc3..b790f51 100644
--- a/Common/Real/Set.lean
+++ b/Common/Real/Set.lean
@@ -1,3 +1,2 @@
 import Common.Real.Set.Basic
-import Common.Real.Set.Interval
 import Common.Real.Set.Partition
\ No newline at end of file
diff --git a/Common/Real/Set/Interval.lean b/Common/Real/Set/Interval.lean
deleted file mode 100644
index fb14b0d..0000000
--- a/Common/Real/Set/Interval.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-import Mathlib.Data.Real.Basic
-
-/-! # Common.Real.Set.Interval
-
-A syntactic description of the various types of continuous intervals permitted
-on the real number line.
--/
-
-/--
-Representation of a closed interval.
--/
-syntax (priority := high) "i[" term "," term "]" : term
-
-macro_rules
-  | `(i[$a, $b]) => `({ z | $a ≤ z ∧ z ≤ $b })
-
-/--
-Representation of an open interval.
--/
-syntax (priority := high) "i(" term "," term ")" : term
-
-macro_rules
-  | `(i($a, $b)) => `({ z | $a < z ∧ z < $b })
-
-/--
-Representation of a left half-open interval.
--/
-syntax (priority := high) "i(" term "," term "]" : term
-
-macro_rules
-  | `(i($a, $b]) => `({ z | $a < z ∧ z ≤ $b })
-
-/--
-Representation of a right half-open interval.
--/
-syntax (priority := high) "i[" term "," term ")" : term
-
-macro_rules
-  | `(i[$a, $b)) => `({ z | $a ≤ z ∧ z < $b })
\ No newline at end of file
diff --git a/Common/Real/Set/Partition.lean b/Common/Real/Set/Partition.lean
index d31c4ef..4368417 100644
--- a/Common/Real/Set/Partition.lean
+++ b/Common/Real/Set/Partition.lean
@@ -1,7 +1,7 @@
+import Mathlib.Data.Real.Basic
 import Mathlib.Data.List.Sort
 
 import Common.List.Basic
-import Common.Real.Set.Interval
 
 /-! # Common.Real.Set.Partition