Merge pull request #298 from Noaillesss/master

Axiom/Circle

EuclideanGeometry/Foundation/Axiom/Basic/Plane_trash.lean

@@ -0,0 +1,29 @@
+import EuclideanGeometry.Foundation.Axiom.Basic.Plane
+
+noncomputable section
+namespace EuclidGeom
+
+variable {P : Type _} [EuclideanPlane P]
+
+/- point reflection -/
+def pt_flip (A O : P) : P := (VEC A O) +ᵥ O
+
+theorem pt_flip_symm {A B O : P} (h : B = pt_flip A O) : A = pt_flip B O := by
+  rw [h]
+  unfold pt_flip Vec.mkPtPt
+  rw [vsub_vadd_eq_vsub_sub]
+  simp
+
+theorem pt_flip_vec_eq {A B O : P} (h : B = pt_flip A O) : VEC A O = VEC O B := by
+  rw [h, pt_flip, Vec.mkPtPt, Vec.mkPtPt]
+  simp
+
+theorem pt_flip_vec_eq_half_vec {A B O : P} (h : B = pt_flip A O) : VEC A O = (1 / 2 : ℝ) • (VEC A B) := by
+  symm
+  calc
+    _ = (1 / 2 : ℝ) • (VEC A O + VEC O B) := by rw [vec_add_vec]
+    _ = VEC A O := by
+      rw [← pt_flip_vec_eq h, ← two_smul ℝ, smul_smul]
+      simp
+
+end EuclidGeom

EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean

@@ -1,8 +1,8 @@
-import EuclideanGeometry.Foundation.Axiom.Position.Orientation
-import EuclideanGeometry.Foundation.Axiom.Triangle.Basic
 import EuclideanGeometry.Foundation.Axiom.Triangle.Trigonometric
 import EuclideanGeometry.Foundation.Axiom.Linear.Line_trash
-import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular
+import EuclideanGeometry.Foundation.Axiom.Linear.Ray_trash
+import EuclideanGeometry.Foundation.Axiom.Basic.Plane_trash
+import EuclideanGeometry.Foundation.Axiom.Position.Orientation_trash
 
 noncomputable section
 namespace EuclidGeom
@@ -123,11 +123,15 @@ instance pt_liesout_ne_pt_liesint {A B : P} {ω : Circle P} (h₁ : A LiesOut ω
   linarith
   ⟩
 
-theorem interior_of_circle_iff_inside_not_on_circle (p : P) (ω : Circle P) : p LiesInt ω ↔ (p LiesIn ω) ∧ (¬ p LiesOn ω) := by
+theorem liesint_iff_liesin_and_not_lieson (p : P) (ω : Circle P) : p LiesInt ω ↔ (p LiesIn ω) ∧ (¬ p LiesOn ω) := by
   show dist ω.center p < ω.radius ↔ (dist ω.center p ≤ ω.radius) ∧ (¬ dist ω.center p = ω.radius)
   push_neg
   exact lt_iff_le_and_ne
 
+theorem liesin_iff_liesint_or_lieson (A : P) (ω : Circle P) : A LiesIn ω ↔ (A LiesInt ω) ∨ (A LiesOn ω) := by
+  show dist ω.center A ≤ ω.radius ↔ (dist ω.center A < ω.radius) ∨ (dist ω.center A = ω.radius)
+  exact le_iff_lt_or_eq
+
 theorem mk_pt_pt_lieson {O A : P} [PtNe O A] : A LiesOn (CIR O A) := rfl
 
 theorem mk_pt_pt_diam_fst_lieson {A B : P} [_h : PtNe A B] : A LiesOn (mk_pt_pt_diam A B) := by
@@ -225,46 +229,286 @@ end Circle
 
 end Collinear
 
+
 section antipode
 
 namespace Circle
 
-def antipode (A : P) (ω : Circle P) : P := VEC A ω.center +ᵥ ω.center
-
-theorem antipode_lieson_circle {A : P} {ω : Circle P} {ha : A LiesOn ω} : (antipode A ω) LiesOn ω := by
-  show dist ω.center (antipode A ω) = ω.radius
-  rw [NormedAddTorsor.dist_eq_norm', antipode,  vsub_vadd_eq_vsub_sub]
-  simp only [vsub_self, zero_sub, norm_neg]
-  show ‖ω.center -ᵥ A‖ = ω.radius
-  rw [← NormedAddTorsor.dist_eq_norm', ha]
-
-theorem antipode_symm {A B : P} {ω : Circle P} {ha : A LiesOn ω} (h : antipode A ω = B) : antipode B ω = A := by
-  show VEC B ω.center +ᵥ ω.center = A
-  symm
-  apply (eq_vadd_iff_vsub_eq _ _ _).mpr
-  show VEC ω.center A = VEC B ω.center
-  have : VEC ω.center B = VEC A ω.center := by
-    show B -ᵥ ω.center = VEC A ω.center
-    apply (eq_vadd_iff_vsub_eq _ _ _).mp h.symm
-  rw [← neg_vec, ← this, neg_vec]
-
-theorem antipode_distinct {A : P} {ω : Circle P} {ha : A LiesOn ω} : antipode A ω ≠ A := by
-  intro eq
-  have : VEC ω.center A = VEC A ω.center := by
-    show A -ᵥ ω.center = VEC A ω.center
-    apply (eq_vadd_iff_vsub_eq _ _ _).mp eq.symm
-  have neq : A ≠ ω.center := (pt_lieson_ne_center ha).out
-  contrapose! neq
-  apply (eq_iff_vec_eq_zero _ _).mpr
-  have : 2 • (VEC ω.center A) = 0 := by
-    rw [two_smul]
-    nth_rw 1 [this]
-    rw [vec_add_vec]
-    simp
-  apply (two_nsmul_eq_zero ℝ _).mp this
+def IsAntipode {A B : P} (ω : Circle P) (_ha : A LiesOn ω) (_hb : B LiesOn ω) : Prop := B = pt_flip A ω.center
+
+theorem antipode_symm {A B : P} {ω : Circle P} (ha : A LiesOn ω) (hb : B LiesOn ω) : IsAntipode ω ha hb ↔ IsAntipode ω hb ha := by
+  unfold IsAntipode
+  constructor
+  · apply pt_flip_symm
+  apply pt_flip_symm
+
+theorem antipode_center_is_midpoint {A B : P} {ω : Circle P} (ha : A LiesOn ω) (hb : B LiesOn ω) (h : IsAntipode ω ha hb) : ω.center = (SEG A B).midpoint := pt_flip_center_is_midpoint h
+
+theorem antipode_iff_collinear (A B : P) {ω : Circle P} [h : PtNe B A] (ha : A LiesOn ω) (hb : B LiesOn ω) : IsAntipode ω ha hb ↔ Collinear A ω.center B := by
+  constructor
+  · intro hh
+    apply pt_flip_collinear hh
+  intro hcl
+  haveI : PtNe A ω.center := pt_lieson_ne_center ha
+  have hl : B LiesOn LIN ω.center A := Line.pt_pt_maximal (Collinear.perm₂₁₃ hcl)
+  have heq : VEC A ω.center = VEC ω.center B := by
+    apply vec_eq_dist_eq_of_lies_on_line_pt_pt_of_ptNe hl
+    rw [ha, hb]
+  unfold IsAntipode pt_flip
+  rw [heq, eq_vadd_iff_vsub_eq]
+  rfl
+
+theorem mk_pt_pt_diam_isantipode {A B : P} [h : PtNe A B] : IsAntipode (mk_pt_pt_diam A B) mk_pt_pt_diam_fst_lieson mk_pt_pt_diam_snd_lieson := by
+  have hc : Collinear A (SEG A B).midpoint B := by
+    apply Collinear.perm₁₃₂
+    apply Line.pt_pt_linear
+    show (SEG A B).midpoint LiesOn (SEG_nd A B).toLine
+    apply SegND.lies_on_toLine_of_lie_on
+    apply Seg.midpt_lies_on
+  exact (antipode_iff_collinear _ _ mk_pt_pt_diam_fst_lieson mk_pt_pt_diam_snd_lieson).mpr hc
 
 end Circle
 
 end antipode
 
+
+section arc
+
+variable (ω : Circle P)
+
+@[ext]
+structure Arc (P : Type _) [EuclideanPlane P] (ω : Circle P) where
+  source : P
+  target : P
+  ison : (source LiesOn ω) ∧ (target LiesOn ω)
+  endpts_ne : PtNe target source
+
+namespace Arc
+
+attribute [instance] Arc.endpts_ne
+
+protected def mk_pt_pt_circle {ω : Circle P} {A B : P} [h : PtNe B A] (ha : A LiesOn ω) (hb : B LiesOn ω) : Arc P ω where
+  source := A
+  target := B
+  ison := ⟨ha, hb⟩
+  endpts_ne := h
+
+end Arc
+
+scoped notation "ARC" => Arc.mk_pt_pt_circle
+
+namespace Arc
+
+protected def IsOn {ω : Circle P} (p : P) (β : Arc P ω) : Prop := (p LiesOn ω) ∧ (¬ p LiesOnLeft (DLIN β.source β.target))
+
+protected def ne_endpts {ω : Circle P} (p : P) (β : Arc P ω) : Prop := (p ≠ β.source) ∧ (p ≠ β.target)
+
+instance pt_ne_source {ω : Circle P} {p : P} {β : Arc P ω} (h : β.ne_endpts p) : PtNe β.source p := ⟨h.1.symm⟩
+
+instance pt_ne_target {ω : Circle P} {p : P} {β : Arc P ω} (h : β.ne_endpts p) : PtNe β.target p := ⟨h.2.symm⟩
+
+protected def IsInt {ω : Circle P} (p : P) (β : Arc P ω) : Prop := (Arc.IsOn p β) ∧ (β.ne_endpts p)
+
+protected def carrier {ω : Circle P} (β : Arc P ω) : Set P := { p : P | Arc.IsOn p β }
+
+protected def interior {ω : Circle P} (β : Arc P ω) : Set P := { p : P | Arc.IsInt p β }
+
+instance : Fig (Arc P ω) P where
+  carrier := Arc.carrier
+
+instance : Interior (Arc P ω) P where
+  interior := Arc.interior
+
+theorem center_ne_endpts {ω : Circle P} (β : Arc P ω) : β.ne_endpts ω.center := by
+  constructor
+  · intro h
+    have : β.source LiesOn ω := β.ison.1
+    rw [← h] at this
+    unfold lies_on Fig.carrier Circle.instFigCircle Circle.carrier Circle.IsOn at this
+    simp at this
+    have : ω.radius > 0 := ω.rad_pos
+    linarith
+  intro h
+  have : β.target LiesOn ω := β.ison.2
+  rw [← h] at this
+  unfold lies_on Fig.carrier Circle.instFigCircle Circle.carrier Circle.IsOn at this
+  simp at this
+  have : ω.radius > 0 := ω.rad_pos
+  linarith
+
+instance source_ne_center {ω : Circle P} (β : Arc P ω) : PtNe β.source ω.center := ⟨ (center_ne_endpts β).1.symm ⟩
+
+instance target_ne_center {ω : Circle P} (β : Arc P ω) : PtNe β.target ω.center := ⟨ (center_ne_endpts β).2.symm ⟩
+
+protected def complement {ω : Circle P} (β : Arc P ω) : Arc P ω where
+  source := β.target
+  target := β.source
+  ison := and_comm.mp β.ison
+  endpts_ne := β.endpts_ne.symm
+
+lemma pt_liesint_not_lieson_dlin {ω : Circle P} {β : Arc P ω} {p : P} (h : p LiesInt β) : ¬ (p LiesOn (DLIN β.source β.target)) := by
+  intro hl
+  have hl : p LiesOn (LIN β.source β.target) := hl
+  have hco : Collinear β.source β.target p := Line.pt_pt_linear hl
+  have hco' : ¬ (Collinear β.source β.target p) := Circle.three_pts_lieson_circle_not_collinear (hne₂ := ⟨h.2.2⟩) (hne₃ := ⟨h.2.1.symm⟩) β.ison.1 β.ison.2 h.1.1
+  tauto
+
+theorem pt_liesint_liesonright_dlin {ω : Circle P} {β : Arc P ω} {p : P} (h : p LiesInt β) : p LiesOnRight (DLIN β.source β.target) := by
+  have hnl : ¬ (p LiesOn (DLIN β.source β.target)) := pt_liesint_not_lieson_dlin h
+  have hnll : ¬ (p LiesOnLeft (DLIN β.source β.target)) := h.1.2
+  rcases DirLine.lieson_or_liesonleft_or_liesonright p (DLIN β.source β.target) with hh | (hh | hh)
+  · exfalso; tauto
+  · exfalso; tauto
+  exact hh
+
+theorem pt_liesint_complementary_liesonleft_dlin {ω : Circle P} {β : Arc P ω} {p : P} (h : p LiesInt β.complement) : p LiesOnLeft (DLIN β.source β.target) := by
+  have hh : p LiesOnRight (DLIN β.target β.source) := by apply pt_liesint_liesonright_dlin h
+  apply liesonleft_iff_liesonright_reverse.mpr
+  rw [← DirLine.pt_pt_rev_eq_rev]
+  exact hh
+
+end Arc
+
+end arc
+
+
+section chord
+
+@[ext]
+structure Chord (P : Type _) [EuclideanPlane P] (ω : Circle P) where
+  toSegND : SegND P
+  ison : (toSegND.source LiesOn ω) ∧ (toSegND.target LiesOn ω)
+
+instance Chord.IsND {ω : Circle P} (s : Chord P ω) : PtNe s.1.source s.1.target := ⟨s.1.2.symm⟩
+
+attribute [instance] Chord.IsND
+
+variable (ω : Circle P)
+
+namespace Chord
+
+protected def mk_pt_pt_circle {ω : Circle P} {A B : P} [h : PtNe A B] (ha : A LiesOn ω) (hb : B LiesOn ω) : Chord P ω where
+  toSegND := SEG_nd A B h.out.symm
+  ison := ⟨ha, hb⟩
+
+protected def IsOn {ω : Circle P} (A : P) (s : Chord P ω) : Prop := A LiesOn s.toSegND
+
+protected def IsInt {ω : Circle P} (A : P) (s : Chord P ω) : Prop := A LiesInt s.toSegND
+
+protected def carrier {ω : Circle P} (s : Chord P ω) : Set P := { p : P | Chord.IsOn p s }
+
+protected def interior {ω : Circle P} (s : Chord P ω) : Set P := { p : P | Chord.IsInt p s }
+
+instance : Fig (Chord P ω) P where
+  carrier := Chord.carrier
+
+instance : Interior (Chord P ω) P where
+  interior := Chord.interior
+
+protected def ne_endpts {ω : Circle P} (A : P) (s : Chord P ω) : Prop := (A ≠ s.1.source) ∧ (A ≠ s.1.target)
+
+theorem center_ne_endpts {ω : Circle P} (s : Chord P ω) : s.ne_endpts ω.center := by
+  constructor
+  · intro h
+    have : s.1.source LiesOn ω := s.2.1
+    rw [← h] at this
+    unfold lies_on Fig.carrier Circle.instFigCircle Circle.carrier Circle.IsOn at this
+    simp at this
+    have : ω.radius > 0 := ω.rad_pos
+    linarith
+  intro h
+  have : s.1.target LiesOn ω := s.2.2
+  rw [← h] at this
+  unfold lies_on Fig.carrier Circle.instFigCircle Circle.carrier Circle.IsOn at this
+  simp at this
+  have : ω.radius > 0 := ω.rad_pos
+  linarith
+
+instance source_ne_center {ω : Circle P} (s : Chord P ω) : PtNe s.1.source ω.center := ⟨ (center_ne_endpts s).1.symm ⟩
+
+instance target_ne_center {ω : Circle P} (s : Chord P ω) : PtNe s.1.target ω.center := ⟨ (center_ne_endpts s).2.symm ⟩
+
+protected def reverse {ω : Circle P} (s : Chord P ω) : Chord P ω where
+  toSegND := s.1.reverse
+  ison := ⟨s.2.2, s.2.1⟩
+
+theorem pt_liesint_liesint_circle {ω : Circle P} {A : P} {s : Chord P ω} (h : A LiesInt s) : A LiesInt ω := by
+  have : s.1 SegInCir ω := by
+    unfold Circle.seg_lies_inside_circle
+    constructor
+    · apply (Circle.liesin_iff_liesint_or_lieson _ _).mpr
+      right; exact s.2.1
+    apply (Circle.liesin_iff_liesint_or_lieson _ _).mpr
+    right; exact s.2.2
+  apply Circle.pt_lies_inside_circle_of_seg_inside_circle this h
+
+end Chord
+
+def Arc.toChord {ω : Circle P} (β : Arc P ω) : Chord P ω where
+  toSegND := SEG_nd β.source β.target β.endpts_ne.out
+  ison := β.ison
+
+def Chord.toArc {ω : Circle P} (s : Chord P ω) : Arc P ω where
+  source := s.1.source
+  target := s.1.target
+  ison := s.2
+  endpts_ne := ⟨s.1.2⟩
+
+theorem Circle.complementary_arc_toChord_eq_reverse {ω : Circle P} (β : Arc P ω) : β.complement.toChord = β.toChord.reverse := rfl
+
+theorem Circle.reverse_chord_toArc_eq_complement {ω : Circle P} (s : Chord P ω) : s.reverse.toArc = s.toArc.complement := rfl
+
+namespace Chord
+
+protected def length {ω : Circle P} (s : Chord P ω) : ℝ := s.1.length
+
+protected def IsDiameter {ω : Circle P} (s : Chord P ω) : Prop := ω.center LiesOn s
+
+theorem diameter_iff_antipide {ω : Circle P} {s : Chord P ω} : Chord.IsDiameter s ↔ Circle.IsAntipode ω s.2.1 s.2.2 := by
+  haveI : PtNe s.1.source s.1.target := ⟨s.1.2.symm⟩
+  constructor
+  · unfold Chord.IsDiameter
+    intro hl
+    have : Collinear s.1.source s.1.target ω.center := by
+      apply Line.pt_pt_linear
+      apply SegND.lies_on_toLine_of_lie_on hl
+    apply (Circle.antipode_iff_collinear s.1.source s.1.target s.2.1 s.2.2).mpr (Collinear.perm₁₃₂ this)
+  unfold Circle.IsAntipode
+  intro hf
+  have : VEC s.1.source ω.center = VEC ω.center s.1.target := pt_flip_vec_eq hf
+  unfold Chord.IsDiameter
+  show ω.center LiesOn s.1
+  apply SegND.lies_on_iff.mpr
+  use (1 / 2 : ℝ)
+  constructor
+  · norm_num
+  constructor
+  · norm_num
+  apply pt_flip_vec_eq_half_vec hf
+
+theorem diameter_length_eq_twice_radius {ω : Circle P} {s : Chord P ω} (h : Chord.IsDiameter s) : s.length = 2 * ω.radius := by
+  have : VEC s.1.source ω.center = VEC ω.center s.1.target := by
+    apply pt_flip_vec_eq
+    show Circle.IsAntipode ω s.2.1 s.2.2
+    apply diameter_iff_antipide.mp h
+  have : VEC s.1.source s.1.target = (2 : ℝ) • (VEC s.1.source ω.center) := by
+    calc
+      _ = VEC s.1.source ω.center + VEC ω.center s.1.target := by rw [vec_add_vec]
+      _ = (2 : ℝ) • (VEC s.1.source ω.center) := by rw [← this, two_smul]
+  calc
+    _ = s.1.length := rfl
+    _ = ‖VEC s.1.source s.1.target‖ := by
+      show dist s.1.source s.1.target = ‖VEC s.1.source s.1.target‖
+      rw [dist_comm, NormedAddTorsor.dist_eq_norm']
+      rfl
+    _ = 2 * (dist ω.center s.1.source) := by
+      rw [this, NormedAddTorsor.dist_eq_norm', norm_smul]
+      norm_num
+      rfl
+    _ = 2 * ω.radius := by rw [s.2.1]
+
+end Chord
+
+end chord
+
 end EuclidGeom