diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Plane_trash.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Plane_trash.lean new file mode 100644 index 00000000..b3e64077 --- /dev/null +++ b/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 diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean index 4d804b5d..c265c216 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean +++ b/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 diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean index 02cfdf5c..528118a5 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean @@ -1,7 +1,7 @@ import EuclideanGeometry.Foundation.Axiom.Circle.Basic import EuclideanGeometry.Foundation.Axiom.Circle.CCPosition import EuclideanGeometry.Foundation.Axiom.Circle.LCPosition -import EuclideanGeometry.Foundation.Axiom.Circle.IncribedAngle +import EuclideanGeometry.Foundation.Axiom.Circle.InscribedAngle noncomputable section namespace EuclidGeom @@ -15,20 +15,20 @@ namespace Circle -- Define the power of a point P relative to a circle ω with center O and radius r to be OP ^ 2 - r ^ 2 def power (ω : Circle P) (p : P) : ℝ := dist ω.center p ^ 2 - ω.radius ^ 2 -theorem inside_circle_iff_power_npos (p : P) (ω : Circle P) : p LiesIn ω ↔ ω.power p ≤ 0 := by +theorem pt_liesin_circle_iff_power_npos (p : P) (ω : Circle P) : p LiesIn ω ↔ ω.power p ≤ 0 := by apply Iff.trans _ sub_nonpos.symm unfold Circle.IsInside apply Iff.trans _ sq_le_sq.symm rw [abs_of_nonneg dist_nonneg, abs_of_pos ω.rad_pos] -theorem interior_of_circle_iff_power_neg (p : P) (ω : Circle P) : p LiesInt ω ↔ ω.power p < 0 := by +theorem pt_liesint_circle_iff_power_neg (p : P) (ω : Circle P) : p LiesInt ω ↔ ω.power p < 0 := by apply Iff.trans _ sub_neg.symm unfold lies_int Interior.interior instInteriorCircle Circle.interior Circle.IsInt simp apply Iff.trans _ sq_lt_sq.symm rw [abs_of_nonneg dist_nonneg, abs_of_pos ω.rad_pos] -theorem lies_on_circle_iff_power_zero (p : P) (ω : Circle P) : p LiesOn ω ↔ ω.power p = 0 := by +theorem pt_lieson_circle_iff_power_zero (p : P) (ω : Circle P) : p LiesOn ω ↔ ω.power p = 0 := by apply Iff.trans _ sub_eq_zero.symm unfold lies_on Fig.carrier instFigCircle Circle.carrier Circle.IsOn simp @@ -37,7 +37,7 @@ theorem lies_on_circle_iff_power_zero (p : P) (ω : Circle P) : p LiesOn ω ↔ apply le_iff_lt_or_eq.mpr left; exact ω.rad_pos -theorem outside_circle_iff_power_pos (p : P) (ω : Circle P) : p LiesOut ω ↔ 0 < ω.power p := by +theorem pt_liesout_circle_iff_power_pos (p : P) (ω : Circle P) : p LiesOut ω ↔ 0 < ω.power p := by apply Iff.trans _ sub_pos.symm unfold Circle.IsOutside apply Iff.trans _ sq_lt_sq.symm @@ -73,35 +73,35 @@ lemma tangent_circle_intersected {ω : Circle P} {p : P} (h : p LiesOut ω) : Ci apply sub_lt_iff_lt_add.mpr simp; exact ω.rad_pos -def pt_tangent_circle_pts {ω : Circle P} {p : P} (h : p LiesOut ω) : Tangents P where +def pt_outside_tangent_pts {ω : Circle P} {p : P} (h : p LiesOut ω) : Tangents P where left := (Inxpts (tangent_circle_intersected h)).left right := (Inxpts (tangent_circle_intersected h)).right -theorem tangents_lieson_circle {ω : Circle P} {p : P} (h : p LiesOut ω) : ((pt_tangent_circle_pts h).left LiesOn ω) ∧ ((pt_tangent_circle_pts h).right LiesOn ω) := by +theorem tangents_lieson_circle {ω : Circle P} {p : P} (h : p LiesOut ω) : ((pt_outside_tangent_pts h).left LiesOn ω) ∧ ((pt_outside_tangent_pts h).right LiesOn ω) := by rcases inx_pts_lieson_circles (tangent_circle_intersected h) with ⟨_, ⟨h₂, ⟨_, h₄⟩⟩⟩ exact ⟨h₂, h₄⟩ -lemma tangents_ne_pt {ω : Circle P} {p : P} (h : p LiesOut ω) : ((pt_tangent_circle_pts h).left ≠ p) ∧ ((pt_tangent_circle_pts h).right ≠ p) := by +lemma tangents_ne_pt {ω : Circle P} {p : P} (h : p LiesOut ω) : ((pt_outside_tangent_pts h).left ≠ p) ∧ ((pt_outside_tangent_pts h).right ≠ p) := by constructor · intro hp have h₁ : ω.radius < dist ω.center p := h - have : (pt_tangent_circle_pts h).left LiesOn ω := (tangents_lieson_circle h).1 + have : (pt_outside_tangent_pts h).left LiesOn ω := (tangents_lieson_circle h).1 rw [hp] at this have h₂ : dist ω.center p = ω.radius := this linarith intro hp have h₁ : ω.radius < dist ω.center p := h - have : (pt_tangent_circle_pts h).right LiesOn ω := (tangents_lieson_circle h).2 + have : (pt_outside_tangent_pts h).right LiesOn ω := (tangents_lieson_circle h).2 rw [hp] at this have h₂ : dist ω.center p = ω.radius := this linarith -lemma tangents_ne_center {ω : Circle P} {p : P} (h : p LiesOut ω) : ((pt_tangent_circle_pts h).left ≠ ω.center) ∧ ((pt_tangent_circle_pts h).right ≠ ω.center) := by - have hpos₁ : dist ω.center (pt_tangent_circle_pts h).left > 0 := by +lemma tangents_ne_center {ω : Circle P} {p : P} (h : p LiesOut ω) : ((pt_outside_tangent_pts h).left ≠ ω.center) ∧ ((pt_outside_tangent_pts h).right ≠ ω.center) := by + have hpos₁ : dist ω.center (pt_outside_tangent_pts h).left > 0 := by calc _ = ω.radius := (tangents_lieson_circle h).1 _ > 0 := ω.rad_pos - have hpos₂ : dist ω.center (pt_tangent_circle_pts h).right > 0 := by + have hpos₂ : dist ω.center (pt_outside_tangent_pts h).right > 0 := by calc _ = ω.radius := (tangents_lieson_circle h).2 _ > 0 := ω.rad_pos @@ -111,44 +111,58 @@ lemma tangents_ne_center {ω : Circle P} {p : P} (h : p LiesOut ω) : ((pt_tange apply dist_pos.mp rw [dist_comm]; exact hpos₂ -lemma tangents_perp₁ {ω : Circle P} {p : P} (h : p LiesOut ω) : (DLIN p (pt_tangent_circle_pts h).left (tangents_ne_pt h).1) ⟂ (DLIN ω.center (pt_tangent_circle_pts h).left (tangents_ne_center h).1) := by - haveI : PtNe ω.center p := (Circle.pt_liesout_ne_center h).symm - haveI : PtNe (pt_tangent_circle_pts h).left ω.center := ⟨(tangents_ne_center h).1⟩ - haveI : PtNe (pt_tangent_circle_pts h).left p := ⟨(tangents_ne_pt h).1⟩ - have heq₁ : ∠ p (pt_tangent_circle_pts h).left ω.center = ∡[π / 2] := by - apply inscribed_angle_of_diameter_eq_mod_pi_pt_pt_pt - · exact (inx_pts_lieson_circles (tangent_circle_intersected h)).1 - exact Arc.mk_pt_pt_diam_isantipode - show (DLIN p (pt_tangent_circle_pts h).left).toProj = (DLIN ω.center (pt_tangent_circle_pts h).left).toProj.perp +lemma tangents_perp₁ {ω : Circle P} {p : P} (h : p LiesOut ω) : (DLIN p (pt_outside_tangent_pts h).left (tangents_ne_pt h).1) ⟂ (DLIN ω.center (pt_outside_tangent_pts h).left (tangents_ne_center h).1) := by + haveI hi₁ : PtNe ω.center p := (Circle.pt_liesout_ne_center h).symm + haveI hi₂ : PtNe (pt_outside_tangent_pts h).left ω.center := ⟨(tangents_ne_center h).1⟩ + haveI hi₃ : PtNe (pt_outside_tangent_pts h).left p := ⟨(tangents_ne_pt h).1⟩ + have heq₁ : ∠ p (pt_outside_tangent_pts h).left ω.center = ∡[π / 2] := by + let ω' : Circle P := Circle.mk_pt_pt_diam p ω.center + let s : Chord P ω' := Chord.mk_pt_pt_circle (A := p) (B := ω.center) mk_pt_pt_diam_fst_lieson mk_pt_pt_diam_snd_lieson + apply iangle_of_diameter_eq_mod_pi (ω := ω') (s := s) + apply Chord.angle_mk_pt_is_iangle (inx_pts_lieson_circles (tangent_circle_intersected h)).1 + constructor + · show (pt_outside_tangent_pts h).left ≠ p + exact hi₃.out + show (pt_outside_tangent_pts h).left ≠ ω.center + exact hi₂.out + apply Chord.diameter_iff_antipide.mpr mk_pt_pt_diam_isantipode + show (DLIN p (pt_outside_tangent_pts h).left).toProj = (DLIN ω.center (pt_outside_tangent_pts h).left).toProj.perp calc - _ = (RAY p (pt_tangent_circle_pts h).left).toProj := rfl - _ = (RAY (pt_tangent_circle_pts h).left p).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt - _ = (RAY (pt_tangent_circle_pts h).left ω.center).toProj.perp := dir_perp_iff_dvalue_eq_pi_div_two.mpr heq₁ - _ = (RAY ω.center (pt_tangent_circle_pts h).left).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt] - _ = (DLIN ω.center (pt_tangent_circle_pts h).left).toProj.perp := rfl - -lemma tangents_perp₂ {ω : Circle P} {p : P} (h : p LiesOut ω) : (DLIN p (pt_tangent_circle_pts h).right (tangents_ne_pt h).2) ⟂ (DLIN ω.center (pt_tangent_circle_pts h).right (tangents_ne_center h).2) := by - haveI : PtNe ω.center p := (Circle.pt_liesout_ne_center h).symm - haveI : PtNe (pt_tangent_circle_pts h).right p := ⟨(tangents_ne_pt h).2⟩ - haveI : PtNe ω.center (pt_tangent_circle_pts h).right := ⟨(tangents_ne_center h).2.symm⟩ - have heq₂ : ∠ p (pt_tangent_circle_pts h).right ω.center = ∡[π / 2] := by - apply inscribed_angle_of_diameter_eq_mod_pi_pt_pt_pt - · exact (inx_pts_lieson_circles (tangent_circle_intersected h)).2.2.1 - apply Arc.mk_pt_pt_diam_isantipode - show (DLIN p (pt_tangent_circle_pts h).right).toProj = (DLIN ω.center (pt_tangent_circle_pts h).right).toProj.perp + _ = (RAY p (pt_outside_tangent_pts h).left).toProj := rfl + _ = (RAY (pt_outside_tangent_pts h).left p).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt + _ = (RAY (pt_outside_tangent_pts h).left ω.center).toProj.perp := dir_perp_iff_dvalue_eq_pi_div_two.mpr heq₁ + _ = (RAY ω.center (pt_outside_tangent_pts h).left).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt] + _ = (DLIN ω.center (pt_outside_tangent_pts h).left).toProj.perp := rfl + +lemma tangents_perp₂ {ω : Circle P} {p : P} (h : p LiesOut ω) : (DLIN p (pt_outside_tangent_pts h).right (tangents_ne_pt h).2) ⟂ (DLIN ω.center (pt_outside_tangent_pts h).right (tangents_ne_center h).2) := by + haveI hi₁ : PtNe ω.center p := (Circle.pt_liesout_ne_center h).symm + haveI hi₂ : PtNe (pt_outside_tangent_pts h).right p := ⟨(tangents_ne_pt h).2⟩ + haveI hi₃ : PtNe ω.center (pt_outside_tangent_pts h).right := ⟨(tangents_ne_center h).2.symm⟩ + have heq₂ : ∠ p (pt_outside_tangent_pts h).right ω.center = ∡[π / 2] := by + let ω' : Circle P := Circle.mk_pt_pt_diam p ω.center + let s : Chord P ω' := Chord.mk_pt_pt_circle (A := p) (B := ω.center) mk_pt_pt_diam_fst_lieson mk_pt_pt_diam_snd_lieson + apply iangle_of_diameter_eq_mod_pi (ω := ω') (s := s) + apply Chord.angle_mk_pt_is_iangle (inx_pts_lieson_circles (tangent_circle_intersected h)).2.2.1 + constructor + · show (pt_outside_tangent_pts h).right ≠ p + exact hi₂.out + show (pt_outside_tangent_pts h).right ≠ ω.center + exact hi₃.out.symm + apply Chord.diameter_iff_antipide.mpr mk_pt_pt_diam_isantipode + show (DLIN p (pt_outside_tangent_pts h).right).toProj = (DLIN ω.center (pt_outside_tangent_pts h).right).toProj.perp calc - _ = (RAY p (pt_tangent_circle_pts h).right).toProj := rfl - _ = (RAY (pt_tangent_circle_pts h).right p).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt - _ = (RAY (pt_tangent_circle_pts h).right ω.center).toProj.perp := dir_perp_iff_dvalue_eq_pi_div_two.mpr heq₂ - _ = (RAY ω.center (pt_tangent_circle_pts h).right).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt] - _ = (DLIN ω.center (pt_tangent_circle_pts h).right).toProj.perp := rfl + _ = (RAY p (pt_outside_tangent_pts h).right).toProj := rfl + _ = (RAY (pt_outside_tangent_pts h).right p).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt + _ = (RAY (pt_outside_tangent_pts h).right ω.center).toProj.perp := dir_perp_iff_dvalue_eq_pi_div_two.mpr heq₂ + _ = (RAY ω.center (pt_outside_tangent_pts h).right).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt] + _ = (DLIN ω.center (pt_outside_tangent_pts h).right).toProj.perp := rfl -theorem line_tangent_circle {ω : Circle P} {p : P} (h : p LiesOut ω) : ((DLIN p (pt_tangent_circle_pts h).left (tangents_ne_pt h).1) Tangent ω) ∧ ((DLIN p (pt_tangent_circle_pts h).right (tangents_ne_pt h).2) Tangent ω) := by +theorem line_tangent_circle {ω : Circle P} {p : P} (h : p LiesOut ω) : ((DLIN p (pt_outside_tangent_pts h).left (tangents_ne_pt h).1) Tangent ω) ∧ ((DLIN p (pt_outside_tangent_pts h).right (tangents_ne_pt h).2) Tangent ω) := by constructor · apply pt_pt_perp_tangent h (tangents_lieson_circle h).1 (tangents_perp₁ h) apply pt_pt_perp_tangent h (tangents_lieson_circle h).2 (tangents_perp₂ h) -theorem tangent_pts_eq_tangents {ω : Circle P} {p : P} (h : p LiesOut ω) : (Tangentpt (line_tangent_circle h).1 = (pt_tangent_circle_pts h).left) ∧ (Tangentpt (line_tangent_circle h).2 = (pt_tangent_circle_pts h).right) := by +theorem tangent_pts_eq_tangents {ω : Circle P} {p : P} (h : p LiesOut ω) : (Tangentpt (line_tangent_circle h).1 = (pt_outside_tangent_pts h).left) ∧ (Tangentpt (line_tangent_circle h).2 = (pt_outside_tangent_pts h).right) := by constructor · symm apply pt_pt_perp_eq_tangent_pt h (tangents_lieson_circle h).1 (tangents_perp₁ h) @@ -167,34 +181,43 @@ lemma tangent_length_sq_eq_power {p : P} {l : DirLine P} {ω : Circle P} (h₁ : exact (inx_pts_lieson_circle (intersect_iff_tangent_or_secant.mpr (Or.inl h₁))).1 _ = power ω p := rfl -theorem length_of_tangent {ω : Circle P} {p : P} (h : p LiesOut ω) : dist p (pt_tangent_circle_pts h).left = dist p (pt_tangent_circle_pts h).right := by +lemma tangent_length_sq_eq_power' {ω : Circle P} {A B : P} (ha : A LiesOut ω) (hb : B LiesOn ω) (h : (DLIN A B (pt_liesout_ne_pt_lieson ha hb).out.symm) Tangent ω) : (dist A B) ^ 2 = power ω A := by + haveI : PtNe A B := pt_liesout_ne_pt_lieson ha hb + rw [pt_pt_tangent_eq_tangent_pt ha hb h, tangent_length_sq_eq_power h DirLine.fst_pt_lies_on_mk_pt_pt] + +theorem length_of_tangent_eq {ω : Circle P} {p : P} (h : p LiesOut ω) : dist p (pt_outside_tangent_pts h).left = dist p (pt_outside_tangent_pts h).right := by apply (sq_eq_sq (by exact dist_nonneg) (by exact dist_nonneg)).mp - haveI : PtNe (pt_tangent_circle_pts h).left p := ⟨(tangents_ne_pt h).1⟩ - haveI : PtNe (pt_tangent_circle_pts h).right p := ⟨(tangents_ne_pt h).2⟩ - have hl₁ : p LiesOn (DLIN p (pt_tangent_circle_pts h).left) := DirLine.fst_pt_lies_on_mk_pt_pt - have hl₂ : p LiesOn (DLIN p (pt_tangent_circle_pts h).right) := DirLine.fst_pt_lies_on_mk_pt_pt + haveI : PtNe (pt_outside_tangent_pts h).left p := ⟨(tangents_ne_pt h).1⟩ + haveI : PtNe (pt_outside_tangent_pts h).right p := ⟨(tangents_ne_pt h).2⟩ + have hl₁ : p LiesOn (DLIN p (pt_outside_tangent_pts h).left) := DirLine.fst_pt_lies_on_mk_pt_pt + have hl₂ : p LiesOn (DLIN p (pt_outside_tangent_pts h).right) := DirLine.fst_pt_lies_on_mk_pt_pt rw [← (tangent_pts_eq_tangents h).1, tangent_length_sq_eq_power _ hl₁, ← (tangent_pts_eq_tangents h).2, tangent_length_sq_eq_power _ hl₂] +theorem length_of_tangent_eq' {ω : Circle P} {A B C : P} (ha : A LiesOut ω) (hb : B LiesOn ω) (hc : C LiesOn ω) (ht₁ : (DLIN A B (pt_liesout_ne_pt_lieson ha hb).out.symm) Tangent ω) (ht₂ : (DLIN A C (pt_liesout_ne_pt_lieson ha hc).out.symm) Tangent ω) : dist A B = dist A C := by + apply (sq_eq_sq (by exact dist_nonneg) (by exact dist_nonneg)).mp + rw [tangent_length_sq_eq_power' ha hb ht₁, tangent_length_sq_eq_power' ha hc ht₂] + end Circle end tangent -section position + +section powerthm namespace Circle -lemma liesout_ne_inxpts {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (_h₂ : p LiesOn l) (h₃ : p LiesOut ω) : (p ≠ (Inxpts h₁).front) ∧ (p ≠ (Inxpts h₁).back) := by +lemma pt_liesout_ne_inxpts {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (_h₂ : p LiesOn l) (h₃ : p LiesOut ω) : (p ≠ (Inxpts h₁).front) ∧ (p ≠ (Inxpts h₁).back) := by constructor · apply (pt_liesout_ne_pt_lieson h₃ (inx_pts_lieson_circle h₁).1).out apply (pt_liesout_ne_pt_lieson h₃ (inx_pts_lieson_circle h₁).2).out -lemma liesint_ne_inxpts {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (_h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (p ≠ (Inxpts h₁).front) ∧ (p ≠ (Inxpts h₁).back) := by +lemma pt_liesint_ne_inxpts {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (_h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (p ≠ (Inxpts h₁).front) ∧ (p ≠ (Inxpts h₁).back) := by constructor · apply (pt_liesint_ne_pt_lieson h₃ (inx_pts_lieson_circle h₁).1).out apply (pt_liesint_ne_pt_lieson h₃ (inx_pts_lieson_circle h₁).2).out -theorem liesout_back_lieson_ray_front {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesOut ω) : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front (liesout_ne_inxpts h₁ h₂ h₃).1.symm) := by - haveI : PtNe p (Inxpts h₁).front := ⟨(liesout_ne_inxpts h₁ h₂ h₃).1⟩ +theorem pt_liesout_back_lieson_ray_pt_front {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesOut ω) : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front (pt_liesout_ne_inxpts h₁ h₂ h₃).1.symm) := by + haveI : PtNe p (Inxpts h₁).front := ⟨(pt_liesout_ne_inxpts h₁ h₂ h₃).1⟩ by_cases heq : (Inxpts h₁).front = (Inxpts h₁).back · simp_rw [← heq] apply Ray.snd_pt_lies_on_mk_pt_pt @@ -224,8 +247,8 @@ theorem liesout_back_lieson_ray_front {ω : Circle P} {p : P} {l : DirLine P} (h _ = dist (Inxpts h₁).front (SEG (Inxpts h₁).front (Inxpts h₁).back).midpoint := by rw [abs_of_nonneg dist_nonneg] exact (not_lies_on_seg_nd_iff_lies_on_ray h₂').mp <| ((SEG_nd (DirLC.Inxpts h₁).front (DirLC.Inxpts h₁).back).dist_midpt_gt_iff_not_lies_on_of_lies_on_toLine h₂').mp hgt -theorem liesint_back_lieson_ray_front_reverse {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front (liesint_ne_inxpts h₁ h₂ h₃).1.symm).reverse := by - haveI : PtNe p (Inxpts h₁).front := ⟨(liesint_ne_inxpts h₁ h₂ h₃).1⟩ +theorem pt_liesint_back_lieson_ray_pt_front_reverse {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front (pt_liesint_ne_inxpts h₁ h₂ h₃).1.symm).reverse := by + haveI : PtNe p (Inxpts h₁).front := ⟨(pt_liesint_ne_inxpts h₁ h₂ h₃).1⟩ have hs : dist_pt_line ω.center l.toLine < ω.radius := by calc _ ≤ dist ω.center p := dist_pt_line_shortest _ _ h₂ @@ -259,15 +282,7 @@ theorem liesint_back_lieson_ray_front_reverse {ω : Circle P} {p : P} {l : DirLi apply (lies_int_seg_nd_iff_lies_on_ray_reverse h₂').mp exact ((SEG_nd (Inxpts h₁).front (Inxpts h₁).back).dist_midpt_lt_iff_lies_int_of_lies_on_toLine h₂').mp hgt -end Circle - -end position - -section power - -namespace Circle - -theorem circle_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) : ⟪VEC p (Inxpts h₁).front, VEC p (Inxpts h₁).back⟫_ℝ = power ω p := by +theorem power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) : ⟪VEC p (Inxpts h₁).front, VEC p (Inxpts h₁).back⟫_ℝ = power ω p := by rcases intersect_iff_tangent_or_secant.mp h₁ with h | h · have heq : (Inxpts h₁).back = (Inxpts h₁).front := (inx_pts_same_iff_tangent h₁).mpr h rw [heq, Vec.real_inner_apply _ _, ← Vec.norm_sq] @@ -314,8 +329,8 @@ theorem circle_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine _ = power ω p := rfl theorem chord_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesInt ω) : (dist p (Inxpts h₁).front) * (dist p (Inxpts h₁).back) = - power ω p := by - haveI hne : PtNe p (Inxpts h₁).front := ⟨(liesint_ne_inxpts h₁ h₂ h₃).1⟩ - have hl : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front).reverse := liesint_back_lieson_ray_front_reverse h₁ h₂ h₃ + haveI hne : PtNe p (Inxpts h₁).front := ⟨(pt_liesint_ne_inxpts h₁ h₂ h₃).1⟩ + have hl : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front).reverse := pt_liesint_back_lieson_ray_pt_front_reverse h₁ h₂ h₃ rcases pt_lies_on_ray_rev_iff_vec_opposite_dir.mp hl with ⟨t, tnonpos, ht⟩ have heq : dist p (Inxpts h₁).back = -t := by calc @@ -329,7 +344,7 @@ theorem chord_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine. _ = (t * (dist p (Inxpts h₁).front)⁻¹) • (VEC p (Inxpts h₁).front) := by rw [smul_smul] symm calc - _ = -⟪VEC p (Inxpts h₁).front, VEC p (Inxpts h₁).back⟫_ℝ := by rw [circle_power_thm h₁ h₂] + _ = -⟪VEC p (Inxpts h₁).front, VEC p (Inxpts h₁).back⟫_ℝ := by rw [power_thm h₁ h₂] _ = -⟪VEC p (Inxpts h₁).front, (t * (dist p (Inxpts h₁).front)⁻¹) • (VEC p (Inxpts h₁).front)⟫_ℝ := by rw [ht'] _ = -(t * (dist p (Inxpts h₁).front)⁻¹) * ‖VEC p (Inxpts h₁).front‖ ^ 2 := by rw [real_inner_smul_right, Vec.real_inner_apply _ _, ← Vec.norm_sq] @@ -341,8 +356,8 @@ theorem chord_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine. apply dist_ne_zero.mpr hne.out.symm theorem secant_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine.IsIntersected l ω) (h₂ : p LiesOn l) (h₃ : p LiesOut ω) : (dist p (Inxpts h₁).front) * (dist p (Inxpts h₁).back) = power ω p := by - haveI hne : PtNe p (Inxpts h₁).front := ⟨(liesout_ne_inxpts h₁ h₂ h₃).1⟩ - have hl : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front) := liesout_back_lieson_ray_front h₁ h₂ h₃ + haveI hne : PtNe p (Inxpts h₁).front := ⟨(pt_liesout_ne_inxpts h₁ h₂ h₃).1⟩ + have hl : (Inxpts h₁).back LiesOn (RAY p (Inxpts h₁).front) := pt_liesout_back_lieson_ray_pt_front h₁ h₂ h₃ rcases Ray.lies_on_iff.mp hl with ⟨t, tnonneg, ht⟩ have heq : dist p (Inxpts h₁).back = t := by calc @@ -356,7 +371,7 @@ theorem secant_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine _ = (t * (dist p (Inxpts h₁).front)⁻¹) • (VEC p (Inxpts h₁).front) := by rw [smul_smul] symm calc - _ = ⟪VEC p (Inxpts h₁).front, VEC p (Inxpts h₁).back⟫_ℝ := by rw [circle_power_thm h₁ h₂] + _ = ⟪VEC p (Inxpts h₁).front, VEC p (Inxpts h₁).back⟫_ℝ := by rw [power_thm h₁ h₂] _ = ⟪VEC p (Inxpts h₁).front, (t * (dist p (Inxpts h₁).front)⁻¹) • (VEC p (Inxpts h₁).front)⟫_ℝ := by rw [ht'] _ = (t * (dist p (Inxpts h₁).front)⁻¹) * ‖VEC p (Inxpts h₁).front‖ ^ 2 := by rw [real_inner_smul_right, Vec.real_inner_apply _ _, ← Vec.norm_sq] _ = (dist p (Inxpts h₁).front) * (dist p (Inxpts h₁).back) := by @@ -364,16 +379,13 @@ theorem secant_power_thm {ω : Circle P} {p : P} {l : DirLine P} (h₁ : DirLine rw [← NormedAddTorsor.dist_eq_norm', dist_comm, heq, mul_assoc, mul_comm, pow_two, inv_mul_cancel_left₀] apply dist_ne_zero.mpr hne.out.symm -end Circle +theorem intersecting_chords_thm {ω : Circle P} {S : P} {s₁ s₂ : Chord P ω} (h : S LiesInt ω) (h₁ : S LiesOn s₁) (h₂ : S LiesOn s₂) : (dist S s₁.1.source) * (dist S s₁.1.target) = (dist S s₂.1.source) * (dist S s₂.1.target) := sorry -end power - -section radical_axis - -namespace Circle +theorem intersecting_secants_thm {ω : Circle P} {S : P} {l₁ l₂ : DirLine P} (h : S LiesOut ω) (h₁ : S LiesOn l₁) (h₂ : S LiesOn l₂) (hx₁ : DirLine.IsIntersected l₁ ω) (hx₂ : DirLine.IsIntersected l₂ ω) : (dist S (Inxpts hx₁).front) * (dist S (Inxpts hx₁).back) = (dist S (Inxpts hx₂).front) * (dist S (Inxpts hx₂).back) := by + rw [secant_power_thm hx₁ h₁ h, secant_power_thm hx₂ h₂ h] end Circle -end radical_axis +end powerthm end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean b/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean deleted file mode 100644 index 11fe61ea..00000000 --- a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean +++ /dev/null @@ -1,262 +0,0 @@ -import EuclideanGeometry.Foundation.Axiom.Circle.Basic -import EuclideanGeometry.Foundation.Axiom.Position.Angle_ex2 -import EuclideanGeometry.Foundation.Axiom.Position.Orientation_trash -import EuclideanGeometry.Foundation.Axiom.Triangle.IsocelesTriangle_trash -import EuclideanGeometry.Foundation.Axiom.Basic.Angle_trash -import EuclideanGeometry.Foundation.Axiom.Triangle.Basic -import EuclideanGeometry.Foundation.Axiom.Triangle.Basic_ex - -noncomputable section -namespace EuclidGeom - -open AngValue Angle - -@[ext] -structure Arc (P : Type _) [EuclideanPlane P] where - source : P - target : P - circle : Circle P - ison : (source LiesOn circle) ∧ (target LiesOn circle) - endpts_ne : PtNe target source - -variable {P : Type _} [EuclideanPlane P] - -namespace Arc - -attribute [instance] Arc.endpts_ne - -protected def mk_pt_pt_circle (A B : P) {ω : Circle P} [h : PtNe B A] (ha : A LiesOn ω) (hb : B LiesOn ω) : Arc P where - source := A - target := B - circle := ω - ison := ⟨ha, hb⟩ - endpts_ne := h - -end Arc - -scoped notation "ARC" => Arc.mk_pt_pt_circle - - -section position - -namespace Arc - -protected def IsOn (p : P) (β : Arc P) : Prop := (p LiesOn β.circle) ∧ (¬ p LiesOnLeft (DLIN β.source β.target)) - -def Isnot_arc_endpts (p : P) (β : Arc P) : Prop := (p ≠ β.source) ∧ (p ≠ β.target) - -instance (p : P) (β : Arc P) (h : Isnot_arc_endpts p β) : PtNe β.source p := ⟨h.1.symm⟩ - -instance (p : P) (β : Arc P) (h : Isnot_arc_endpts p β) : PtNe β.target p := ⟨h.2.symm⟩ - -protected def IsInt (p : P) (β : Arc P) : Prop := (Arc.IsOn p β) ∧ (Isnot_arc_endpts p β) - -protected def carrier (β : Arc P) : Set P := { p : P | Arc.IsOn p β } - -protected def interior (β : 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_isnot_arc_endpts (β : Arc P) : Isnot_arc_endpts β.circle.center β := by - constructor - · intro h - have : β.source LiesOn β.circle := β.ison.1 - rw [← h] at this - unfold lies_on Fig.carrier Circle.instFigCircle Circle.carrier Circle.IsOn at this - simp at this - have : β.circle.radius > 0 := β.circle.rad_pos - linarith - intro h - have : β.target LiesOn β.circle := β.ison.2 - rw [← h] at this - unfold lies_on Fig.carrier Circle.instFigCircle Circle.carrier Circle.IsOn at this - simp at this - have : β.circle.radius > 0 := β.circle.rad_pos - linarith - -instance (β : Arc P) : PtNe β.source β.circle.center := ⟨ (center_isnot_arc_endpts β).1.symm ⟩ -instance (β : Arc P) : PtNe β.target β.circle.center := ⟨ (center_isnot_arc_endpts β).2.symm ⟩ - -def complement (β : Arc P) : Arc P where - source := β.target - target := β.source - circle := β.circle - ison := and_comm.mp β.ison - endpts_ne := β.endpts_ne.symm - -lemma liesint_arc_not_lieson_dlin {β : 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 liesint_arc_liesonright_dlin {β : Arc P} {p : P} (h : p LiesInt β) : p LiesOnRight (DLIN β.source β.target) := by - have hnl : ¬ (p LiesOn (DLIN β.source β.target)) := liesint_arc_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 liesint_complementary_arc_liesonleft_dlin {β : Arc P} {p : P} (h : p LiesInt β.complement) : p LiesOnLeft (DLIN β.source β.target) := by - have hh : p LiesOnRight (DLIN β.target β.source) := by apply liesint_arc_liesonright_dlin h - apply liesonleft_iff_liesonright_reverse.mpr - rw [← DirLine.pt_pt_rev_eq_rev] - exact hh - -end Arc - -end position - - -section angle - -namespace Arc - -protected def angle_mk_pt_arc (p : P) (β : Arc P) (h : Isnot_arc_endpts p β) : Angle P := ANG β.source p β.target h.1.symm h.2.symm - -protected def cangle (β : Arc P) : Angle P := Arc.angle_mk_pt_arc β.circle.center β (center_isnot_arc_endpts β) - -protected def IsMajor (β : Arc P) : Prop := β.cangle.value.toReal < 0 - -protected def IsMinor (β : Arc P) : Prop := β.cangle.value.toReal > 0 - -protected def IsAntipode (A B : P) {ω : Circle P} [_h : PtNe B A] (h₁ : A LiesOn ω) (h₂ : B LiesOn ω) : Prop := (ARC A B h₁ h₂).cangle.value = π - -theorem cangle_of_complementary_arc_are_opposite (β : Arc P) : β.cangle.value = - β.complement.cangle.value := by - show (∠ β.source β.circle.center β.target = -∠ β.target β.circle.center β.source) - apply neg_value_of_rev_ang - -theorem antipode_iff_collinear (A B : P) {ω : Circle P} [h : PtNe B A] (h₁ : A LiesOn ω) (h₂ : B LiesOn ω) : Arc.IsAntipode A B h₁ h₂ ↔ Collinear ω.center A B := by - haveI : PtNe A ω.center := Circle.pt_lieson_ne_center h₁ - haveI : PtNe B ω.center := Circle.pt_lieson_ne_center h₂ - constructor - · exact collinear_of_angle_eq_pi - intro hh - show ∠ A ω.center B = π - have hl : B LiesOn LIN ω.center A := Line.pt_pt_maximal hh - have heq₁ : VEC A ω.center = VEC ω.center B := by - apply vec_eq_dist_eq_of_lies_on_line_pt_pt_of_ptNe hl - rw [h₁, h₂] - have heq₂ : VEC A B = (2 : ℝ) • (VEC A ω.center) := by - calc - _ = VEC A ω.center + VEC ω.center B := by rw [vec_add_vec] - _ = (2 : ℝ) • (VEC A ω.center) := by rw [← heq₁, two_smul] - have hli : ω.center LiesInt SEG_nd A B := by - apply SegND.lies_int_iff.mpr - use 2⁻¹ - constructor - · norm_num - constructor - · norm_num - show VEC A ω.center = 2⁻¹ • (VEC A B) - rw [heq₂] - simp - exact value_eq_pi_of_lies_int_seg_nd hli - -theorem mk_pt_pt_diam_isantipode {A B : P} [h : PtNe A B] : Arc.IsAntipode A B (Circle.mk_pt_pt_diam_fst_lieson) (Circle.mk_pt_pt_diam_snd_lieson) := by - have hc : Collinear (SEG A B).midpoint A 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 _ _ (Circle.mk_pt_pt_diam_fst_lieson) (Circle.mk_pt_pt_diam_snd_lieson)).mpr hc - -end Arc - -end angle - - -theorem inscribed_angle_is_positive {p : P} {β : Arc P} (h : p LiesInt β.complement) : (Arc.angle_mk_pt_arc p β h.2.symm).value.IsPos := by - unfold Arc.angle_mk_pt_arc - apply TriangleND.liesonleft_angle_ispos - exact (Arc.liesint_complementary_arc_liesonleft_dlin h) - -theorem inscribed_angle_of_complementary_arc_is_negative {p : P} {β : Arc P} (h : p LiesInt β) : (Arc.angle_mk_pt_arc p β h.2).value.IsNeg := by - unfold Arc.angle_mk_pt_arc - apply TriangleND.liesonright_angle_isneg - exact (Arc.liesint_arc_liesonright_dlin h) - -theorem cangle_eq_two_times_inscribed_angle {p : P} {β : Arc P} (h₁ : p LiesOn β.circle) (h₂ : Arc.Isnot_arc_endpts p β) : β.cangle.value = 2 • (Arc.angle_mk_pt_arc p β h₂).value := by - haveI : PtNe p β.source := ⟨h₂.1⟩ - haveI : PtNe p β.target := ⟨h₂.2⟩ - haveI : PtNe p β.circle.center := Circle.pt_lieson_ne_center h₁ - have hit₁ : (▵ β.circle.center β.target p).IsIsoceles := by - unfold Triangle.IsIsoceles - show (SEG p β.circle.center).length = (SEG β.circle.center β.target).length - rw [Seg.length_eq_dist, Seg.length_eq_dist, dist_comm, h₁, β.ison.2] - have hit₂ : (▵ β.circle.center p β.source).IsIsoceles := by - unfold Triangle.IsIsoceles - show (SEG β.source β.circle.center).length = (SEG β.circle.center p).length - rw [Seg.length_eq_dist, Seg.length_eq_dist, dist_comm, h₁, β.ison.1] - have eq₁ : ∠ p β.target β.circle.center = ∠ β.circle.center p β.target := by apply is_isoceles_tri_ang_eq_ang_of_tri hit₁ - have eq₂ : ∠ β.source p β.circle.center = ∠ β.circle.center β.source p := by apply is_isoceles_tri_ang_eq_ang_of_tri hit₂ - have π₁ : ∠ β.target β.circle.center p + ∠ p β.target β.circle.center + ∠ β.circle.center p β.target = π := by apply angle_sum_eq_pi_of_tri (▵ β.circle.center β.target p) - have π₂ : ∠ p β.circle.center β.source + ∠ β.source p β.circle.center + ∠ β.circle.center β.source p = π := by apply angle_sum_eq_pi_of_tri (▵ β.circle.center p β.source) - have hsum₁ : ∠ β.target β.circle.center p + ∠ p β.circle.center β.source = ∠ β.target β.circle.center β.source := by - have : (ANG β.target β.circle.center p).end_ray = (ANG p β.circle.center β.source).start_ray := rfl - have hhs : (Angle.sum_adj this).value = ∠ β.target β.circle.center β.source := rfl - rw [← hhs, Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang] - have hsum₂ : ∠ β.source p β.circle.center + ∠ β.circle.center p β.target = ∠ β.source p β.target := by - have : (ANG β.source p β.circle.center).end_ray = (ANG β.circle.center p β.target).start_ray := rfl - have hhs : (Angle.sum_adj this).value = ∠ β.source p β.target := rfl - rw [← hhs, Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang] - have eq₃ : ∠ β.target β.circle.center β.source + 2 • (∠ β.source p β.target) = 0 := by - calc - _ = ∠ β.target β.circle.center p + ∠ p β.circle.center β.source + 2 • (∠ β.source p β.circle.center + ∠ β.circle.center p β.target) := by rw [hsum₁, hsum₂] - _ = ∠ β.target β.circle.center p + ∠ p β.circle.center β.source + (∠ p β.target β.circle.center + ∠ β.circle.center p β.target) + (∠ β.source p β.circle.center + ∠ β.circle.center β.source p) := by - rw [← eq₂, eq₁, two_smul] - abel - _ = (∠ β.target β.circle.center p + ∠ p β.target β.circle.center + ∠ β.circle.center p β.target) + (∠ p β.circle.center β.source + ∠ β.source p β.circle.center + ∠ β.circle.center β.source p) := by - rw [add_assoc, add_add_add_comm] - abel - _ = 0 := by - rw [π₁, π₂, ← coe_two_pi, two_mul] - simp - calc - _ = - ∠ β.target β.circle.center β.source := by rw [← neg_value_of_rev_ang]; rfl - _ = 2 • (∠ β.source p β.target) := by rw [← zero_sub, ← eq₃, add_sub_cancel'] - _ = 2 • (Arc.angle_mk_pt_arc p β h₂).value := rfl - -theorem inscribed_angle_of_diameter_eq_mod_pi {p : P} {β : Arc P} (h₁ : p LiesOn β.circle) (h₂ : Arc.IsAntipode β.source β.target β.ison.1 β.ison.2) (h₃ : Arc.Isnot_arc_endpts p β) : (Arc.angle_mk_pt_arc p β h₃).dvalue = ∡[π / 2] := by - have : β.cangle.value = π := h₂ - have : 2 • (Arc.angle_mk_pt_arc p β h₃).value = π := by - rw [← this, ← cangle_eq_two_times_inscribed_angle] - exact h₁ - rcases two_nsmul_eq_pi_iff.mp this with h | h - · unfold Angle.dvalue - rw [h] - unfold Angle.dvalue - rw [h, neg_div] - simp - -theorem inscribed_angle_of_diameter_eq_mod_pi_pt_pt_pt {A B C : P} {ω : Circle P} [hne₁ : PtNe A B] [hne₂ : PtNe B C] [hne₃ : PtNe C A] (h₁ : A LiesOn ω) (h₂ : B LiesOn ω) (h₃ : C LiesOn ω) (h : Arc.IsAntipode A B h₁ h₂) : ∠ A C B = ∡[π / 2] := by - let β : Arc P := ARC A B h₁ h₂ - have hh₁ : C LiesOn β.circle := h₃ - have hh₂ : Arc.IsAntipode β.source β.target β.ison.1 β.ison.2 := h - have hh₃ : Arc.Isnot_arc_endpts C β := ⟨hne₃.out, hne₂.out.symm⟩ - apply inscribed_angle_of_diameter_eq_mod_pi hh₁ hh₂ hh₃ - -theorem inscribed_angle_on_same_arc_is_invariant_mod_pi {A B : P} {β : Arc P} (h₁ : A LiesOn β.circle) (h₂ : B LiesOn β.circle) (hne₁ : Arc.Isnot_arc_endpts A β) (hne₂ : Arc.Isnot_arc_endpts B β) : (Arc.angle_mk_pt_arc A β hne₁).dvalue = (Arc.angle_mk_pt_arc B β hne₂).dvalue := by - have eq : 2 • (Arc.angle_mk_pt_arc A β hne₁).value = 2 • (Arc.angle_mk_pt_arc B β hne₂).value := by rw [← cangle_eq_two_times_inscribed_angle h₁ hne₁, ← cangle_eq_two_times_inscribed_angle h₂ hne₂] - exact coe_eq_coe_iff_two_nsmul_eq.mpr eq - - -namespace Arc - -protected def iangle (β : Arc P) : AngDValue := sorry - -theorem inscribed_angle_dvalue_eq_iangle {p : P} {β : Arc P} (h₁ : p LiesOn β.circle) (h₂ : Isnot_arc_endpts p β) : (Arc.angle_mk_pt_arc p β h₂).dvalue = β.iangle := by - sorry - -theorem angle_of_osculation : sorry := sorry - -end Arc - -end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean b/EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean new file mode 100644 index 00000000..3580d66e --- /dev/null +++ b/EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean @@ -0,0 +1,207 @@ +import EuclideanGeometry.Foundation.Axiom.Circle.Basic +import EuclideanGeometry.Foundation.Axiom.Position.Angle_ex +import EuclideanGeometry.Foundation.Axiom.Triangle.IsocelesTriangle_trash + +noncomputable section +namespace EuclidGeom + +variable {P : Type _} [EuclideanPlane P] + +open AngValue Angle + +section cangle + +attribute [instance] Arc.endpts_ne Chord.IsND Arc.source_ne_center Arc.target_ne_center Chord.source_ne_center Chord.target_ne_center + +def Arc.cangle {ω : Circle P} (β : Arc P ω) : Angle P := ANG β.source ω.center β.target + +def Arc.IsMajor {ω : Circle P} (β : Arc P ω) : Prop := β.cangle.value.toReal < 0 + +def Arc.IsMinor {ω : Circle P} (β : Arc P ω) : Prop := β.cangle.value.toReal > 0 + +def Chord.cangle {ω : Circle P} (s : Chord P ω) : Angle P := ANG s.1.source ω.center s.1.target + +theorem Circle.cangle_of_arc_eq_cangle_of_toChord {ω : Circle P} (β : Arc P ω) : β.cangle = β.toChord.cangle := rfl + +theorem Circle.cangle_of_chord_eq_cangle_of_toArc {ω : Circle P} (s : Chord P ω) : s.cangle = s.toArc.cangle := rfl + +theorem Chord.cangle_eq_pi_iff_is_diameter {ω : Circle P} (s : Chord P ω) : s.cangle.value = π ↔ Chord.IsDiameter s := by + constructor + · intro heq + have : Collinear ω.center s.1.source s.1.target := collinear_of_angle_eq_pi heq + apply diameter_iff_antipide.mpr + apply (Circle.antipode_iff_collinear s.1.source s.1.target _ _).mpr (Collinear.perm₂₁₃ this) + intro hd + have : ω.center LiesInt s.1 := by + constructor + · exact hd + exact (center_ne_endpts s).1 + exact (center_ne_endpts s).2 + apply value_eq_pi_of_lies_int_seg_nd this + +theorem Arc.complement_cangle_reverse {ω : Circle P} (β : Arc P ω) : β.complement.cangle = β.cangle.reverse := rfl + +theorem Chord.reverse_cangle_reverse {ω : Circle P} (s : Chord P ω) : s.reverse.cangle = s.cangle.reverse := rfl + +theorem Circle.cangle_of_complementary_arc_eq_neg {ω : Circle P} (β : Arc P ω) : β.complement.cangle.value = -β.cangle.value := by + rw [Arc.complement_cangle_reverse, rev_value_eq_neg_value] + +theorem Circle.cangle_of_reverse_chord_eq_neg {ω : Circle P} (s : Chord P ω) : s.reverse.cangle.value = -s.cangle.value := by + rw [Chord.reverse_cangle_reverse, rev_value_eq_neg_value] + +theorem Chord.cangle_eq_iff_length_eq {ω : Circle P} (s₁ s₂ : Chord P ω) : s₁.cangle.value = s₂.cangle.value ↔ s₁.length = s₂.length := sorry + +end cangle + + +section iangle + +attribute [instance] Arc.pt_ne_source Arc.pt_ne_target -- why can't work + +def Arc.IsIangle {ω : Circle P} (β : Arc P ω) (ang : Angle P) : Prop := (ang.source LiesOn ω) ∧ (β.ne_endpts ang.source) ∧ (β.source LiesOn ang.start_ray) ∧ (β.target LiesOn ang.end_ray) + +def Chord.IsIangle {ω : Circle P} (s : Chord P ω) (ang : Angle P) : Prop := (ang.source LiesOn ω) ∧ (s.ne_endpts ang.source) ∧ (s.1.source LiesOn ang.start_ray) ∧ (s.1.target LiesOn ang.end_ray) + +theorem Arc.iangle_eq {ω : Circle P} {β : Arc P ω} {ang : Angle P} (h : β.IsIangle ang) : ANG β.source ang.source β.target h.2.1.1.symm h.2.1.2.symm = ang := eq_of_lies_int_ray ⟨h.2.2.1, h.2.1.1.symm⟩ ⟨h.2.2.2, h.2.1.2.symm⟩ + +theorem Chord.iangle_eq {ω : Circle P} {s : Chord P ω} {ang : Angle P} (h : s.IsIangle ang) : ANG s.1.source ang.source s.1.target h.2.1.1.symm h.2.1.2.symm = ang := eq_of_lies_int_ray ⟨h.2.2.1, h.2.1.1.symm⟩ ⟨h.2.2.2, h.2.1.2.symm⟩ + +theorem Arc.angle_mk_pt_is_iangle {ω : Circle P} {C : P} {β : Arc P ω} (h₁ : C LiesOn ω) (h₂ : β.ne_endpts C) : β.IsIangle (ANG β.source C β.target h₂.1.symm h₂.2.symm) := by + haveI : PtNe C β.source := ⟨h₂.1⟩ + haveI : PtNe C β.target := ⟨h₂.2⟩ + constructor + · exact h₁ + constructor + · exact h₂ + constructor + · show β.source LiesOn (RAY C β.source) + apply Ray.snd_pt_lies_on_mk_pt_pt + show β.target LiesOn (RAY C β.target) + apply Ray.snd_pt_lies_on_mk_pt_pt + +theorem Chord.angle_mk_pt_is_iangle {ω : Circle P} {C : P} {s : Chord P ω} (h₁ : C LiesOn ω) (h₂ : s.ne_endpts C) : s.IsIangle (ANG s.1.source C s.1.target h₂.1.symm h₂.2.symm) := by + haveI : PtNe C s.1.source := ⟨h₂.1⟩ + haveI : PtNe C s.1.target := ⟨h₂.2⟩ + constructor + · exact h₁ + constructor + · exact h₂ + constructor + · show s.1.source LiesOn (RAY C s.1.source) + apply Ray.snd_pt_lies_on_mk_pt_pt + show s.1.target LiesOn (RAY C s.1.target) + apply Ray.snd_pt_lies_on_mk_pt_pt + +theorem Circle.iangle_of_arc_is_iangle_of_toChord {ω : Circle P} {β : Arc P ω} {ang : Angle P} (h : β.IsIangle ang) : β.toChord.IsIangle ang := h + +theorem Circle.iangle_of_chord_is_iangle_of_toArc {ω : Circle P} {s : Chord P ω} {ang : Angle P} (h : s.IsIangle ang) : s.toArc.IsIangle ang := h + +theorem Arc.cangle_eq_two_times_inscribed_angle {ω : Circle P} {β : Arc P ω} {ang : Angle P} (h : β.IsIangle ang) : β.cangle.value = 2 • ang.value := by + let p : P := ang.source + haveI : PtNe p β.source := ⟨h.2.1.1⟩ + haveI : PtNe p β.target := ⟨h.2.1.2⟩ + haveI : PtNe p ω.center := Circle.pt_lieson_ne_center h.1 + have hit₁ : (▵ ω.center β.target p).IsIsoceles := by + unfold Triangle.IsIsoceles + show (SEG p ω.center).length = (SEG ω.center β.target).length + rw [Seg.length_eq_dist, Seg.length_eq_dist, dist_comm, h.1, β.ison.2] + have hit₂ : (▵ ω.center p β.source).IsIsoceles := by + unfold Triangle.IsIsoceles + show (SEG β.source ω.center).length = (SEG ω.center p).length + rw [Seg.length_eq_dist, Seg.length_eq_dist, dist_comm, h.1, β.ison.1] + have eq₁ : ∠ p β.target ω.center = ∠ ω.center p β.target := by apply is_isoceles_tri_ang_eq_ang_of_tri hit₁ + have eq₂ : ∠ β.source p ω.center = ∠ ω.center β.source p := by apply is_isoceles_tri_ang_eq_ang_of_tri hit₂ + have π₁ : ∠ β.target ω.center p + ∠ p β.target ω.center + ∠ ω.center p β.target = π := by apply angle_sum_eq_pi_of_tri (▵ ω.center β.target p) + have π₂ : ∠ p ω.center β.source + ∠ β.source p ω.center + ∠ ω.center β.source p = π := by apply angle_sum_eq_pi_of_tri (▵ ω.center p β.source) + have hsum₁ : ∠ β.target ω.center p + ∠ p ω.center β.source = ∠ β.target ω.center β.source := by + have : (ANG β.target ω.center p).end_ray = (ANG p ω.center β.source).start_ray := rfl + have hhs : (sum_adj this).value = ∠ β.target ω.center β.source := rfl + rw [← hhs, ang_eq_ang_add_ang_mod_pi_of_adj_ang] + have hsum₂ : ∠ β.source p ω.center + ∠ ω.center p β.target = ∠ β.source p β.target := by + have : (ANG β.source p ω.center).end_ray = (ANG ω.center p β.target).start_ray := rfl + have hhs : (sum_adj this).value = ∠ β.source p β.target := rfl + rw [← hhs, ang_eq_ang_add_ang_mod_pi_of_adj_ang] + have eq₃ : ∠ β.target ω.center β.source + 2 • (∠ β.source p β.target) = 0 := by + calc + _ = ∠ β.target ω.center p + ∠ p ω.center β.source + 2 • (∠ β.source p ω.center + ∠ ω.center p β.target) := by rw [hsum₁, hsum₂] + _ = ∠ β.target ω.center p + ∠ p ω.center β.source + (∠ p β.target ω.center + ∠ ω.center p β.target) + (∠ β.source p ω.center + ∠ ω.center β.source p) := by + rw [← eq₂, eq₁, two_smul] + abel + _ = (∠ β.target ω.center p + ∠ p β.target ω.center + ∠ ω.center p β.target) + (∠ p ω.center β.source + ∠ β.source p ω.center + ∠ ω.center β.source p) := by + rw [add_assoc, add_add_add_comm] + abel + _ = 0 := by + rw [π₁, π₂, ← coe_two_pi, two_mul] + simp + calc + _ = - ∠ β.target ω.center β.source := by rw [← neg_value_of_rev_ang]; rfl + _ = 2 • (∠ β.source p β.target) := by rw [← zero_sub, ← eq₃, add_sub_cancel'] + _ = 2 • ang.value := by rw [← Arc.iangle_eq h] + +theorem Chord.cangle_eq_two_times_inscribed_angle {ω : Circle P} {s : Chord P ω} {ang : Angle P} (h : s.IsIangle ang) : s.cangle.value = 2 • ang.value := by + have : s.toArc.IsIangle ang := h + rw [← Arc.cangle_eq_two_times_inscribed_angle this] + rfl + +theorem Circle.iangle_of_diameter_eq_mod_pi {ω : Circle P} {s : Chord P ω} {ang : Angle P} (h : s.IsIangle ang) (hd : s.IsDiameter) : ang.dvalue = ∡[π / 2] := by + have : s.cangle.value = π := (Chord.cangle_eq_pi_iff_is_diameter s).mpr hd + have : 2 • ang.value = π := by rw [← this, Chord.cangle_eq_two_times_inscribed_angle h] + rcases two_nsmul_eq_pi_iff.mp this with h | h + · rw [← h] + unfold dvalue + rw [h, neg_div] + simp + +theorem Arc.iangle_invariant_mod_pi {ω : Circle P} {β : Arc P ω} {ang₁ ang₂ : Angle P} (h₁ : β.IsIangle ang₁) (h₂ : β.IsIangle ang₂) : ang₁.dvalue = ang₂.dvalue := by + have : 2 • ang₁.value = 2 • ang₂.value := by + rw [← cangle_eq_two_times_inscribed_angle h₁, ← cangle_eq_two_times_inscribed_angle h₂] + apply coe_eq_coe_iff_two_nsmul_eq.mpr this + +theorem Chord.iangle_invariant_mod_pi {ω : Circle P} {s : Chord P ω} {ang₁ ang₂ : Angle P} (h₁ : s.IsIangle ang₁) (h₂ : s.IsIangle ang₂) : ang₁.dvalue = ang₂.dvalue := by + have : 2 • ang₁.value = 2 • ang₂.value := by + rw [← cangle_eq_two_times_inscribed_angle h₁, ← cangle_eq_two_times_inscribed_angle h₂] + apply coe_eq_coe_iff_two_nsmul_eq.mpr this + +end iangle + + +section iangdvalue + +def Arc.iangdv {ω : Circle P} (β : Arc P ω) : AngDValue := β.cangle.value.half + +def Chord.iangdv {ω : Circle P} (s : Chord P ω) : AngDValue := s.cangle.value.half + +theorem Arc.iangle_dvalue_eq {ω : Circle P} {β : Arc P ω} {ang : Angle P} (h : β.IsIangle ang) : ang.dvalue = β.iangdv := by + unfold iangdv + rw [cangle_eq_two_times_inscribed_angle h] + apply AngValue.coe_eq_coe_iff_two_nsmul_eq.mpr + simp + +theorem Chord.iangle_dvalue_eq {ω : Circle P} {s : Chord P ω} {ang : Angle P} (h : s.IsIangle ang) : ang.dvalue = s.iangdv := by + unfold iangdv + rw [cangle_eq_two_times_inscribed_angle h] + apply AngValue.coe_eq_coe_iff_two_nsmul_eq.mpr + simp + +theorem Circle.same_chord_same_iangle_dvalue {ω : Circle P} {s₁ s₂ : Chord P ω} {ang₁ ang₂ : Angle P} (h₁ : s₁.IsIangle ang₁) (h₂ : s₂.IsIangle ang₂) (h : s₁.length = s₂.length) : ang₁.dvalue = ang₂.dvalue := by + have : s₁.cangle.value = s₂.cangle.value := (Chord.cangle_eq_iff_length_eq s₁ s₂).mpr h + rw [Chord.iangle_dvalue_eq h₁, Chord.iangle_dvalue_eq h₂] + unfold Chord.iangdv + rw [this] + +end iangdvalue + + +/- +theorem inscribed_angle_is_positive {p : P} {β : Arc P ω} (h : p LiesInt β.complement) : (angle_mk_pt_arc ω p β h.2.symm).value.IsPos := by + unfold angle_mk_pt_arc + apply TriangleND.liesonleft_angle_ispos + exact (Arc.pt_liesint_complementary_liesonleft_dlin ω h) + +theorem inscribed_angle_of_complementary_arc_is_negative {p : P} {β : Arc P ω} (h : p LiesInt β) : (angle_mk_pt_arc ω p β h.2).value.IsNeg := by + unfold angle_mk_pt_arc + apply TriangleND.liesonright_angle_isneg + exact (Arc.pt_liesint_liesonright_dlin ω h) +-/ + +end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean index 4520d488..9309acaf 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean @@ -1,5 +1,4 @@ import EuclideanGeometry.Foundation.Axiom.Circle.Basic -import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular_trash noncomputable section namespace EuclidGeom @@ -53,6 +52,17 @@ theorem intersect_iff_tangent_or_secant {l : DirLine P} {ω : Circle P} : (DirLi have : dist_pt_line ω.center l.toLine < ω.radius := h linarith +theorem pt_liesint_secant {l : DirLine P} {ω : Circle P} {A : P} (h₁ : A LiesInt ω) (h₂ : A LiesOn l) : l Secant ω := by + have : dist ω.center A < ω.radius := h₁ + have : dist_pt_line ω.center l ≤ dist ω.center A := dist_pt_line_shortest ω.center A h₂ + show dist_pt_line ω.center l < ω.radius + linarith + +theorem pt_liesint_intersect {l : DirLine P} {ω : Circle P} {A : P} (h₁ : A LiesInt ω) (h₂ : A LiesOn l) : DirLine.IsIntersected l ω := by + apply intersect_iff_tangent_or_secant.mpr + right + apply pt_liesint_secant h₁ h₂ + end DirLC @[ext] @@ -181,6 +191,8 @@ lemma inx_pts_ne_center {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersect · apply (pt_lieson_ne_center (inx_pts_lieson_circle h).1).out apply (pt_lieson_ne_center (inx_pts_lieson_circle h).2).out +theorem inx_pts_antipode_iff_center_lieson {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersected l ω) : IsAntipode ω (inx_pts_lieson_circle h).1 (inx_pts_lieson_circle h).2 ↔ ω.center LiesOn l := sorry + theorem inxwith_iff_intersect {l : DirLine P} {ω : Circle P} : l InxWith ω ↔ DirLine.IsIntersected l ω := by unfold intersect constructor @@ -287,6 +299,14 @@ theorem pt_pt_tangent_eq_tangent_pt {A B : P} {ω : Circle P} (h₁ : A LiesOut rw [(inx_pts_same_iff_tangent _).mpr ht] at heq exact heq +theorem chord_toDirLine_intersected {ω : Circle P} (s : Chord P ω) : DirLine.IsIntersected s.1.toDirLine ω := by + show dist_pt_line ω.center s.1.toDirLine ≤ ω.radius + rw [← s.2.1] + apply dist_pt_line_shortest ω.center s.1.source DirLine.fst_pt_lies_on_mk_pt_pt + +theorem chord_toDirLine_inx_front_pt_eq_target {ω : Circle P} (s : Chord P ω) : (Inxpts (chord_toDirLine_intersected s)).front = s.1.target := sorry + +theorem chord_toDirLine_inx_back_pt_eq_source {ω : Circle P} (s : Chord P ω) : (Inxpts (chord_toDirLine_intersected s)).back = s.1.source := sorry /- Equivalent condition for tangency -/ theorem pt_pt_tangent_perp {A B : P} {ω : Circle P} (h₁ : A LiesOut ω) (h₂ : B LiesOn ω) (ht : (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) Tangent ω) : (DLIN ω.center B (pt_lieson_ne_center h₂).out) ⟂ (DLIN A B (pt_liesout_ne_pt_lieson h₁ h₂).out.symm) := by diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean index 3bf264d7..946d6c37 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean @@ -5,4 +5,14 @@ namespace EuclidGeom variable {P : Type _} [EuclideanPlane P] +theorem pt_flip_collinear {A B O : P} (h : B = pt_flip A O) : Collinear A O B := by + apply Collinear.perm₁₃₂ + by_cases hne : A = B + · rw [hne] + unfold Collinear + simp + haveI : PtNe A B := ⟨hne⟩ + apply Line.pt_pt_linear + sorry + end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean index 0613a3f8..0998cf36 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean @@ -1,4 +1,5 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Ray +import EuclideanGeometry.Foundation.Axiom.Basic.Plane_trash noncomputable section @@ -16,4 +17,10 @@ variable {P : Type _} [EuclideanPlane P] (seg_nd : SegND P) by the way in_seg shoud be renamed by current naming system -/ +theorem pt_flip_center_is_midpoint {A B O : P} (h : B = pt_flip A O) : O = (SEG A B).midpoint := by + unfold Seg.midpoint + apply (eq_vadd_iff_vsub_eq _ _ _).mpr + show VEC A O = (1 / 2 : ℝ) • (VEC A B) + exact pt_flip_vec_eq_half_vec h + end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Index.lean b/EuclideanGeometry/Foundation/Index.lean index 8504fd51..f0965524 100644 --- a/EuclideanGeometry/Foundation/Index.lean +++ b/EuclideanGeometry/Foundation/Index.lean @@ -32,7 +32,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.IsocelesTriangle import EuclideanGeometry.Foundation.Axiom.Circle.Basic import EuclideanGeometry.Foundation.Axiom.Circle.CCPosition import EuclideanGeometry.Foundation.Axiom.Circle.LCPosition -import EuclideanGeometry.Foundation.Axiom.Circle.IncribedAngle +import EuclideanGeometry.Foundation.Axiom.Circle.InscribedAngle import EuclideanGeometry.Foundation.Axiom.Circle.CirclePower /- Tactic -/ diff --git a/Plan_files/DetailedPlan/Axiom-Circle.pdf b/Plan_files/DetailedPlan/Axiom-Circle.pdf index 93e35402..e49aeca7 100644 Binary files a/Plan_files/DetailedPlan/Axiom-Circle.pdf and b/Plan_files/DetailedPlan/Axiom-Circle.pdf differ diff --git a/Plan_files/DetailedPlan/Axiom-Circle.tex b/Plan_files/DetailedPlan/Axiom-Circle.tex index 01ba0f19..caf20c95 100644 --- a/Plan_files/DetailedPlan/Axiom-Circle.tex +++ b/Plan_files/DetailedPlan/Axiom-Circle.tex @@ -1,44 +1,355 @@ -\documentclass[12pt,a4paper]{article} -\usepackage{graphicx} % Required for inserting images +\documentclass[12pt]{amsart} +\usepackage{graphicx} \usepackage{amssymb} \usepackage{amsmath} +\usepackage{verbatim} +\usepackage{fullpage} +\usepackage{color} -\title{LEAN Project Circle} -\author{} -\date{} +\newcommand{\toadd}{{\color{red}To Add: }} +\newcommand{\changename}{{\color{red}To Change Name: }} +\title{Document file for content in subfolder: Axiom--Circle} \begin{document} \maketitle -\section{Content in file CCPosition.lean} -In this file, we define the relative positions between circles. - Definitions: - (defn) separated_of_circle_circle : Prop -- Given two circles (\omega_1 \omega_2 : Circle P), return a proposition that the distance between two circle centers is larger than the sum of two radii, i.e., |O_1O_2|>r_1+r_2. - (defn) intersected_of_circle_circle : Prop -- Given two circles (\omega_1 \omega_2 : Circle P), return a proposition that the distance between two circle centers is less than the sum of two radii and more than the difference of their radii, i.e., |r_1-r_2|<|O_1O_2| 0$; it is the circle whose center and radius are given. +\end{itemize} + +\subsection{Make of concepts} +\begin{itemize} + \item Definition \verb|Circle.mk_pt_pt|: Given two distinct points $O$ and $A$, this function returns a circle whose center is $O$ and radius is $\|OA\|$. + \item Definition \verb|Circle.mk_pt_pt_pt|: Given three points $A,B,C$ that are not collinear, this function returns a circle which is the circumcircle of triangle $ABC$. {\color{red} This \verb|def| will be moved into the construction of circumcenter.} + \item Definition \verb|CIR| as \verb|Circle.mk_pt_pt|: This is to abbreviate the function \verb|Circle.mk_pt_pt| into \verb|CIR|. + \item Definition $\odot$ as \verb|Circle.mk_pt_pt|: This is to abbreviate the function \verb|Circle.mk_pt_pt| into $\odot$. + \item Definition \verb|Circle.mk_pt_radius|: Given a point $O$ and a positive real number $r$, this function returns a circle whose center is $O$ and radius is $r$. + \item Definition \verb|Circle.mk_pt_pt_diam|: Given two distinct points $A$ and $B$, this function returns a circle with $AB$ as its diameter, i.e. the circle's center is the midpoint of $AB$, and its radius is $\frac{1}{2}\|AB\|$. +\end{itemize} + +\subsection{Position between a point and a circle} +\begin{itemize} + \item Definition \verb|Circle.IsInside|: Given a point $A$ and a circle $\omega$, this function returns whether $A$ lies inside $\omega$; here saying that $A$ lies inside $\omega$ means that the distance between $A$ and the center of $\omega$ is not greater than the radius of $\omega$. + \item Definition \verb|Circle.IsOn|: Given a point $A$ and a circle $\omega$, this function returns whether $A$ lies on $\omega$; here saying that $A$ lies on $\omega$ means that the distance between $A$ and the center of $\omega$ is equal to the radius of $\omega$. + \item Definition \verb|Circle.IsInt|: Given a point $A$ and a circle $\omega$, this function returns whether $A$ lies in the interior of $\omega$; here saying that $A$ lies in the interior of $\omega$ means that the distance between $A$ and the center of $\omega$ is smaller than the radius of $\omega$. + \item Definition \verb|Circle.IsOutside|: Given a point $A$ and a circle $\omega$, this function returns whether $A$ lies outside $\omega$; here saying that $A$ lies outside $\omega$ means that the distance between $A$ and the center of $\omega$ is greater than the radius of $\omega$. + \item Definition \verb|Circle.carrier|: Given a circle, its underlying set is the set of points that lie on this circle. + \item Definition \verb|Circle.interior|: Given a circle, its interior is the set of points that lie in the interior of this circle. + \item Definition \verb|LiesIn| as \verb|Circle.IsInside|: This is to abbreviate the function \verb|Circle.IsInside| into \verb|LiesIn|. + \item Definition \verb|LiesOut| as \verb|Circle.IsOutside|: This is to abbreviate the function \verb|Circle.IsOutside| into \verb|LiesOut|. + \item Instance \verb|Circle.pt_liesout_ne_center|: Given a circle $\omega$ and a point $A$ that lies outside $\omega$, then $A$ is distinct to the center of $\omega$. + \item Instance \verb|Circle.pt_lieson_ne_center|: Given a circle $\omega$ and a point $A$ that lies on $\omega$, then $A$ is distinct to the center of $\omega$. + \item Instance \verb|Circle.pt_liesout_ne_pt_lieson|: Given a circle $\omega$, a point $A$ that lies outside $\omega$ and a point $B$ that lies on $\omega$, then $A$ and $B$ are distinct, i.e. $A \ne B$. + \item Instance \verb|Circle.pt_liesint_ne_pt_lieson|: Given a circle $\omega$, a point $A$ that lies in the interior of $\omega$ and a point $B$ that lies on $\omega$, then $A$ and $B$ are distinct, i.e. $A \ne B$. + \item Instance \verb|Circle.pt_liesout_ne_pt_liesint|: Given a circle $\omega$, a point $A$ that lies outside $\omega$ and a point $B$ that lies in the interior of $\omega$, then $A$ and $B$ are distinct, i.e. $A \ne B$. + \item Theorem \verb|Circle.liesint_iff_liesin_and_not_lieson|: Given a circle $\omega$ and a point $A$, then $A$ lies in the interior of $\omega$ if and only if $A$ lies inside $\omega$ and $A$ doesn't lie on $\omega$. + \item Theorem \verb|Circle.liesin_iff_liesint_or_lieson|: Given a circle $\omega$ and a point $A$, then $A$ lies inside $\omega$ if and only if $A$ lies in the interior of $\omega$ or $A$ lies on $\omega$. + \item Theorem \verb|Circle.mk_pt_pt_lieson|: Given two distinct points $O$ and $A$, then $A$ lies on \verb|CIR O A|, i.e. the center of the circle is $O$ and the radius is $\|OA\|$. + \item Theorem \verb|Circle.mk_pt_pt_diam_fst_lieson|: Given two distinct points $A$ and $B$, then the first point $A$ lies on the circle with $AB$ as its diameter. + \item Theorem \verb|Circle.mk_pt_pt_diam_snd_lieson|: Given two distinct points $A$ and $B$, then the second point $B$ lies on the circle with $AB$ as its diameter. + \item Definition \verb|Circle.seg_lies_inside_circle|: Given a segment $l$ and a circle $\omega$, this function returns whether $l$ lies inside $\omega$; here saying that $l$ lies inside $\omega$ means that the two endpoints of $l$ both lie inside $\omega$. + \item Definition \verb|SegInCir| as \verb|Circle.seg_lies_inside_circle|: This is to abbreviate the function \verb|Circle.seg_lies_inside_circle| into \verb|SegInCir|. + \item Theorem \verb|Circle.pt_lies_inside_circle_of_seg_inside_circle|: Given a circle $\omega$, a segment $l$ that lies in the interior of $\omega$ and a point $A$ that lies in the interior of $l$, then $A$ lies in the interior of $\omega$. {\color{red} still \verb|sorry|, need a lemma of \emph{Seg}} +\end{itemize} + +\subsection{Position between different points} +\begin{itemize} + \item Lemma \verb|Circle.pts_lieson_circle_vec_eq|: Given a circle $\omega$ and two distinct points $A,B$ that both lie on $\omega$, if we denote the perpendicular foot of the center of $\omega$ to the line $AB$ as $P$, then $\overrightarrow{AP} = \overrightarrow{PB}$. + \item Theorem \verb|Circle.pts_lieson_circle_perpfoot_eq_midpoint|: Given a circle $\omega$ and two distinct points $A,B$ that both lie on $\omega$, then the perpendicular foot of the center of $\omega$ to the line $AB$ is equal to the midpoint of $AB$. + \item Theorem \verb|Circle.three_pts_lieson_circle_not_collinear|: Given a circle $\omega$ and three points $A,B,C$ that is distinct to each other, and they all lie on $\omega$, then $A,B,C$ are not collinear. +\end{itemize} + +\subsection{Antipode} +\begin{itemize} + \item Definition \verb|Circle.IsAntipode|: Given a circle $\omega$ and two points $A,B$ that both lie on $\omega$, this function returns whether $B$ is $A$'s antipode; here saying that $B$ is $A$'s antipode means that $B$ is the point reflection of $A$ respect to the center of $\omega$. + \item Theorem \verb|Circle.antipode_symm|: Given a circle $\omega$ and two points $A,B$ that both lie on $\omega$, if $B$ is $A$'s antipode, then $A$ is $B$'s antipode. + \item Theorem \verb|Circle.antipode_center_is_midpoint|: Given a circle $\omega$ and two points $A,B$ that both lie on $\omega$, if $B$ is $A$'s antipode, then the center of $\omega$ is the midpoint of segment $AB$. + \item Theorem \verb|Circle.antipode_iff_collinear|: Given a circle $\omega$ and two distinct points $A,B$ that both lie on $\omega$, then $B$ is $A$'s antipode if and only if $A,O,B$ are collinear, where $O$ is the center of $\omega$. + \item Theorem \verb|Circle.mk_pt_pt_diam_is_antipode|: Given two distinct points $A,B$, then $B$ is $A$'s antipode respect to the circle with segment $AB$ as its diameter. +\end{itemize} + +\subsection{Arc} +\begin{itemize} + \item Structure \verb|Arc|: Given a circle $\omega$, an \emph{Arc} consists of two points named \verb|source| and \verb|target|, and properties that these two points both lies on the circle and they are distinct; it is an arc from \verb|source| to \verb|target| respect to $\omega$. + \item Definition \verb|Arc.mk_pt_pt_circle|: Given a circle $\omega$ and two distinct points $A,B$ that lie on $\omega$, this function returns the arc from $A$ to $B$ respect to $\omega$. + \item Definition \verb|ARC| as \verb|Arc.mk_pt_pt_circle|: This is to abbreviate the function \verb|Arc.mk_pt_pt_circle| into \verb|ARC|. + \item Definition \verb|Arc.IsOn|: Given a circle $\omega$, a point $A$ and an arc $\beta$ on $\omega$, this function returns whether $A$ lies on $\beta$; here saying that $A$ lies on $\beta$ means that $A$ lies on $\omega$ and $A$ doesn't lie on the left side of the directed line from $\beta$'s source to target. + \item Definition \verb|Arc.ne_endpts|: Given a circle $\omega$, a point $A$ and an arc $\beta$ on $\omega$, this function returns whether $A$ is not equal to $\beta$'s endpoints; here saying that $A$ is not equal to $\beta$'s endpoints means that $A$ is not equal to $\beta$'s source or target. + \item Instance \verb|Arc.pt_ne_source|: Given a circle $\omega$, an arc $\beta$ on $\omega$ and a point $A$ that is not equal to $\beta$'s endpoints, then $A$ is not equal to $\beta$'s source. + \item Instance \verb|Arc.pt_ne_target|: Given a circle $\omega$, an arc $\beta$ on $\omega$ and a point $A$ that is not equal to $\beta$'s endpoints, then $A$ is not equal to $\beta$'s target. + \item Definition \verb|Arc.IsInt|: Given a circle $\omega$, a point $A$ and an arc $\beta$ on $\omega$, this function returns whether $A$ lies in the interior of $\beta$; here saying that $A$ lies in the interior of $\beta$ means that $A$ lies on $\beta$ and $A$ is not $\beta$'s endpoints. + \item Definition \verb|Arc.carrier|: Given an arc, its underlying set is the set of points that lie on this arc. + \item Definition \verb|Arc.interior|: Given an arc, its interior is the set of points that lie in the interior of this arc. + \item Theorem \verb|Arc.center_ne_endpts|: Given a circle $\omega$ and an arc $\beta$ on $\omega$, then $\omega$'s center is not equal to $\beta$'s endpoints. + \item Instance \verb|Arc.source_ne_center|: Given a circle $\omega$ and an arc $\beta$ on $\omega$, then $\beta$'s source is not equal to $\omega$'s center. + \item Instance \verb|Arc.target_ne_center|: Given a circle $\omega$ and an arc $\beta$ on $\omega$, then $\beta$'s target is not equal to $\omega$'s center. + \item Definition \verb|Arc.complement|: Given a circle $\omega$ and an arc $\beta$ on $\omega$, this function returns the complement of $\beta$; here saying that the complement of $\beta$ starts from $\beta$'s target and ends at $\beta$'s source. + \item Lemma \verb|Arc.pt_liesint_not_lieson_dlin|: Given a circle $\omega$, an arc $\beta$ on $\omega$ and a point $A$ that lies in the interior of $\beta$, then $A$ doesn't lie on the directed line from $\beta$'s source to target. + \item Theorem \verb|Arc.pt_liesint_liesonright_dlin|: Given a circle $\omega$, an arc $\beta$ on $\omega$ and a point $A$ that lies in the interior of $\beta$, then $A$ lies on the right side of the directed line from $\beta$'s source to target. + \item Theorem \verb|Arc.pt_liesint_complementary_liesonleft_dlin|: Given a circle $\omega$, an arc $\beta$ on $\omega$ and a point $A$ that lies in the interior of $\beta$'s complement, then $A$ lies on the left side of the directed line from $\beta$'s source to target. + {\color{red} \item Is it necessary to define the sum of arcs which are connected?} +\end{itemize} + +\subsection{Chord} +\begin{itemize} + \item Structure \verb|Chord|: Given a circle $\omega$, a Chord consists of a non-degenerate segment $AB$ and condition that both $A$ and $B$ lie on $\omega$. + \item Instance \verb|Chord.IsND|: Given a circle $\omega$ and a chord $s$ in $\omega$, then the source and target of $s$ are distinct. + \item Definition \verb|Chord.mk_pt_pt_circle|: Given a circle $\omega$ and two distinct points $A,B$ that both lie on $\omega$, this function returns the chord $AB$ in $\omega$. + \item Definition \verb|Chord.IsOn|: Given a circle $\omega$, a point $A$ and a chord $s$ in $\omega$, this function returns whether $A$ lies on $s$; here saying that $A$ lies on $s$ means that $A$ lies on the non-degenerate segment respect to $s$. + \item Definition \verb|Chord.IsInt|: Given a circle $\omega$, a point $A$ and a chord $s$ in $\omega$, this function returns whether $A$ lies in the interior of $s$; here saying that $A$ lies in the interior of $s$ means that $A$ lies in the interior of the non-degenerate segment respect to $s$. + \item Definition \verb|Chord.carrier|: Given a chord, its underlying set is the set of points that lie on this chord. + \item Definition \verb|Chord.interior|: Given a chord, its interior is the set of points that lie in the interior of this chord. + \item Definition \verb|Chord.ne_endpts|: Given a circle $\omega$, a point $A$ and a chord $s$ in $\omega$, this function returns whether $A$ is not equal to the endpoints of $s$; here saying that $A$ is not equal to $s$'s endpoints means that $A$ is not equal to the source or target of $s$. + \item Theorem \verb|Chord.center_ne_endpts|: Given a circle $\omega$ and a chord $s$ in $\omega$, then $\omega$'s center is not equal to the endpoints of $s$. + \item Instance \verb|Chord.source_ne_center|: Given a circle $\omega$ and a chord $s$ in $\omega$, then the source of $s$ is not equal to $\omega$'s center. + \item Instance \verb|Chord.target_ne_center|: Given a circle $\omega$ and a chord $s$ in $\omega$, then the target of $s$ is not equal to $\omega$'s center. + \item Definition \verb|Chord.reverse|: Given a circle $\omega$ and a chord $s$ in $\omega$, then this function returns the reverse chord of $s$, which starts from the target of $s$ and ends at the source of $s$. + \item Theorem \verb|Chord.pt_liesint_liesint_circle|: Given a circle $\omega$, a chord $s$ in $\omega$ and a point A that lies in the interior of $s$, then A lies in the interior of $\omega$. + \item Definition \verb|Arc.toChord|: Given a circle $\omega$ and an arc $\beta$ on $\omega$, this function returns the chord respect to $\beta$. + \item Definition \verb|Chord.toArc|: Given a circle $\omega$ and a chord $s$ in $\omega$, this function returns the arc respect to $s$. + \item Theorem \verb|Circle.complementary_arc_toChord_eq_reverse|: Given a circle $\omega$ and an arc $\beta$ on $\omega$, then the chord respect to the complement of $\beta$ is equal to the reverse chord respect to $\beta$. + \item Theorem \verb|Circle.reverse_chord_toArc_eq_complement|: Given a circle $\omega$ and a chord $s$ in $\omega$, then the arc respect to the reverse chord of $s$ is equal to the complement arc respect to $s$. + \item Definition \verb|Chord.length|: Given a circle $\omega$ and a chord $s$ in $\omega$, this function returns the length of $s$. + \item Definition \verb|Chord.IsDiameter|: Given a circle $\omega$ and a chord $s$ in $\omega$, this function returns whether $s$ is a diameter; here saying that $s$ is a diameter means that the center of $\omega$ lies on $s$. + \item Theorem \verb|Chord.diameter_iff_antipide|: Given a circle $\omega$ and a chord $s$ in $\omega$, then $s$ is a diameter if and only if the source and target of $s$ are antipodes. + \item Theorem \verb|Chord.diameter_length_eq_twice_radius|: Given a circle $\omega$ and a chord $s$ in $\omega$, if $s$ is a diameter, then the length of $s$ is twice as large as $\omega$'s radius, i.e. $|s|=2r$. +\end{itemize} \section{Content in file LCPosition.lean} -In this file, we define the relative position between lines and circles and rays and circles. What's more, when discuss position bewteen rays and circles, we want give a criterion whether the underlying lines have common points with the circles and give constructions to the TWO intersections (may be the same point). - \subsection{position of lines and circles} - Definitions : - (defn) line_tangent_to_circle : Prop -- Given a line and a circle, return a proposition that the line has exactly one common point with the circle, i.e., there exist a common point A and any common point must be A. - (defn) line_secant_to_circle : Prop -- Given a line and a circle, return a proposition that they have exactly two common points. - (defn) line_disjoint_from_circle : Prop -- Given a line and a circle, returen a proposition that they have no common points. - (defn) line_intersect_circle : Prop -- Given a line and a circle, returen a proposition that the line has at least a common point with the circle. - Theorems : - line_tangent_to_circle_iff_one_intersection -- Given a line and a circle, the line is tangent to the circle iff the distance from the center to the line is equal to radius of the circle. - line_secant_to_circle_iff_two_intersection -- Given a line and a circle, the line is secant to the circle iff the distance from the center to the line is less than the radius of the circle. - line_disjoint_from_circle_iff_two_intersection -- Given a line and a circle, the line is disjoint from the circle iff the distance from the center to the line is more than the radius of the circle. - -\end{document} \ No newline at end of file +In this file, we define the position between a line and a circle, and there intersected points if intersected. + +\subsection{Position between a directed line and a circle} +\begin{itemize} + \item Definition \verb|Circle.DirLine.IsDisjoint|: Given a directed line $l$ and a circle $\omega$, this function returns whether $l$ is disjoint to $\omega$; here saying that $l$ is disjoint to $\omega$ means that the distance from the circle of $\omega$ to $l$ is greater than the radius of $\omega$. + \item Definition \verb|Circle.DirLine.IsTangent|: Given a directed line $l$ and a circle $\omega$, this function returns whether $l$ is tangent to $\omega$; here saying that $l$ is tangent to $\omega$ means that the distance from the circle of $\omega$ to $l$ is equal to the radius of $\omega$. + \item Definition \verb|Circle.DirLine.IsSecant|: Given a directed line $l$ and a circle $\omega$, this function returns whether $l$ is secant to $\omega$; here saying that $l$ is secant to $\omega$ means that the distance from the circle of $\omega$ to $l$ is smaller than the radius of $\omega$. + \item Definition \verb|Circle.DirLine.IsIntersected|: Given a directed line $l$ and a circle $\omega$, this function returns whether $l$ is intersected with $\omega$; here saying that $l$ is intersected with $\omega$ means that the distance from the circle of $\omega$ to $l$ is not greater than the radius of $\omega$. + \item Definition \verb|Secant| as \verb|Circle.DirLine.IsSecant|: This is to abbreviate the function \verb|Circle.DirLine.IsSecant| into \verb|Secant|. + \item Definition \verb|Tangent| as \verb|Circle.DirLine.IsTangent|: This is to abbreviate the function \verb|Circle.DirLine.IsTangent| into \verb|Tangent|. + \item Definition \verb|Disjoint| as \verb|Circle.DirLine.IsDisjoint|: This is to abbreviate the function \verb|Circle.DirLine.IsDisjoint| into \verb|Disjoint|. + \item Theorem \verb|DirLC.disjoint_pt_liesout_circle|: Given a circle $\omega$, a directed line $l$ which is disjoint to $\omega$, and a point $A$ that lies on $l$, then $A$ lies outside $\omega$. + \item Theorem \verb|DirLC.intersect_iff_tangent_or_secant|: Given a directed line $l$ and a circle $\omega$, then $l$ is intersected with $\omega$ if and only if $l$ is tangent to $\omega$ or $l$ is secant to $\omega$. + \item Theorem \verb|DirLC.pt_liesint_secant|: Given a circle $\omega$, a point $A$ in the interior of $\omega$ and a directed line $l$ such that $A$ lies on $l$, then $l$ is secant to $\omega$. + \item Theorem \verb|DirLC.pt_liesint_intersect|: Given a circle $\omega$, a point $A$ in the interior of $\omega$ and a directed line $l$ such that $A$ lies on $l$, then $l$ is intersected with $\omega$. +\end{itemize} + +\subsection{Definition of intersected points} +\begin{itemize} + \item Structure \verb|DirLCInxpts|: A \emph{DirLCInxpts} consists of two points named \verb|front| and \verb|back|; they are the intersected points of a directed line and a circle, distinguished by the direction of the directed line. + \item Lemma \verb|DirLC.dist_pt_line_ineq|: Given a circle $\omega$ and a directed line $l$ that is intersected with $\omega$, then we have an inequality $r^2-d^2\ge0$, where $r$ is the radius of $\omega$ and $d$ is the distance from the center of $\omega$ to $l$. {\color{blue} This lemma makes sure that the definition of intersected points is well defined.} + \item Definition \verb|DirLC.Inxpts|: Given a circle $\omega$ and a directed line $l$ that is intersected with $\omega$, this function returns the intersected points of $l$ and $\omega$. +\end{itemize} + +\subsection{Basic properties of intersected points} +\begin{itemize} + \item Lemma \verb|DirLC.inx_pts_lieson_dlin|: Given a circle $\omega$ and a directed line $l$ that is intersected with $\omega$, then both of the intersected points of $l$ and $\omega$ lie on $l$. + \item Theorem \verb|DirLC.inx_pts_lieson_circle|: Given a circle $\omega$ and a directed line $l$ that is intersected with $\omega$, then both of the intersected points of $l$ and $\omega$ lie on $\omega$. + \item Theorem \verb|DirLC.inx_pts_same_iff_tangent|: Given a circle $\omega$ and a directed line $l$ that is intersected with $\omega$, then two intersected points of $l$ and $\omega$ coincide if and only if $l$ is tangent to $\omega$. + \item Lemma \verb|DirLC.inx_pts_ne_center|: Given a circle $\omega$ and a directed line $l$ that is intersected with $\omega$, then both of the intersected points of $l$ and $\omega$ are distinct with the center of $\omega$. + \item Theorem \verb|DirLC.inx_pts_antipode_iff_center_lieson|: Given a circle $\omega$ and a directed line $l$ that is intersected with $\omega$, then one of the intersected points of $l$ and $\omega$ is the antipode of another if and only if the center of $\omega$ lies on $l$. {\color{red} still \verb|sorry|} + \item Theorem \verb|DirLC.inxwith_iff_intersect|: Given a circle $\omega$ and a directed line $l$, then the images of $l$ and $\omega$ have intersection if and only if $l$ is intersected with $\omega$. + \item Theorem \verb|DirLC.inxwith_iff_tangent_or_secant|: Given a circle $\omega$ and a directed line $l$, then the images of $l$ and $\omega$ have intersection if and only if $l$ is tangent to $\omega$ or $l$ is secant to $\omega$. + {\color{red} Do we need to change the statement of \verb|IsIntersected| to \verb|InxWith| in the above theorems?} +\end{itemize} + +\subsection{Tangent point} +\begin{itemize} + \item Definition \verb|DirLC.Tangentpt|: Given a circle $\omega$ and a directed line $l$ that is tangent to $\omega$, this function returns the tangent point of $l$ and $\omega$. + \item Lemma \verb|DirLC.tangent_pt_ne_center|: Given a circle $\omega$ and a directed line $l$ that is tangent to $\omega$, then the tangent point of $l$ and $\omega$ is distinct with the center of $\omega$. + \item Theorem \verb|DirLC.tangent_pt_center_perp_line|: Given a circle $\omega$ and a directed line $l$ that is tangent to $\omega$, then the line between the center of $\omega$ and the tangent point is perpendicular to $l$. + \item Theorem \verb|DirLC.tangent_pt_eq_perp_foot|: Given a circle $\omega$ and a directed line $l$ that is tangent to $\omega$, then the tangent point is the perpendicular foot from the center of $\omega$ to $l$. +\end{itemize} + +\subsection{The uniqueness of intersected points} +\begin{itemize} + \item Theorem \verb|Circle.DirLC_intersection_eq_inxpts|: Given a circle $\omega$, a directed line $l$ that is intersected with $\omega$ and a point $A$ that both lie on $l$ and $\omega$, then $A$ is equal to one of the intersected points of $l$ and $\omega$. + \item Theorem \verb|Circle.pt_pt_tangent_eq_tangent_pt|: Given a circle $\omega$ and two points $A,B$ that $A$ lies outside $\omega$ and $B$ lies on $\omega$, if directed line $AB$ is tangent to $\omega$, then $B$ is the tangent point. + \item Theorem \verb|Circle.chord_toDirLine_intersected|: Given a circle $\omega$ and a chord $s$ in $\omega$, then the directed line respect to $s$, which starts from the source of $s$ and ends at the target of $s$, is intersected with $\omega$. + \item Theorem \verb|Circle.chord_toDirLine_inx_front_pt_eq_target|: Given a circle $\omega$ and a chord $s$ in $\omega$, then the front intersected point of the directed line respect to $s$ and $\omega$ is equal to the target of $s$. {\color{red} still \verb|sorry|} + \item Theorem \verb|Circle.chord_toDirLine_inx_back_pt_eq_source|: Given a circle $\omega$ and a chord $s$ in $\omega$, then the back intersected point of the directed line respect to $s$ and $\omega$ is equal to the source of $s$. {\color{red} still \verb|sorry|} +\end{itemize} + +\subsection{Equivalent condition for tangency} +\begin{itemize} + \item Theorem \verb|Circle.pt_pt_tangent_perp|: Given a circle $\omega$ and two points $A,B$ that $A$ lies outside $\omega$ and $B$ lies on $\omega$, if directed line $AB$ is tangent to $\omega$, then the directed line from the center of $\omega$ to $B$ is perpendicular to directed line $AB$. + \item Theorem \verb|Circle.pt_pt_perp_tangent|: Given a circle $\omega$ and two points $A,B$ that $A$ lies outside $\omega$ and $B$ lies on $\omega$, if directed line $AB$ is perpendicular to the directed line from the center of $\omega$ to $B$, then directed line $AB$ is tangent to $\omega$. + \item Theorem \verb|Circle.pt_pt_perp_eq_tangent_pt|: Given a circle $\omega$ and two points $A,B$ that $A$ lies outside $\omega$ and $B$ lies on $\omega$, if directed line $AB$ is perpendicular to the directed line from the center of $\omega$ to $B$, then $B$ is the tangent point of directed line $AB$ and $\omega$. +\end{itemize} + +\subsection{Position between a line and a circle} +\begin{itemize} + \item Definition \verb|Circle.Line.IsDisjoint|: Given a line $l$ and a circle $\omega$, this function returns whether $l$ is disjoint to $\omega$; here saying that $l$ is disjoint to $\omega$ means that the distance from the circle of $\omega$ to $l$ is greater than the radius of $\omega$. + \item Definition \verb|Circle.Line.IsTangent|: Given a line $l$ and a circle $\omega$, this function returns whether $l$ is tangent to $\omega$; here saying that $l$ is tangent to $\omega$ means that the distance from the circle of $\omega$ to $l$ is equal to the radius of $\omega$. + \item Definition \verb|Circle.Line.IsSecant|: Given a line $l$ and a circle $\omega$, this function returns whether $l$ is secant to $\omega$; here saying that $l$ is secant to $\omega$ means that the distance from the circle of $\omega$ to $l$ is smaller than the radius of $\omega$. + \item Definition \verb|Circle.Line.IsIntersected|: Given a line $l$ and a circle $\omega$, this function returns whether $l$ is intersected with $\omega$; here saying that $l$ is intersected with $\omega$ means that the distance from the circle of $\omega$ to $l$ is not greater than the radius of $\omega$. +\end{itemize} + + +\section{Content in file CCPosition.lean} +In this file, we define the position between two circles, and there intersected points if intersected. + +\subsection{Position between two circles} +\begin{itemize} + \item Definition \verb|Circle.CC.IsSeparated|: Given two circles $\omega_1,\omega_2$, this function returns whether $\omega_1$ is separated from $\omega_2$; here saying that $\omega_1$ is separated from $\omega_2$ means that the distance between their centers is greater than the sum of their radius, i.e. $d > r_1 + r_2$. + \item Definition \verb|Circle.CC.IsIntersected|: Given two circles $\omega_1,\omega_2$, this function returns whether $\omega_1$ is intersected with $\omega_2$; here saying that $\omega_1$ is intersected with $\omega_2$ means that the distance between their centers is smaller than the sum of their radius and greater than the absolute value of the difference between their radius, i.e, $|r_1-r_2|