From 56751a6f3ba335de6cfbcbda49f48742b0312edd Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 12 May 2023 11:08:18 -0600 Subject: [PATCH] Use a consistent naming convention. --- Bookshelf/Apostol/Chapter_I_03.lean | 13 ++++++------- Bookshelf/Enderton/Chapter_0.lean | 10 +++++----- Common/Real/Geometry/Area.lean | 16 ++++++++-------- Common/Real/Geometry/Basic.lean | 4 ++-- Common/Real/Geometry/Rectangle.lean | 16 ++++++++-------- Common/Real/Geometry/StepFunction.lean | 2 +- Common/Real/Sequence/Arithmetic.lean | 18 +++++++++--------- Common/Real/Sequence/Geometric.lean | 18 +++++++++--------- Common/Set/Basic.lean | 4 ++-- 9 files changed, 50 insertions(+), 51 deletions(-) diff --git a/Bookshelf/Apostol/Chapter_I_03.lean b/Bookshelf/Apostol/Chapter_I_03.lean index 2f02b47..c5f0b39 100644 --- a/Bookshelf/Apostol/Chapter_I_03.lean +++ b/Bookshelf/Apostol/Chapter_I_03.lean @@ -352,8 +352,8 @@ has a supremum, and `sup C = sup A + sup B`. theorem sup_minkowski_sum_eq_sup_add_sup (A B : Set ℝ) (a b : ℝ) (hA : A.Nonempty) (hB : B.Nonempty) (ha : IsLUB A a) (hb : IsLUB B b) - : IsLUB (Set.minkowski_sum A B) (a + b) := by - let C := Set.minkowski_sum A B + : IsLUB (Set.minkowskiSum A B) (a + b) := by + let C := Set.minkowskiSum A B -- First we show `a + b` is an upper bound of `C`. have hub : a + b ∈ upperBounds C := by rw [mem_upper_bounds_iff_forall_le] @@ -402,8 +402,8 @@ has an infimum, and `inf C = inf A + inf B`. theorem inf_minkowski_sum_eq_inf_add_inf (A B : Set ℝ) (hA : A.Nonempty) (hB : B.Nonempty) (ha : IsGLB A a) (hb : IsGLB B b) - : IsGLB (Set.minkowski_sum A B) (a + b) := by - let C := Set.minkowski_sum A B + : IsGLB (Set.minkowskiSum A B) (a + b) := by + let C := Set.minkowskiSum A B -- First we show `a + b` is a lower bound of `C`. have hlb : a + b ∈ lowerBounds C := by rw [mem_lower_bounds_iff_forall_ge] @@ -616,10 +616,9 @@ An integer `n` is called *even* if `n = 2m` for some integer `m`, and *odd* if ###### TODO -/ +def isEven (n : ℤ) := ∃ m : ℤ, n = 2 * m -def is_even (n : ℤ) := ∃ m : ℤ, n = 2 * m - -def is_odd (n : ℤ) := is_even (n + 1) +def isOdd (n : ℤ) := isEven (n + 1) /-! #### Exercise 11 diff --git a/Bookshelf/Enderton/Chapter_0.lean b/Bookshelf/Enderton/Chapter_0.lean index 5ef44b3..24b344c 100644 --- a/Bookshelf/Enderton/Chapter_0.lean +++ b/Bookshelf/Enderton/Chapter_0.lean @@ -219,13 +219,13 @@ private lemma n_pred_m_eq_m_k : n + (m - 1) = m + k := by rw [←Nat.add_sub_assoc p, Nat.add_comm, Nat.add_sub_assoc (n_geq_one p q)] conv => lhs; rw [n_pred_eq_k p q] -private def cast_norm : GTuple α (n, m - 1) → LTuple α (m + k) +private def castNorm : GTuple α (n, m - 1) → LTuple α (m + k) | xs => cast (by rw [q]) xs.norm -private def cast_fst : GTuple α (n, m - 1) → LTuple α (k + 1) +private def castFst : GTuple α (n, m - 1) → LTuple α (k + 1) | xs => cast (by rw [n_eq_succ_k p q]) xs.fst -private def cast_take (ys : LTuple α (m + k)) := +private def castTake (ys : LTuple α (m + k)) := cast (by rw [min_comm_succ_eq p]) (ys.take (k + 1)) /-- #### Lemma 0A @@ -234,7 +234,7 @@ Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. Th `x₁ = ⟨y₁, ..., yₖ₊₁⟩`. -/ theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : LTuple α (m + k)) - : (cast_norm q xs = ys) → (cast_fst p q xs = cast_take p ys) := by + : (castNorm q xs = ys) → (castFst p q xs = castTake p ys) := by intro h suffices HEq (cast (_ : LTuple α n = LTuple α (k + 1)) xs.fst) @@ -257,7 +257,7 @@ theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : LTuple α (m + k)) · exact Eq.symm (n_eq_min_comm_succ p q) · exact n_pred_eq_k p q · rw [GTuple.self_fst_eq_norm_take] - unfold cast_norm at h + unfold castNorm at h simp at h rw [←h, ←n_eq_succ_k p q] have h₂ := Eq.recOn diff --git a/Common/Real/Geometry/Area.lean b/Common/Real/Geometry/Area.lean index 6bae72b..39be5d3 100644 --- a/Common/Real/Geometry/Area.lean +++ b/Common/Real/Geometry/Area.lean @@ -89,7 +89,7 @@ axiom congruent_imp_area_eq_area -/ axiom rectangle_measurable (R : Rectangle) - : R.set_def ∈ 𝓜 + : R.toSet ∈ 𝓜 axiom rectangle_area_eq_mul_edge_lengths (R : Rectangle) : area (rectangle_measurable R) = R.width * R.height @@ -107,23 +107,23 @@ Every step region is measurable. This follows from the choice of scale axiom, and the fact all step regions are equivalent to the union of a collection of rectangles. -/ -theorem step_function_measurable (S : StepFunction) : S.set_def ∈ 𝓜 := by +theorem step_function_measurable (S : StepFunction) : S.toSet ∈ 𝓜 := by sorry -def forall_subset_between_step_imp_le_between_area (k : ℝ) (Q : Set ℝ²) := +def exhaustionProperty (k : ℝ) (Q : Set ℝ²) := ∀ S T : StepFunction, - (hS : S.set_def ⊆ Q) → - (hT : Q ⊆ T.set_def) → + (hS : S.toSet ⊆ Q) → + (hT : Q ⊆ T.toSet) → area (step_function_measurable S) ≤ k ∧ k ≤ area (step_function_measurable T) axiom exhaustion_exists_unique_imp_measurable (Q : Set ℝ²) - : (∃! k : ℝ, forall_subset_between_step_imp_le_between_area k Q) + : (∃! k : ℝ, exhaustionProperty k Q) → Q ∈ 𝓜 axiom exhaustion_exists_unique_imp_area_eq (Q : Set ℝ²) : ∃ k : ℝ, - (h : forall_subset_between_step_imp_le_between_area k Q ∧ - (∀ x : ℝ, forall_subset_between_step_imp_le_between_area x Q → x = k)) + (h : exhaustionProperty k Q ∧ + (∀ x : ℝ, exhaustionProperty x Q → x = k)) → area (exhaustion_exists_unique_imp_measurable Q ⟨k, h⟩) = k end Real.Geometry.Area diff --git a/Common/Real/Geometry/Basic.lean b/Common/Real/Geometry/Basic.lean index a4c7a1b..33ff993 100644 --- a/Common/Real/Geometry/Basic.lean +++ b/Common/Real/Geometry/Basic.lean @@ -20,10 +20,10 @@ definition once ported. -/ axiom angle (p₁ p₂ p₃ : ℝ²) : ℝ -noncomputable def port_geometry_euclidean_angle (p₁ p₂ p₃ : ℝ²) := +noncomputable def euclideanAngle (p₁ p₂ p₃ : ℝ²) := if p₁ = p₂ ∨ p₂ = p₃ then π / 2 else angle p₁ p₂ p₃ -notation "∠" => port_geometry_euclidean_angle +notation "∠" => euclideanAngle /-- Determine the distance between two points in `ℝ²`. diff --git a/Common/Real/Geometry/Rectangle.lean b/Common/Real/Geometry/Rectangle.lean index 5ebc700..d07f71f 100644 --- a/Common/Real/Geometry/Rectangle.lean +++ b/Common/Real/Geometry/Rectangle.lean @@ -28,7 +28,7 @@ namespace Rectangle The top-right corner of the rectangle, oriented with respect to the other vertices. -/ -def top_right (r : Rectangle) : ℝ² := +def topRight (r : Rectangle) : ℝ² := ( r.top_left.fst + r.bottom_right.fst - r.bottom_left.fst , r.top_left.snd + r.bottom_right.snd - r.bottom_left.snd ) @@ -36,23 +36,23 @@ def top_right (r : Rectangle) : ℝ² := /-- A `Rectangle` is the locus of points bounded by its edges. -/ -def set_def (r : Rectangle) : Set ℝ² := +def toSet (r : Rectangle) : Set ℝ² := sorry /-- A `Rectangle`'s top side is equal in length to its bottom side. -/ theorem dist_top_eq_dist_bottom (r : Rectangle) - : dist r.top_left r.top_right = dist r.bottom_left r.bottom_right := by - unfold top_right dist + : dist r.top_left r.topRight = dist r.bottom_left r.bottom_right := by + unfold topRight dist repeat rw [add_comm, sub_right_comm, add_sub_cancel'] /-- A `Rectangle`'s left side is equal in length to its right side. -/ theorem dist_left_eq_dist_right (r : Rectangle) - : dist r.top_left r.bottom_left = dist r.top_right r.bottom_right := by - unfold top_right dist + : dist r.top_left r.bottom_left = dist r.topRight r.bottom_right := by + unfold topRight dist repeat rw [ sub_sub_eq_add_sub, add_comm, @@ -86,7 +86,7 @@ namespace Point /-- A `Point` is the set consisting of just itself. -/ -def set_def (p : Point) : Set ℝ² := p.val.set_def +def toSet (p : Point) : Set ℝ² := p.val.toSet /-- The width of a `Point` is `0`. @@ -121,7 +121,7 @@ namespace LineSegment A `LineSegment` `s` is the set of points corresponding to the shortest line segment joining the two distinct points of `s`. -/ -def set_def (s : LineSegment) : Set ℝ² := s.val.set_def +def toSet (s : LineSegment) : Set ℝ² := s.val.toSet /-- Either the width or height of a `LineSegment` is zero. diff --git a/Common/Real/Geometry/StepFunction.lean b/Common/Real/Geometry/StepFunction.lean index c8c16df..25544a2 100644 --- a/Common/Real/Geometry/StepFunction.lean +++ b/Common/Real/Geometry/StepFunction.lean @@ -154,7 +154,7 @@ namespace StepFunction The set definition of a `StepFunction` is the region between the constant values of the function's subintervals and the real axis. -/ -def set_def (f : StepFunction) : Set ℝ² := sorry +def toSet (f : StepFunction) : Set ℝ² := sorry end StepFunction diff --git a/Common/Real/Sequence/Arithmetic.lean b/Common/Real/Sequence/Arithmetic.lean index 469047e..97a5500 100644 --- a/Common/Real/Sequence/Arithmetic.lean +++ b/Common/Real/Sequence/Arithmetic.lean @@ -72,7 +72,7 @@ The summation of the first `n + 1` terms of an arithmetic sequence. This function calculates the sum directly. -/ -noncomputable def sum_closed (seq : Arithmetic) (n : Nat) : Real := +noncomputable def sumClosed (seq : Arithmetic) (n : Nat) : Real := (n + 1) * (seq.a₀ + seq.termClosed n) / 2 /-- @@ -80,9 +80,9 @@ The summation of the first `n + 1` terms of an arithmetic sequence. This function calculates the sum recursively. -/ -def sum_recursive : Arithmetic → Nat → Real +def sumRecursive : Arithmetic → Nat → Real | seq, 0 => seq.a₀ - | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n + | seq, (n + 1) => seq.termClosed (n + 1) + seq.sumRecursive n /-- Simplify a summation of terms found in the proof of `sum_recursive_closed`. @@ -101,16 +101,16 @@ The recursive and closed definitions of the sum of an arithmetic sequence agree with one another. -/ theorem sum_recursive_closed (seq : Arithmetic) (n : Nat) - : seq.sum_recursive n = seq.sum_closed n := by + : seq.sumRecursive n = seq.sumClosed n := by induction n with | zero => - unfold sum_recursive sum_closed termClosed + unfold sumRecursive sumClosed termClosed norm_num | succ n ih => calc - seq.sum_recursive (n + 1) - _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl - _ = seq.termClosed (n + 1) + seq.sum_closed n := by rw [ih] + seq.sumRecursive (n + 1) + _ = seq.termClosed (n + 1) + seq.sumRecursive n := rfl + _ = seq.termClosed (n + 1) + seq.sumClosed n := by rw [ih] _ = seq.termClosed (n + 1) + ((n + 1) * (seq.a₀ + seq.termClosed n)) / 2 := rfl _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed n + seq.a₀ + seq.termClosed n) / 2 := by ring_nf _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * (seq.termClosed (n + 1) - seq.Δ) + seq.a₀ + (seq.termClosed (n + 1) - seq.Δ)) / 2 := by rw [@term_closed_sub_succ_delta n] @@ -118,6 +118,6 @@ theorem sum_recursive_closed (seq : Arithmetic) (n : Nat) _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed (n + 1) + 2 * seq.a₀) / 2 := by rw [sub_delta_summand_eq_two_mul_a₀] _ = ((n + 1) + 1) * (seq.a₀ + seq.termClosed (n + 1)) / 2 := by ring_nf _ = (↑(n + 1) + 1) * (seq.a₀ + seq.termClosed (n + 1)) / 2 := by simp only [Nat.cast_add, Nat.cast_one] - _ = seq.sum_closed (n + 1) := rfl + _ = seq.sumClosed (n + 1) := rfl end Real.Arithmetic \ No newline at end of file diff --git a/Common/Real/Sequence/Geometric.lean b/Common/Real/Sequence/Geometric.lean index 50b2187..7bda2e4 100644 --- a/Common/Real/Sequence/Geometric.lean +++ b/Common/Real/Sequence/Geometric.lean @@ -57,7 +57,7 @@ The summation of the first `n + 1` terms of a geometric sequence. This function calculates the sum directly. -/ -noncomputable def sum_closed_ratio_neq_one (seq : Geometric) (n : Nat) +noncomputable def sumClosed (seq : Geometric) (n : Nat) : seq.r ≠ 1 → Real := fun _ => (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) @@ -66,33 +66,33 @@ The summation of the first `n + 1` terms of a geometric sequence. This function calculates the sum recursively. -/ -def sum_recursive : Geometric → Nat → Real +def sumRecursive : Geometric → Nat → Real | seq, 0 => seq.a₀ - | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n + | seq, (n + 1) => seq.termClosed (n + 1) + seq.sumRecursive n /-- The recursive and closed definitions of the sum of a geometric sequence agree with one another. -/ theorem sum_recursive_closed (seq : Geometric) (n : Nat) (p : seq.r ≠ 1) - : sum_recursive seq n = sum_closed_ratio_neq_one seq n p := by + : sumRecursive seq n = sumClosed seq n p := by have h : 1 - seq.r ≠ 0 := by intro h rw [sub_eq_iff_eq_add, zero_add] at h exact False.elim (p (Eq.symm h)) induction n with | zero => - unfold sum_recursive sum_closed_ratio_neq_one + unfold sumRecursive sumClosed simp rw [mul_div_assoc, div_self h, mul_one] | succ n ih => calc - sum_recursive seq (n + 1) - _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl - _ = seq.termClosed (n + 1) + sum_closed_ratio_neq_one seq n p := by rw [ih] + sumRecursive seq (n + 1) + _ = seq.termClosed (n + 1) + seq.sumRecursive n := rfl + _ = seq.termClosed (n + 1) + seq.sumClosed n p := by rw [ih] _ = seq.a₀ * seq.r ^ (n + 1) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := rfl _ = seq.a₀ * seq.r ^ (n + 1) * (1 - seq.r) / (1 - seq.r) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := by rw [mul_div_cancel _ h] _ = (seq.a₀ * (1 - seq.r ^ (n + 1 + 1))) / (1 - seq.r) := by ring_nf - _ = sum_closed_ratio_neq_one seq (n + 1) p := rfl + _ = seq.sumClosed (n + 1) p := rfl end Real.Geometric \ No newline at end of file diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean index c1ed9ea..e255ca1 100644 --- a/Common/Set/Basic.lean +++ b/Common/Set/Basic.lean @@ -11,7 +11,7 @@ namespace Set The Minkowski sum of two sets `s` and `t` is the set `s + t = { a + b : a ∈ s, b ∈ t }`. -/ -def minkowski_sum {α : Type u} [Add α] (s t : Set α) := +def minkowskiSum {α : Type u} [Add α] (s t : Set α) := { x | ∃ a ∈ s, ∃ b ∈ t, x = a + b } /-- @@ -19,7 +19,7 @@ The sum of two sets is nonempty **iff** the summands are nonempty. -/ theorem nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α] {s t : Set α} - : (minkowski_sum s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by + : (minkowskiSum s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by apply Iff.intro · intro h have ⟨x, hx⟩ := h