176 lines
3.9 KiB
Plaintext
176 lines
3.9 KiB
Plaintext
import Common.Geometry.Point
|
||
import Common.Geometry.Segment
|
||
import Common.Real.Trigonometry
|
||
|
||
/-! # Common.Geometry.Rectangle.Skew
|
||
|
||
A characterization of a skew rectangle.
|
||
-/
|
||
|
||
namespace Geometry.Rectangle
|
||
|
||
/--
|
||
A `Skew` rectangle is characterized by three points and the angle formed between
|
||
them.
|
||
|
||
A `Point` can alternatively be viewed as a `Skew` rectangle in which all three
|
||
points coincide. A `Segment` can alternatively be viewed as a `Skew` rectangle
|
||
in which two of the three points coincide. Note that, by definition of
|
||
`Point.angle`, such a situation does indeed yield an angle of `π / 2`.
|
||
-/
|
||
structure Skew where
|
||
tl : Point -- top left
|
||
bl : Point -- bottom left
|
||
br : Point -- bottom right
|
||
has_right_angle : Point.angle tl bl br = Real.pi / 2
|
||
|
||
namespace Skew
|
||
|
||
/--
|
||
The top-right corner of the `Skew` rectangle.
|
||
-/
|
||
def tr (r : Skew) : Point :=
|
||
⟨r.tl.x + r.br.x - r.bl.x, r.tl.y + r.br.y - r.bl.y⟩
|
||
|
||
/--
|
||
A `Skew` rectangle's top side is equal in length to its bottom side.
|
||
-/
|
||
theorem dist_top_eq_dist_bottom (r : Skew)
|
||
: Point.dist r.tl r.tr = Point.dist r.bl r.br := by
|
||
unfold tr Point.dist
|
||
simp only
|
||
repeat rw [add_comm, sub_right_comm, add_sub_cancel']
|
||
|
||
/--
|
||
A `Skew` rectangle's left side is equal in length to its right side.
|
||
-/
|
||
theorem dist_left_eq_dist_right (r : Skew)
|
||
: Point.dist r.tl r.bl = Point.dist r.tr r.br := by
|
||
unfold tr Point.dist
|
||
simp only
|
||
repeat rw [
|
||
sub_sub_eq_add_sub,
|
||
add_comm,
|
||
sub_add_eq_sub_sub,
|
||
sub_right_comm,
|
||
add_sub_cancel'
|
||
]
|
||
|
||
/--
|
||
Computes the width of a `Skew` rectangle.
|
||
-/
|
||
noncomputable def width (r : Skew) : ℝ :=
|
||
Point.dist r.bl r.br
|
||
|
||
/--
|
||
Computes the height of a `Skew` rectangle.
|
||
-/
|
||
noncomputable def height (r : Skew) : ℝ :=
|
||
Point.dist r.bl r.tl
|
||
|
||
/--
|
||
A mapping from a `Skew` rectangle to the set describing the region enclosed by
|
||
the rectangle.
|
||
-/
|
||
def toSet (r : Skew) : Set Point := sorry
|
||
|
||
/-! ## Point -/
|
||
|
||
/--
|
||
A `Point` is a `Skew` rectangle in which all points coincide.
|
||
-/
|
||
abbrev AsPoint := Subtype (fun r : Skew => r.tl = r.bl ∧ r.bl = r.br)
|
||
|
||
namespace AsPoint
|
||
|
||
/--
|
||
The function mapping a `Skew` rectangle with all points coinciding to a `Point`.
|
||
-/
|
||
def toPoint (p : AsPoint) : Point := p.val.tl
|
||
|
||
/--
|
||
The function mapping a `Point` to a `Skew` rectangle with all points coinciding.
|
||
-/
|
||
def fromPoint (p : Point) : AsPoint :=
|
||
have hp : Point.angle p p p = Real.pi / 2 := by
|
||
unfold Point.angle Real.euclideanAngle
|
||
simp
|
||
⟨Skew.mk p p p hp, by simp⟩
|
||
|
||
/--
|
||
An isomorphism between a `Skew` rectangle with all points coinciding and a
|
||
`Point`.
|
||
-/
|
||
def isoPoint : AsPoint ≃ Point :=
|
||
{
|
||
toFun := toPoint,
|
||
invFun := fromPoint,
|
||
left_inv := by
|
||
unfold Function.LeftInverse fromPoint toPoint
|
||
simp only
|
||
intro p
|
||
congr
|
||
· exact p.property.left
|
||
· rw [p.property.left]
|
||
exact p.property.right
|
||
right_inv := by
|
||
unfold Function.RightInverse Function.LeftInverse fromPoint toPoint
|
||
simp only
|
||
intro _
|
||
triv
|
||
}
|
||
|
||
/--
|
||
The width of an `AsPoint` is `0`.
|
||
-/
|
||
theorem width_eq_zero (p : AsPoint) : p.val.width = 0 := by
|
||
unfold Skew.width
|
||
rw [p.property.right]
|
||
unfold Point.dist
|
||
simp
|
||
|
||
/--
|
||
The height of an `AsPoint` is `0`.
|
||
-/
|
||
theorem height_eq_zero (p : AsPoint) : p.val.height = 0 := by
|
||
unfold Skew.height
|
||
rw [p.property.left]
|
||
unfold Point.dist
|
||
simp
|
||
|
||
end AsPoint
|
||
|
||
/-! ## Segment -/
|
||
|
||
/--
|
||
A `Segment` is a `Skew` rectangle in which two of three points coincide.
|
||
-/
|
||
abbrev AsSegment := Subtype (fun r : Skew =>
|
||
(r.tl = r.bl ∧ r.bl ≠ r.br) ∨ (r.tl ≠ r.bl ∧ r.bl = r.br))
|
||
|
||
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.inr ?_
|
||
unfold height
|
||
rw [h.left]
|
||
unfold Point.dist
|
||
simp
|
||
· intro h
|
||
refine Or.inl ?_
|
||
unfold width
|
||
rw [h.right]
|
||
unfold Point.dist
|
||
simp
|
||
|
||
end AsSegment
|
||
|
||
end Skew
|
||
|
||
end Geometry.Rectangle |