From 68d46e1a7dda37aa97c69870d4e40d293ddbba02 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 15 May 2023 14:07:42 -0600 Subject: [PATCH] Redefine an `Orthogonal` rectangle as a subtype of a `Skew` one. --- Common/Geometry/Area.lean | 2 +- Common/Geometry/Rectangle/Orthogonal.lean | 168 ++-------------------- Common/Geometry/StepFunction.lean | 11 +- Common/Real/Floor.lean | 1 - 4 files changed, 19 insertions(+), 163 deletions(-) diff --git a/Common/Geometry/Area.lean b/Common/Geometry/Area.lean index 3f5036f..4eb5dea 100644 --- a/Common/Geometry/Area.lean +++ b/Common/Geometry/Area.lean @@ -1,5 +1,5 @@ import Common.Geometry.Basic -import Common.Geometry.Rectangle.Orthogonal +import Common.Geometry.Rectangle.Skew import Common.Geometry.StepFunction /-! # Common.Geometry.Area diff --git a/Common/Geometry/Rectangle/Orthogonal.lean b/Common/Geometry/Rectangle/Orthogonal.lean index 234cb5a..41e367b 100644 --- a/Common/Geometry/Rectangle/Orthogonal.lean +++ b/Common/Geometry/Rectangle/Orthogonal.lean @@ -1,5 +1,4 @@ import Mathlib.Data.Fin.Basic -import Mathlib.Tactic.LibrarySearch import Common.Geometry.Point import Common.Geometry.Segment @@ -13,176 +12,27 @@ A characterization of an orthogonal rectangle. namespace Geometry.Rectangle /-- -An `Orthogonal` rectangle is characterized by two points on opposite corners. It -is assumed the edges of the rectangle are parallel to the coordinate axes. - -A `Point` can alternatively be viewed as an `Orthogonal` rectangle in which the -two points coincide. A horizontal or vertical `Segment` can alternatively be -viewed as an `Orthogonal` rectangle with width or height (but not both) `0`. +An `Orthogonal` rectangle is a `Skew` rectangle with edges parallel to the +coordinate axes. -/ -structure Orthogonal where - bl : Point -- bottom left - tr : Point -- top right +def Orthogonal := { r : Skew // r.bl.x = r.tl.x ∧ r.bl.y = r.br.y } namespace Orthogonal -/-- -The width of the `Orthogonal` rectangle. --/ -def width (r : Orthogonal) := r.tr.x - r.bl.x - -/-- -The height of the `Orthogonal` rectangle. --/ -def height (r : Orthogonal) := r.tr.y - r.bl.y - -/-- -The top-left corner of the `Orthogonal` rectangle. --/ -def tl (r : Orthogonal) : Point := ⟨r.bl.x, r.bl.y + r.height⟩ - -/-- -The bottom-right corner of the `Orthogonal` rectangle. --/ -def br (r : Orthogonal) : Point := ⟨r.bl.x + r.width, r.bl.y⟩ - /-- The `Set` of `Point`s enclosed in the region determined by the edges of the `Orthogonal` rectangle. Edges of the rectangle are included in the result set. -/ def toSet (r : Orthogonal) : Set Point := - { p | r.bl.x ≤ p.x ∧ p.x ≤ r.br.x ∧ r.bl.y ≤ p.y ∧ p.y ≤ r.tl.y } + { p | r.val.bl.x ≤ p.x ∧ p.x ≤ r.val.br.x ∧ + r.val.bl.y ≤ p.y ∧ p.y ≤ r.val.tl.y } /-- -An `Orthogonal` rectangle's top side is equal in length to its bottom side. +Show the `toSet` definition of an `Orthogonal` rectangle is in agreement with +its `Skew` counterpart. -/ -theorem dist_top_eq_dist_bottom (r : Orthogonal) - : Point.dist r.tl r.tr = Point.dist r.bl r.br := by - unfold tl br Point.dist width height - norm_num - -/-- -An `Orthogonal` rectangle's left side is equal in length to its right side. --/ -theorem dist_left_eq_dist_right (r : Orthogonal) - : Point.dist r.tl r.bl = Point.dist r.tr r.br := by - unfold tl br Point.dist width height - norm_num - -/-- -Convert an `Orthogonal` rectangle into a `Skew` one. --/ -def toSkew (r : Orthogonal) : Skew := ⟨r.tl, r.bl, r.br, sorry⟩ - -/-- -The set of `Orthogonal` rectangles are embedded in the set of `Skew` rectangles. --/ -def skewEmbedding : Orthogonal ↪ Skew := - have : Function.Injective toSkew := by - unfold Function.Injective - intro r₁ r₂ h - unfold toSkew at h - have ⟨⟨blx₁, bly₁⟩, ⟨trx₁, try₁⟩⟩ := r₁ - have ⟨⟨blx₂, bry₂⟩, ⟨trx₂, try₂⟩⟩ := r₂ - simp - simp at h - unfold tl br width height at h - simp at h - exact ⟨⟨h.left.left, h.right.left.right⟩, ⟨h.right.right.left, h.left.right⟩⟩ - ⟨toSkew, this⟩ - -/-! ## Point -/ - -/-- -A `Point` is an `Orthogonal` rectangle in which all points coincide. --/ -abbrev AsPoint := Subtype (fun r : Orthogonal => r.bl = r.tr) - -namespace AsPoint - -/-- -The function mapping an `Orthogonal` rectangle with all points coinciding to a -`Point`. --/ -def toPoint (p : AsPoint) : Point := p.val.tl - -/-- -The function mapping a `Point` to an `Orthogonal` rectangle with all points -coinciding. --/ -def fromPoint (p : Point) : AsPoint := ⟨Orthogonal.mk p p, by simp⟩ - -/-- -An isomorphism between an `Orthogonal` rectangle with all points coinciding and -a `Point`. --/ -def isoPoint : AsPoint ≃ Point := - { - toFun := toPoint, - invFun := fromPoint, - left_inv := by - unfold Function.LeftInverse fromPoint toPoint - intro ⟨r, hr⟩ - congr - repeat { - simp only - unfold tl height - rw [hr] - simp - } - right_inv := by - unfold Function.RightInverse Function.LeftInverse fromPoint toPoint - intro ⟨r, hr⟩ - unfold tl height - simp - } - -/-- -The width of an `AsPoint` is `0`. --/ -theorem width_eq_zero (p : AsPoint) : p.val.width = 0 := by - unfold Orthogonal.width - rw [p.property] - simp - -/-- -The height of an `AsPoint` is `0`. --/ -theorem height_eq_zero (p : AsPoint) : p.val.height = 0 := by - unfold Orthogonal.height - rw [p.property] - simp - -end AsPoint - -/-! ## Segment -/ - -/-- -A `Segment` is an `Orthogonal` rectangle either width or height equal to `0`. --/ -abbrev AsSegment := Subtype (fun r : Orthogonal => - (r.bl.x = r.tr.x ∧ r.bl.y ≠ r.tr.y) ∨ (r.bl.x ≠ r.tr.x ∧ r.bl.y = r.tr.y)) - -namespace AsSegment - -/-- -Either the width or height of an `AsSegment` is zero. --/ -theorem width_or_height_eq_zero (s : AsSegment) - : s.val.width = 0 ∨ s.val.height = 0 := by - apply Or.elim s.property - · intro h - refine Or.inl ?_ - unfold width - rw [h.left] - simp - · intro h - refine Or.inr ?_ - unfold height - rw [h.right] - simp - -end AsSegment +theorem orthogonal_set_eq_skew_set (r : Orthogonal) + : r.toSet = r.val.toSet := sorry end Orthogonal diff --git a/Common/Geometry/StepFunction.lean b/Common/Geometry/StepFunction.lean index 49b27cd..fd3119b 100644 --- a/Common/Geometry/StepFunction.lean +++ b/Common/Geometry/StepFunction.lean @@ -1,5 +1,4 @@ import Common.Finset -import Common.Geometry.Point import Common.Geometry.Rectangle.Orthogonal import Common.List.Basic import Common.Set.Partition @@ -34,7 +33,15 @@ def toSet (sf : StepFunction) : Set Point := ⋃ i ∈ Finset.finRange sf.p.ivls.length, let I := sf.p.ivls[i] Rectangle.Orthogonal.toSet - ⟨{ x := I.left, y := 0 }, { x := I.right, y := sf.toFun i }⟩ + ⟨ + { + tl := ⟨I.left, sf.toFun i⟩, + bl := ⟨I.left, 0⟩, + br := ⟨I.right, 0⟩, + has_right_angle := sorry + }, + by simp + ⟩ end StepFunction diff --git a/Common/Real/Floor.lean b/Common/Real/Floor.lean index f271657..fccedd5 100644 --- a/Common/Real/Floor.lean +++ b/Common/Real/Floor.lean @@ -1,7 +1,6 @@ import Mathlib.Algebra.BigOperators.Basic import Mathlib.Data.Real.Basic import Mathlib.Data.Finset.Basic -import Mathlib.Tactic.LibrarySearch /-! # Common.Real.Floor