diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean index ad9ef2c1..63fafdb3 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean @@ -742,7 +742,8 @@ def cu (u v w: Vec) : ℝ := (det u v)⁻¹ * (w.1 * v.2 - v.1 * w.2) def cv (u v w: Vec) : ℝ := (det u v)⁻¹ * (u.1 * w.2 - w.1 * u.2) -theorem det_eq_zero_iff_eq_smul (u v : Vec) (hu : u ≠ 0) : u.1 * v.2 - u.2 * v.1 = 0 ↔ (∃ (t : ℝ), v = t • u) := by +theorem det_eq_zero_iff_eq_smul (u v : Vec) (hu : u ≠ 0) : det u v = 0 ↔ (∃ (t : ℝ), v = t • u) := by + unfold det have h : (u.1 ≠ 0) ∨ (u.2 ≠ 0) := by by_contra _ have h₁ : u.1 = 0 := by tauto @@ -781,34 +782,52 @@ theorem det_eq_zero_iff_eq_smul (u v : Vec) (hu : u ≠ 0) : u.1 * v.2 - u.2 * v rcases e ring -theorem linear_combination_of_not_colinear' {u v w : Vec} (hu : u ≠ 0) (h' : ¬(∃ (t : ℝ), v = t • u)) : ∃ (cu cv : ℝ), w = cu • u + cv • v := by +theorem det'_ne_zero_of_not_colinear {u v : Vec} (hu : u ≠ 0) (h' : ¬(∃ (t : ℝ), v = t • u)) : det' u v ≠ 0 := by + unfold det' have h₁ : (¬ (∃ (t : ℝ), v = t • u)) → (¬ (u.1 * v.2 - u.2 * v.1 = 0)) := by intro _ by_contra h₂ let _ := (det_eq_zero_iff_eq_smul u v hu).1 h₂ tauto - let d := u.1 * v.2 - u.2 * v.1 - have h₃ : d ≠ 0 := h₁ h' - use d⁻¹ * (w.1 * v.2 - v.1 * w.2) - use d⁻¹ * (u.1 * w.2 - w.1 * u.2) symm - rw [mul_smul, mul_smul, ← smul_add] - apply ((inv_smul_eq_iff₀ h₃).2) - unfold HSMul.hSMul instHSMul SMul.smul MulAction.toSMul Complex.mulAction Complex.instSMulRealComplex - simp only [smul_eq_mul, zero_mul, sub_zero] + field_simp + have trivial : ((u.re : ℂ) * v.im - u.im * v.re) = ((Sub.sub (α := ℝ) (Mul.mul (α := ℝ) u.re v.im) (Mul.mul (α := ℝ) u.im v.re)) : ℂ) := by + symm + calc + ((Sub.sub (α := ℝ) (Mul.mul (α := ℝ) u.re v.im) (Mul.mul (α := ℝ) u.im v.re)) : ℂ) = ((Mul.mul u.re v.im) - (Mul.mul u.im v.re)) := Complex.ofReal_sub _ _ + _ = ((Mul.mul u.re v.im) - (u.im * v.re)) := by + rw [← Complex.ofReal_mul u.im v.re] + rfl + _ = ((u.re * v.im) - (u.im * v.re)) := by + rw [← Complex.ofReal_mul u.re _] + rfl + rw [trivial, ← ne_eq] + symm + rw [ne_eq, Complex.ofReal_eq_zero] + exact h₁ h' + +theorem linear_combination_of_not_colinear' {u v w : Vec} (hu : u ≠ 0) (h' : ¬(∃ (t : ℝ), v = t • u)) : w = (cu u v w) • u + (cv u v w) • v := by + unfold cu cv det + have : ((u.re : ℂ) * v.im - u.im * v.re) ≠ 0 := det'_ne_zero_of_not_colinear hu h' + field_simp apply Complex.ext - simp only [add_zero, Complex.add_re] + simp ring - simp only [add_zero, Complex.add_im] + simp ring -theorem linear_combination_of_not_colinear {u v : Vec_nd} (w : Vec) (h' : Vec_nd.toProj u ≠ Vec_nd.toProj v) : ∃ (cᵤ cᵥ : ℝ), w = cᵤ • u.1 + cᵥ • v.1 := by +theorem linear_combination_of_not_colinear_vec_nd {u v : Vec_nd} (w : Vec) (h' : Vec_nd.toProj u ≠ Vec_nd.toProj v) : w = (cu u.1 v.1 w) • u.1 + (cv u.1 v.1 w) • v.1 := by have h₁ : (Vec_nd.toProj u ≠ Vec_nd.toProj v) → ¬(∃ (t : ℝ), v.1 = t • u.1) := by intro _ by_contra h₂ let _ := (Vec_nd.eq_toProj_iff u v).2 h₂ tauto - exact linear_combination_of_not_colinear' u.2 (h₁ h') + exact @linear_combination_of_not_colinear' u.1 v.1 w u.2 (h₁ h') + +theorem linear_combination_of_not_colinear_dir {u v : Dir} (w : Vec) (h' : u.toProj ≠ v.toProj) : w = (cu u.1 v.1 w) • u.1 + (cv u.1 v.1 w) • v.1 := by + have h₁ : (u.toProj ≠ v.toProj) → ¬(∃ (t : ℝ), v.1 = t • u.1) := by + sorry + exact @linear_combination_of_not_colinear' u.1 v.1 w u.toVec_nd.2 (h₁ h') end Linear_Algebra diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line'.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line'.lean deleted file mode 100644 index d67ba396..00000000 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line'.lean +++ /dev/null @@ -1,149 +0,0 @@ -import EuclideanGeometry.Foundation.Axiom.Linear.Colinear -import EuclideanGeometry.Foundation.Axiom.Linear.Ray -import EuclideanGeometry.Foundation.Axiom.Linear.Ray_ex - -noncomputable section -namespace EuclidGeom - -section setoid - -variable {P : Type _} [EuclideanPlane P] - -def same_extn_line : Ray P → Ray P → Prop := fun r₁ r₂ => r₁.toProj = r₂.toProj ∧ (r₂.source LiesOn r₁ ∨ r₂.source LiesOn r₁.reverse) - -namespace same_extn_line - -theorem dir_eq_or_eq_neg {x y : Ray P} (h : same_extn_line x y) : (x.toDir = y.toDir ∨ x.toDir = - y.toDir) := (Dir.eq_toProj_iff _ _).mp h.1 - -protected theorem refl (x : Ray P) : same_extn_line x x := ⟨rfl, Or.inl (Ray.source_lies_on x)⟩ - -protected theorem symm {x y : Ray P} (h : same_extn_line x y) : same_extn_line y x := by - constructor - · exact h.1.symm - · have g := dir_eq_or_eq_neg h - cases g with - | inl h₁ => sorry - | inr h₂ => sorry - -protected theorem trans {x y z : Ray P} (h₁ : same_extn_line x y) (h₂ : same_extn_line y z) : same_extn_line x z := sorry - -protected def setoid : Setoid (Ray P) where - r := same_extn_line - iseqv := { - refl := same_extn_line.refl - symm := same_extn_line.symm - trans := same_extn_line.trans - } - -instance : Setoid (Ray P) := same_extn_line.setoid - -end same_extn_line - -theorem same_extn_line_of_PM (A : P) (x y : Dir) (h : PM x y) : same_extn_line (Ray.mk A x) (Ray.mk A y) := sorry - -theorem same_extn_line.eq_carrier_union_rev_carrier (ray ray' : Ray P) (h : same_extn_line ray ray') : ray.carrier ∪ ray.reverse.carrier = ray'.carrier ∪ ray'.reverse.carrier := sorry - -end setoid - -def Line (P : Type _) [EuclideanPlane P] := Quotient (@same_extn_line.setoid P _) - -variable {P : Type _} [EuclideanPlane P] - -section make - -namespace Line - --- define a line from two points -def mk_pt_pt (A B : P) (h : B ≠ A) : Line P := ⟦RAY A B h⟧ - --- define a line from a point and a proj -def mk_pt_proj (A : P) (proj : Proj) : Line P := Quotient.map (sa := PM.con.toSetoid) (fun x : Dir => Ray.mk A x) (same_extn_line_of_PM A) proj - --- define a line from a point and a direction -def mk_pt_dir (A : P) (dir : Dir) : Line P := mk_pt_proj A dir.toProj - --- define a line from a point and a nondegenerate vector -def mk_pt_vec_nd (A : P) (vec_nd : Vec_nd) : Line P := mk_pt_proj A vec_nd.toProj - -end Line - -scoped notation "LIN" => Line.mk_pt_pt - -end make - -section coercion - -def Line.toProj (l : Line P) : Proj := Quotient.lift (fun ray : Ray P => ray.toProj) (fun _ _ h => And.left h) l - -def Ray.toLine (ray : Ray P) : Line P := ⟦ray⟧ - -def Seg_nd.toLine (seg_nd : Seg_nd P) : Line P := ⟦seg_nd.toRay⟧ - -instance : Coe (Ray P) (Line P) where - coe := Ray.toLine - -section carrier - -namespace Line - -protected def carrier (l : Line P) : Set P := Quotient.lift (fun ray : Ray P => ray.carrier ∪ ray.reverse.carrier) (same_extn_line.eq_carrier_union_rev_carrier) l - -/- Def of point lies on a line, LiesInt is not defined -/ -protected def IsOn (a : P) (l : Line P) : Prop := - a ∈ l.carrier - -instance : Carrier P (Line P) where - carrier := fun l => l.carrier - -theorem linear (l : Line P) {A B C : P} (h₁ : A LiesOn l) (h₂ : B LiesOn l) (h₃ : C LiesOn l) : colinear A B C := by - unfold Line at l - revert l - rw [forall_quotient_iff (p := fun k : Line P => A LiesOn k → B LiesOn k → C LiesOn k → colinear A B C)] - unfold lies_on instCarrierLine Carrier.carrier Line.carrier at * - simp only - intro ray a b c - rw [@Quotient.lift_mk _ _ same_extn_line.setoid _ _ _] at * - cases a with - | inl a => - cases b with - | inl b => - cases c with - | inl c => - exact Ray.colinear_of_lies_on a b c - | inr c => - let ray' := Ray.mk C ray.toDir - have a' : A ∈ ray'.carrier := lies_on_pt_toDir_of_pt_lies_on_rev a c - have b' : B ∈ ray'.carrier := lies_on_pt_toDir_of_pt_lies_on_rev b c - exact Ray.colinear_of_lies_on a' b' (Ray.source_lies_on ray') - | inr b => - cases c with - | inl c => sorry - | inr c => sorry - | inr a => - cases b with - | inl b => - cases c with - | inl c => sorry - | inr c => sorry - | inr b => - cases c with - | inl c => sorry - | inr c => sorry - -theorem maximal (l : Line P) {A B : P} (h₁ : A ∈ l.carrier) (h₂ : B ∈ l.carrier) (h : B ≠ A) : (∀ (C : P), colinear A B C → (C ∈ l.carrier)) := sorry - -theorem nontriv (l : Line P) : ∃ (A B : P), (A ∈ l.carrier) ∧ (B ∈ l.carrier) ∧ (B ≠ A) := sorry - -end Line - --- A point lies on a line associated to a ray if and only if it lies on the ray or the reverse of the ray - -theorem Ray.lies_on_toLine_iff_lies_on_or_lies_on_rev (A : P) (ray : Ray P) : (A LiesOn ray.toLine) ↔ (A LiesOn ray) ∨ (A LiesOn ray.reverse) := sorry - -theorem Ray.lies_on_toLine_iff_lies_int_or_lies_int_rev_or_eq_source (A : P) (ray : Ray P) : (A LiesOn ray.toLine) ↔ (A LiesInt ray) ∨ (A LiesInt ray.reverse) ∨ (A = ray.source) := sorry - -end carrier - -end coercion - -end EuclidGeom \ No newline at end of file diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean index 9a39feb3..d67ba396 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean @@ -1,342 +1,149 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Colinear +import EuclideanGeometry.Foundation.Axiom.Linear.Ray +import EuclideanGeometry.Foundation.Axiom.Linear.Ray_ex noncomputable section namespace EuclidGeom -@[ext] -class Line (P : Type _) [EuclideanPlane P] where - carrier : Set P - linear : ∀ (A B C : P), (A ∈ carrier) → (B ∈ carrier) → (C ∈ carrier) → colinear A B C - maximal : ∀ (A B : P), (A ∈ carrier) → (B ∈ carrier) → (B ≠ A) → (∀ (C : P), colinear A B C → (C ∈ carrier)) - nontriv : ∃ (A B : P), (A ∈ carrier) ∧ (B ∈ carrier) ∧ (B ≠ A) - -namespace Line - -variable {P : Type _} [EuclideanPlane P] - --- define a line from two points - -def mk_pt_pt (A B : P) (h : B ≠ A) : Line P where - carrier := {C : P | ∃ t : ℝ, VEC A C = t • VEC A B} - linear x y z:= by - unfold Membership.mem Set.instMembershipSet Set.Mem setOf - simp only [forall_exists_index] - intro tx hx ty hy tz hz - by_cases ty ≠ tx ∧ tz ≠ tx ∧ ty ≠ tz - · rcases h with ⟨h₁, _, _⟩ - have w₂ : ∃ t : ℝ, VEC x z = t • VEC x y := by - use (ty - tx)⁻¹ * (tz - tx) - rw [mul_smul] - symm - apply ((inv_smul_eq_iff₀ (Iff.mpr sub_ne_zero h₁)).2) - rw [← vec_sub_vec A x y, ← vec_sub_vec A x z, hx, hy, hz] - rw [← sub_smul, ← sub_smul, ← mul_smul, ← mul_smul, mul_comm] - apply colinear_of_vec_eq_smul_vec' - exact w₂ - · have h' : (ty = tx) ∨ (tz = tx) ∨ (ty = tz) := by tauto - by_cases ty = tx - · rw [pt_eq_pt_of_eq_smul_smul h hy hx] - exact triv_colinear _ _ - · by_cases tz = tx - · rw [pt_eq_pt_of_eq_smul_smul h hz hx] - exact flip_colinear_snd_trd $ triv_colinear _ _ - · have h : ty = tz := by tauto - rw [pt_eq_pt_of_eq_smul_smul h hy hz] - exact flip_colinear_fst_snd $ flip_colinear_snd_trd $ triv_colinear _ _ - maximal x y := by - unfold Membership.mem Set.instMembershipSet Set.Mem setOf - simp only [forall_exists_index] - intro tx hx ty hy hne z c - have e : VEC x y = (ty - tx) • VEC A B := by - rw [← vec_sub_vec A x y, hx, hy, sub_smul] - rcases (eq_mul_vec_iff_colinear_of_ne hne).1 c with ⟨t, ht⟩ - use tx + t * (ty - tx) - rw [← vec_add_vec A x z, ht, e, hx, ← mul_smul, ← add_smul] - nontriv := by - use A - use B - unfold Membership.mem Set.instMembershipSet Set.Mem setOf - simp only [forall_exists_index] - constructor - use 0 - simp only [vec_same_eq_zero, zero_smul] - constructor - use 1 - simp only [one_smul] - exact h - -end Line - -scoped notation "LIN" => Line.mk_pt_pt - -namespace Line +section setoid variable {P : Type _} [EuclideanPlane P] -/- Def of point lies on a line, LiesInt is not defined -/ -protected def IsOn (a : P) (l : Line P) : Prop := - a ∈ l.carrier +def same_extn_line : Ray P → Ray P → Prop := fun r₁ r₂ => r₁.toProj = r₂.toProj ∧ (r₂.source LiesOn r₁ ∨ r₂.source LiesOn r₁.reverse) -instance : Carrier P (Line P) where - carrier := fun l => l.carrier +namespace same_extn_line -end Line - --- Now we introduce useful theorems to avoid using more unfolds in further proofs. -variable {P : Type _} [EuclideanPlane P] +theorem dir_eq_or_eq_neg {x y : Ray P} (h : same_extn_line x y) : (x.toDir = y.toDir ∨ x.toDir = - y.toDir) := (Dir.eq_toProj_iff _ _).mp h.1 -section Compaitiblity_of_coersions_of_mk_pt_pt +protected theorem refl (x : Ray P) : same_extn_line x x := ⟨rfl, Or.inl (Ray.source_lies_on x)⟩ --- The first point and the second point in Line.mk_pt_pt LiesOn the line it make. - -theorem fst_pt_lies_on_line_of_pt_pt {A B : P} (h : B ≠ A) : A LiesOn LIN A B h := by - unfold lies_on Carrier.carrier Line.instCarrierLine - simp only [Set.setOf_mem_eq] - unfold Line.carrier Line.mk_pt_pt - simp only [Set.mem_setOf_eq, vec_same_eq_zero] - use 0 - simp only [zero_smul] - -theorem snd_pt_lies_on_line_of_pt_pt {A B : P} (h : B ≠ A) : B LiesOn LIN A B h := by - unfold lies_on Carrier.carrier Line.instCarrierLine - simp only [Set.setOf_mem_eq] - unfold Line.carrier Line.mk_pt_pt - simp only [Set.mem_setOf_eq, vec_same_eq_zero] - use 1 - simp only [one_smul] - -theorem pt_lies_on_line_of_pt_pt_of_ne {A B : P} (h: B ≠ A) : A LiesOn LIN A B h ∧ B LiesOn LIN A B h := by - constructor - exact fst_pt_lies_on_line_of_pt_pt h - exact snd_pt_lies_on_line_of_pt_pt h - -theorem lies_on_line_of_pt_pt_iff_colinear {A B : P} (h : B ≠ A) : ∀ X : P, (X LiesOn (LIN A B h)) ↔ colinear A B X := by - intro X - constructor - intro hx - apply (LIN A B h).linear - exact fst_pt_lies_on_line_of_pt_pt h - exact snd_pt_lies_on_line_of_pt_pt h - exact hx - intro c - apply (LIN A B h).maximal A B - exact fst_pt_lies_on_line_of_pt_pt h - exact snd_pt_lies_on_line_of_pt_pt h - exact h - exact c - -end Compaitiblity_of_coersions_of_mk_pt_pt - -section Define_line_toProj - -/- examine a line has uniquely defined toProj -/ - -theorem vec_eq_smul_vec_of_lies_on {l : Line P} {A B X Y : P} (ha : A LiesOn l) (hb : B LiesOn l) (hx : X LiesOn l) (hy : Y LiesOn l) (hab : B ≠ A) : ∃ t : ℝ, VEC X Y = t • VEC A B := by - rcases (eq_mul_vec_iff_colinear_of_ne hab).1 (Line.linear A B X ha hb hx) with ⟨t₁, e₁⟩ - rcases (eq_mul_vec_iff_colinear_of_ne hab).1 (Line.linear A B Y ha hb hy) with ⟨t₂, e₂⟩ - use t₂ - t₁ - rw [← vec_sub_vec A, e₁, e₂, sub_smul] - -theorem toProj_eq_toProj_of_Seg_nd_lies_on {l : Line P} {A B X Y : P} (ha : A LiesOn l) (hb : B LiesOn l) (hx : X LiesOn l) (hy : Y LiesOn l) (hab : B ≠ A) (hxy : Y ≠ X) : Seg_nd.toProj ⟨SEG A B, hab⟩ = Seg_nd.toProj ⟨SEG X Y, hxy⟩ := by - rcases (vec_eq_smul_vec_of_lies_on ha hb hx hy hab) with ⟨t, e⟩ - exact eq_toProj_of_smul _ _ e - -/- define Line.toProj -/ - -theorem uniqueness_of_proj_of_line (l : Line P) : ∀ A B C D : P, (A LiesOn l) → (B LiesOn l) → (C LiesOn l) → (D LiesOn l) → (hab : B ≠ A) → (hcd : D ≠ C) → Seg_nd.toProj ⟨SEG A B, hab⟩ = Seg_nd.toProj ⟨SEG C D, hcd⟩ := by - intro A B C D ha hb hc hd hab hcd - exact toProj_eq_toProj_of_Seg_nd_lies_on ha hb hc hd hab hcd - -theorem exist_unique_proj_of_line (l : Line P) : ∃! pr : Proj, ∀ (A B : P) (ha : A LiesOn l) (hb : B LiesOn l) (h : B ≠ A), Seg_nd.toProj ⟨SEG A B, h⟩ = pr := by - rcases l.nontriv with ⟨x, ⟨y, c⟩⟩ - use Seg_nd.toProj ⟨SEG x y, c.2.2⟩ - simp +protected theorem symm {x y : Ray P} (h : same_extn_line x y) : same_extn_line y x := by constructor - intro A B ha hb hab - exact toProj_eq_toProj_of_Seg_nd_lies_on ha hb c.1 c.2.1 hab c.2.2 - intro pr w - rw [← w] - exact c.1 - exact c.2.1 + · exact h.1.symm + · have g := dir_eq_or_eq_neg h + cases g with + | inl h₁ => sorry + | inr h₂ => sorry -def Line.toProj (l : Line P) : Proj := - Classical.choose (exist_unique_proj_of_line l) - -- by choose pr _ using (exist_unique_proj_of_line l) - -- exact pr +protected theorem trans {x y z : Ray P} (h₁ : same_extn_line x y) (h₂ : same_extn_line y z) : same_extn_line x z := sorry --- If you don't want to use Classical.choose, please use this theorem to simplify your Line.toProj. +protected def setoid : Setoid (Ray P) where + r := same_extn_line + iseqv := { + refl := same_extn_line.refl + symm := same_extn_line.symm + trans := same_extn_line.trans + } -theorem line_toProj_eq_seg_nd_toProj_of_lies_on {A B : P} {l : Line P} (ha : A LiesOn l) (hb : B LiesOn l) (hab : B ≠ A) : Seg_nd.toProj ⟨SEG A B, hab⟩ = l.toProj := (Classical.choose_spec (exist_unique_proj_of_line l)).1 A B ha hb hab +instance : Setoid (Ray P) := same_extn_line.setoid -theorem line_of_pt_pt_toProj_eq_seg_nd_toProj {A B : P} (h : B ≠ A) : (LIN A B h).toProj = Seg_nd.toProj ⟨SEG A B, h⟩ := by - symm - apply line_toProj_eq_seg_nd_toProj_of_lies_on - exact fst_pt_lies_on_line_of_pt_pt h - exact snd_pt_lies_on_line_of_pt_pt h +end same_extn_line -end Define_line_toProj +theorem same_extn_line_of_PM (A : P) (x y : Dir) (h : PM x y) : same_extn_line (Ray.mk A x) (Ray.mk A y) := sorry -section Compatibility_of_LiesOn +theorem same_extn_line.eq_carrier_union_rev_carrier (ray ray' : Ray P) (h : same_extn_line ray ray') : ray.carrier ∪ ray.reverse.carrier = ray'.carrier ∪ ray'.reverse.carrier := sorry --- This is also a typical proof that shows how to use the four conditions in the def of a line. Please write it shorter in future. +end setoid -theorem lies_on_iff_colinear_of_ne_lies_on_lies_on {A B : P} {l : Line P} (h : B ≠ A) (ha : A LiesOn l) (hb : B LiesOn l) : ∀ C : P, (C LiesOn l) ↔ colinear A B C := by - intro C - constructor - intro hc - apply l.linear - exact ha - exact hb - exact hc - intro c - apply l.maximal A B - exact ha - exact hb - exact h - exact c - -/- Two lines are equal iff they have the same carrier -/ - -theorem lies_on_iff_lies_on_iff_line_eq_line (l₁ l₂ : Line P) : (∀ A : P, A LiesOn l₁ ↔ A LiesOn l₂) ↔ l₁ = l₂ := by - constructor - intro hiff - exact Line.ext l₁ l₂ (Set.ext hiff) - intro e - rw [e] - simp only [forall_const] - -/- tautological theorems of Line.mk_pt_pt -/ - -theorem eq_line_of_pt_pt_of_ne {A B : P} {l : Line P} (h : B ≠ A) (ha : A LiesOn l) (hb : B LiesOn l) : LIN A B h = l := by - apply (lies_on_iff_lies_on_iff_line_eq_line (LIN A B h) l).1 - intro X - constructor - intro hx - apply (lies_on_iff_colinear_of_ne_lies_on_lies_on h ha hb X).2 - exact (lies_on_line_of_pt_pt_iff_colinear h X).1 hx - intro hx - exact (lies_on_line_of_pt_pt_iff_colinear h X).2 ((lies_on_iff_colinear_of_ne_lies_on_lies_on h ha hb X).1 hx) - -theorem eq_of_pt_pt_lies_on_of_ne {A B : P} (h : B ≠ A) {l₁ l₂ : Line P}(hA₁ : A LiesOn l₁) (hB₁ : B LiesOn l₁) (hA₂ : A LiesOn l₂) (hB₂ : B LiesOn l₂) : l₁ = l₂ := sorry - -theorem colinear_iff_exist_line_lies_on (A B C : P) : colinear A B C ↔ ∃ l : Line P, (A LiesOn l) ∧ (B LiesOn l) ∧ (C LiesOn l) := by - sorry +def Line (P : Type _) [EuclideanPlane P] := Quotient (@same_extn_line.setoid P _) -end Compatibility_of_LiesOn -/- def coe from ray to line-/ - -def Ray.toLine (r : Ray P) := LIN r.source (r.toDir.toVec +ᵥ r.source) (by - simp only [ne_eq, vadd_eq_self_iff_vec_eq_zero] - exact Dir.toVec_ne_zero r.toDir) +variable {P : Type _} [EuclideanPlane P] -instance : Coe (Ray P) (Line P) where - coe := Ray.toLine +section make -theorem ray_toLine_toProj_eq_ray_toProj (r : Ray P) : r.toLine.toProj = r.toProj := by - sorry +namespace Line -/- def coe from non trivial segment to line-/ +-- define a line from two points +def mk_pt_pt (A B : P) (h : B ≠ A) : Line P := ⟦RAY A B h⟧ -def Seg_nd.toLine (seg_nd : Seg_nd P) := (LIN seg_nd.1.source seg_nd.1.target seg_nd.2) +-- define a line from a point and a proj +def mk_pt_proj (A : P) (proj : Proj) : Line P := Quotient.map (sa := PM.con.toSetoid) (fun x : Dir => Ray.mk A x) (same_extn_line_of_PM A) proj -def Line.mk_pt_vec_nd (A : P) (vec_nd : Vec_nd) := (LIN A (vec_nd.1 +ᵥ A) (by - sorry)) +-- define a line from a point and a direction +def mk_pt_dir (A : P) (dir : Dir) : Line P := mk_pt_proj A dir.toProj -section Compaitiblity_of_coersions +-- define a line from a point and a nondegenerate vector +def mk_pt_vec_nd (A : P) (vec_nd : Vec_nd) : Line P := mk_pt_proj A vec_nd.toProj --- If a point lies on a ray, then it lies on the line associated to the ray. -theorem Ray.lies_on_toLine_of_lie_on {A : P} {r : Ray P} (h : A LiesOn r) : A LiesOn (r.toLine) := sorry +end Line -theorem Seg_nd.lies_on_toLine_of_lie_on {A : P} {s : Seg_nd P} (h : A LiesOn s.1) : A LiesOn (s.toLine) := sorry +scoped notation "LIN" => Line.mk_pt_pt --- If A and B are two distinct points, they lie on the line AB -theorem Ray.source_lies_on_toLine (l : Ray P) : l.source LiesOn l.toLine := sorry +end make -theorem Seg_nd.source_lies_on_toLine (s : Seg_nd P) : s.1.source LiesOn s.toLine := sorry +section coercion -theorem Seg_nd.target_lies_on_toLine (s : Seg_nd P) : s.1.target LiesOn s.toLine := sorry +def Line.toProj (l : Line P) : Proj := Quotient.lift (fun ray : Ray P => ray.toProj) (fun _ _ h => And.left h) l --- The line defined from a nontrivial segment is equal to the line defined from the ray associated this nontrivial segment +def Ray.toLine (ray : Ray P) : Line P := ⟦ray⟧ -theorem Seg_nd.toLine_eq_toRay_toLine (seg_nd : Seg_nd P) : seg_nd.toLine = (seg_nd.toRay).toLine := sorry +def Seg_nd.toLine (seg_nd : Seg_nd P) : Line P := ⟦seg_nd.toRay⟧ -theorem line_of_pt_pt_eq_ray_toLine {A B : P} (h : B ≠ A) : LIN A B h = Ray.toLine (RAY A B h) := sorry +instance : Coe (Ray P) (Line P) where + coe := Ray.toLine -theorem line_of_pt_pt_eq_seg_nd_toLine {A B : P} (h : B ≠ A) : LIN A B h = Seg_nd.toLine ⟨SEG A B, h⟩ := rfl +section carrier -end Compaitiblity_of_coersions +namespace Line -section Archimedean_property +protected def carrier (l : Line P) : Set P := Quotient.lift (fun ray : Ray P => ray.carrier ∪ ray.reverse.carrier) (same_extn_line.eq_carrier_union_rev_carrier) l --- there are two distinct points on a line +/- Def of point lies on a line, LiesInt is not defined -/ +protected def IsOn (a : P) (l : Line P) : Prop := + a ∈ l.carrier -theorem exists_ne_pt_pt_lies_on_of_line (A : P) (l : Line P) : ∃ B : P, B LiesOn l ∧ B ≠ A := by - rcases l.nontriv with ⟨X, ⟨Y, _⟩⟩ - by_cases A = X - · use Y - rw [h] - tauto - · use X - tauto +instance : Carrier P (Line P) where + carrier := fun l => l.carrier -theorem lies_on_of_Seg_nd_toProj_eq_toProj {A B : P} {l : Line P} (ha : A LiesOn l) (hab : B ≠ A) (hp : Seg_nd.toProj ⟨SEG A B, hab⟩ = l.toProj) : B LiesOn l := by - rcases exists_ne_pt_pt_lies_on_of_line A l with ⟨X, h⟩ - let g := line_toProj_eq_seg_nd_toProj_of_lies_on ha h.1 h.2 - rw [← hp] at g - unfold Seg_nd.toProj Seg_nd.toVec_nd at g - simp only [ne_eq] at g - have c : colinear A X B := by - rw [← iff_true (colinear A X B), ← eq_iff_iff] - unfold colinear colinear_of_nd - simp [g] - by_cases (B = X ∨ A = B ∨ X = A) - · simp only [h, dite_eq_ite] - · simp only [h, dite_eq_ite] - exact (lies_on_iff_colinear_of_ne_lies_on_lies_on h.2 ha h.1 B).2 c +theorem linear (l : Line P) {A B C : P} (h₁ : A LiesOn l) (h₂ : B LiesOn l) (h₃ : C LiesOn l) : colinear A B C := by + unfold Line at l + revert l + rw [forall_quotient_iff (p := fun k : Line P => A LiesOn k → B LiesOn k → C LiesOn k → colinear A B C)] + unfold lies_on instCarrierLine Carrier.carrier Line.carrier at * + simp only + intro ray a b c + rw [@Quotient.lift_mk _ _ same_extn_line.setoid _ _ _] at * + cases a with + | inl a => + cases b with + | inl b => + cases c with + | inl c => + exact Ray.colinear_of_lies_on a b c + | inr c => + let ray' := Ray.mk C ray.toDir + have a' : A ∈ ray'.carrier := lies_on_pt_toDir_of_pt_lies_on_rev a c + have b' : B ∈ ray'.carrier := lies_on_pt_toDir_of_pt_lies_on_rev b c + exact Ray.colinear_of_lies_on a' b' (Ray.source_lies_on ray') + | inr b => + cases c with + | inl c => sorry + | inr c => sorry + | inr a => + cases b with + | inl b => + cases c with + | inl c => sorry + | inr c => sorry + | inr b => + cases c with + | inl c => sorry + | inr c => sorry + +theorem maximal (l : Line P) {A B : P} (h₁ : A ∈ l.carrier) (h₂ : B ∈ l.carrier) (h : B ≠ A) : (∀ (C : P), colinear A B C → (C ∈ l.carrier)) := sorry + +theorem nontriv (l : Line P) : ∃ (A B : P), (A ∈ l.carrier) ∧ (B ∈ l.carrier) ∧ (B ≠ A) := sorry -theorem Seg_nd_toProj_eq_toProj_iff_lies_on {A B : P} {l : Line P} (ha : A LiesOn l) (hab : B ≠ A) : B LiesOn l ↔ (Seg_nd.toProj ⟨SEG A B, hab⟩ = l.toProj) := by - constructor - exact fun a => line_toProj_eq_seg_nd_toProj_of_lies_on ha a hab - exact fun a => lies_on_of_Seg_nd_toProj_eq_toProj ha hab a +end Line --- Given distinct A B on a line, there exist C s.t. C LiesOn AB (a cor of Archimedean_property in Seg) and there exist D s.t. B LiesOn AD -theorem Line.exist_pt_beyond_pt {A B : P} {l : Line P} (hA : A LiesOn l) (hB : B LiesOn l) (h : B ≠ A) : (∃ C D : P, (C LiesOn l) ∧ (D LiesOn l) ∧ (A LiesInt (SEG C B)) ∧ (B LiesInt (SEG A D))) := sorry +-- A point lies on a line associated to a ray if and only if it lies on the ray or the reverse of the ray -end Archimedean_property +theorem Ray.lies_on_toLine_iff_lies_on_or_lies_on_rev (A : P) (ray : Ray P) : (A LiesOn ray.toLine) ↔ (A LiesOn ray) ∨ (A LiesOn ray.reverse) := sorry -section Line_passing_point_with_given_Proj +theorem Ray.lies_on_toLine_iff_lies_int_or_lies_int_rev_or_eq_source (A : P) (ray : Ray P) : (A LiesOn ray.toLine) ↔ (A LiesInt ray) ∨ (A LiesInt ray.reverse) ∨ (A = ray.source) := sorry -theorem exist_line_of_pt_proj (A : P) (pr : Proj) : ∃ l : Line P, A LiesOn l ∧ l.toProj = pr := by - rcases Quot.exists_rep pr with ⟨dir, hd⟩ - let r : Ray P := ⟨A, dir⟩ - use r.toLine - constructor - exact Ray.lies_on_toLine_of_lie_on (Ray.source_lies_on r) - rw [ray_toLine_toProj_eq_ray_toProj r] - exact hd +end carrier -theorem exist_unique_line_of_pt_proj (A : P) (pr : Proj) : ∃! l : Line P, A LiesOn l ∧ l.toProj = pr := by - rcases (exist_line_of_pt_proj A pr) with ⟨l₁, hl₁⟩ - use l₁ - constructor - exact hl₁ - intro l₂ hl₂ - rcases Quot.exists_rep pr with ⟨dir, _⟩ - have _ : dir.toVec +ᵥ A ≠ A := by - simp only [ne_eq, vadd_eq_self_iff_vec_eq_zero, Dir.toVec_ne_zero dir, not_false_eq_true] - apply (lies_on_iff_lies_on_iff_line_eq_line l₂ l₁).1 - intro X - by_cases X = A - · rw [h] - tauto - · rw [Seg_nd_toProj_eq_toProj_iff_lies_on hl₁.1 h, hl₁.2, Seg_nd_toProj_eq_toProj_iff_lies_on hl₂.1 h, hl₂.2] - -def Line.mk_pt_proj (A : P) (pr : Proj) : Line P := - Classical.choose (exist_unique_line_of_pt_proj A pr) - -theorem pt_lies_on_and_proj_eq_of_line_mk_pt_proj (A : P) (pr : Proj) : A LiesOn (Line.mk_pt_proj A pr) ∧ (Line.mk_pt_proj A pr).toProj = pr := by - exact (Classical.choose_spec (exist_unique_line_of_pt_proj A pr)).1 - -end Line_passing_point_with_given_Proj +end coercion end EuclidGeom \ No newline at end of file diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line_ex.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line_ex.lean index 53ccde5f..d01b10dc 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line_ex.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line_ex.lean @@ -1,4 +1,4 @@ -import EuclideanGeometry.Foundation.Axiom.Linear.Line' +import EuclideanGeometry.Foundation.Axiom.Linear.Line import EuclideanGeometry.Foundation.Axiom.Linear.Ray_ex noncomputable section @@ -44,6 +44,14 @@ theorem eq_of_pt_pt_lies_on_of_ne {A B : P} (h : B ≠ A) {l₁ l₂ : Line P}(h end pt_pt +section pt_proj + +theorem pt_lies_on_of_mk_pt_proj (proj : Proj) : A LiesOn Line.mk_pt_proj A proj := sorry + +theorem proj_eq_of_mk_pt_proj (proj : Proj) : (Line.mk_pt_proj A proj).toProj = proj := sorry + +end pt_proj + section coercion -- The line defined from a nontrivial segment is equal to the line defined from the ray associated this nontrivial segment diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean index 0c2229ec..4cc47fc8 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean @@ -1,4 +1,6 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Line +import EuclideanGeometry.Foundation.Axiom.Linear.Ray_ex +import EuclideanGeometry.Foundation.Axiom.Linear.Line_ex noncomputable section namespace EuclidGeom @@ -14,8 +16,6 @@ variable {P : Type _} [EuclideanPlane P] section coersion --- `Is this correct?` - instance : Coe Vec_nd (LinearObj P) where coe := fun v => LinearObj.vec_nd v @@ -43,32 +43,10 @@ def toProj (l : LinearObj P) : Proj := | seg_nd s => s.toProj | line l => l.toProj -/- No need to define this. Should never talk about a LinearObj directly in future. Only mention it for ∥ ⟂. -def IsOnLinearObj (a : P) (l : LinearObj P) : Prop := - match l with - | vec v h => False - | dir v => False - | ray r => a LiesOn r - | seg s nontriv => a LiesOn s - | line l => a ∈ l.carrier --/ - end LinearObj -/- -scoped infix : 50 "LiesOnarObj" => LinearObj.IsOnLinearObj --/ - -- Our definition of parallel for LinearObj is very general. Not only can it apply to different types of Objs, but also include degenerate cases, such as ⊆(inclusions), =(equal). -def parallel' {α β: Type _} (l₁ : α) (l₂ : β) [Coe α (LinearObj P)] [Coe β (LinearObj P)] : Prop := LinearObj.toProj (P := P) (Coe.coe l₁) = LinearObj.toProj (P := P) (Coe.coe l₂) - --- class PlaneFigure' (P : Type _) [EuclideanPlane P] {α : Type _} where - --- instance : PlaneFigure' P (LinearObj P) where - - - def parallel (l₁ l₂: LinearObj P) : Prop := l₁.toProj = l₂.toProj instance : IsEquiv (LinearObj P) parallel where @@ -83,26 +61,82 @@ scoped infix : 50 "∥" => parallel /- lots of trivial parallel relation of vec of 2 pt lies on Line, coersions, ... -/ section parallel_theorem +---- `eq_toProj theorems should be relocate to this file, they are in Line_ex now`. +theorem Ray.para_toLine (ray : Ray P) : (LinearObj.ray ray) ∥ ray.toLine := sorry + +theorem Seg_nd.para_toRay (seg_nd : Seg_nd P) : LinearObj.seg_nd seg_nd ∥ seg_nd.toRay := sorry -theorem ray_parallel_to_line_assoc_ray (ray : Ray P) : parallel (LinearObj.ray ray) ray.toLine := sorry +theorem Seg_nd.para_toLine (seg_nd : Seg_nd P) : LinearObj.seg_nd seg_nd ∥ seg_nd.toLine := sorry -theorem seg_parallel_to_ray_assoc_seg_of_nontriv (seg_nd : Seg_nd P) : LinearObj.seg_nd seg_nd ∥ seg_nd.toRay := sorry +-- many more... + +theorem Ray.para_toLine_of_para (ray ray' : Ray P) (h : LinearObj.ray ray ∥ ray') : (LinearObj.line ray.toLine) ∥ ray'.toLine := h + +theorem Ray.not_para_of_not_para_toLine (ray ray' : Ray P) (h : ¬ (LinearObj.line ray.toLine) ∥ ray'.toLine ) : ¬ LinearObj.ray ray ∥ ray' := h end parallel_theorem +section intersection_of_line + +section construction + +def intx_of_extn_line (r₁ r₂ : Ray P) (h : r₂.toProj ≠ r₁.toProj) : P := (cu r₁.toDir.toVec_nd r₂.toDir.toVec_nd (VEC r₁.source r₂.source) • r₁.toDir.toVec +ᵥ r₁.source) -section intersection_theorem +theorem intx_lies_on_fst_extn_line (r₁ r₂ : Ray P) (h : r₂.toProj ≠ r₁.toProj) : ((intx_of_extn_line r₁ r₂ h) ∈ r₁.carrier ∪ r₁.reverse.carrier) := sorry --- Let us consider the intersection of lines first. --- If two lines l₁ and l₂ are parallel, then there is a unique point on l₁ ∩ l₂. The definition of the point uses the ray intersection by first picking a point +theorem intx_lies_on_snd_extn_line (r₁ r₂ : Ray P) (h : r₂.toProj ≠ r₁.toProj) : ((intx_of_extn_line r₁ r₂ h) ∈ r₂.carrier ∪ r₂.reverse.carrier) := sorry +-- `key theorem` +theorem intx_eq_of_same_extn_line {a₁ b₁ a₂ b₂ : Ray P} (g₁ : same_extn_line a₁ a₂) (g₂ : same_extn_line b₁ b₂) (h₁ : b₁.toProj ≠ a₁.toProj) (h₂ : b₂.toProj ≠ a₂.toProj) : intx_of_extn_line a₁ b₁ h₁ = intx_of_extn_line a₂ b₂ h₂ := by + sorry + +-- This theorem deals only with `HEq` +theorem heq_funext {c₁ c₂ d: Sort _} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := Function.hfunext e (fun _ _ _ => (heq_of_eq (h _ _))) + +theorem heq_of_intx_of_extn_line (a₁ b₁ a₂ b₂ : Ray P) (h₁ : a₁ ≈ a₂) (h₂ : b₁ ≈ b₂) : HEq (fun h => intx_of_extn_line a₁ b₁ h) (fun h => intx_of_extn_line a₂ b₂ h) := by + have e : (Ray.toProj b₁ ≠ Ray.toProj a₁) = (Ray.toProj b₂ ≠ Ray.toProj a₂) := by + rw [h₁.1, h₂.1] + exact @heq_funext (Ray.toProj b₁ ≠ Ray.toProj a₁) (Ray.toProj b₂ ≠ Ray.toProj a₂) P e (fun h => intx_of_extn_line a₁ b₁ h) (fun h => intx_of_extn_line a₂ b₂ h) (intx_eq_of_same_extn_line h₁ h₂) + +/- the construction of the intersection point of two lines-/ +def Line.intx (l₁ l₂ : Line P) (h : l₂.toProj ≠ l₁.toProj) : P := @Quotient.hrecOn₂ (Ray P) (Ray P) same_extn_line.setoid same_extn_line.setoid (fun l l' => (Line.toProj l' ≠ Line.toProj l) → P) l₁ l₂ intx_of_extn_line heq_of_intx_of_extn_line h + +theorem Line.intx_is_intx {l₁ l₂ : Line P} (h : l₂.toProj ≠ l₁.toProj) : is_intx (Line.intx l₁ l₂ h) l₁ l₂ := sorry + +end construction + +section property + +-- In this section, we discuss the property of intersection point using `is_intx` instead of `Line.intx`. As a corollory, we deduce the symmetry of Line.intx. + +theorem unique_of_intx_of_line_of_not_para {A B : P} {l₁ l₂ : Line P} (h : l₂.toProj ≠ l₁.toProj) (a : is_intx A l₁ l₂) (b : is_intx B l₁ l₂) : B = A := by + by_contra d + let p := (SEG_nd A B d).toProj + have : Line.toProj l₂ = Line.toProj l₁ := by + apply Eq.trans (b := p) + · exact (line_toProj_eq_seg_nd_toProj_of_lies_on a.2 b.2 d).symm + · exact line_toProj_eq_seg_nd_toProj_of_lies_on a.1 b.1 d + tauto + +theorem Line.intx.symm {l₁ l₂ : Line P} (h : l₂.toProj ≠ l₁.toProj) : Line.intx l₂ l₁ h.symm = Line.intx l₁ l₂ h := unique_of_intx_of_line_of_not_para h (Line.intx_is_intx h) $ is_intx.symm (Line.intx_is_intx h.symm) + +theorem eq_of_parallel_and_pt_lies_on {A : P} {l₁ l₂ : Line P} (h₁ : A LiesOn l₁) (h₂ : A LiesOn l₂) (h : LinearObj.line l₁ ∥ l₂) : l₁ = l₂ := sorry + + +/-! theorem exists_intersection_of_nonparallel_lines {l₁ l₂ : Line P} (h : ¬ (l₁ ∥ (LinearObj.line l₂))) : ∃ p : P, p LiesOn l₁ ∧ p LiesOn l₂ := by rcases l₁.nontriv with ⟨A, ⟨B, hab⟩⟩ rcases l₂.nontriv with ⟨C, ⟨D, hcd⟩⟩ have e' : Seg_nd.toProj ⟨SEG A B, hab.2.2⟩ ≠ Seg_nd.toProj ⟨SEG C D, hcd.2.2⟩ := by rw [line_toProj_eq_seg_nd_toProj_of_lies_on hab.1 hab.2.1 hab.2.2, line_toProj_eq_seg_nd_toProj_of_lies_on hcd.1 hcd.2.1 hcd.2.2] exact h - have w : ∃ x y, VEC A C = x • VEC A B + y • VEC C D := linear_combination_of_not_colinear _ e' + have w : ∃ x y, VEC A C = x • VEC A B + y • VEC C D := by + let u := VEC A B + use ((VEC A B).1 * (VEC C D).2 - (VEC A B).2 * (VEC C D).1)⁻¹ * ((VEC A C).1 * (VEC C D).2 - (VEC C D).1 * (VEC A C).2) + use ((VEC A B).1 * (VEC C D).2 - (VEC A B).2 * (VEC C D).1)⁻¹ * ((VEC A C).1 * (VEC A B).2 - (VEC A B).1 * (VEC A C).2) + have cal := linear_combination_of_not_colinear (VEC A C) e' + simp only at cal + exact cal rcases w with ⟨x, ⟨y, e⟩⟩ let X := x • VEC A B +ᵥ A use X @@ -148,7 +182,10 @@ scoped notation "RayIntx" => Intersection_of_Lines_of_Rays theorem ray_intersection_lies_on_lines_of_rays {ray₁ ray₂ : Ray P} (h : ¬ (LinearObj.ray ray₁) ∥ ray₂) : (RayIntx h) LiesOn ray₁.toLine ∧ (RayIntx h) LiesOn ray₂.toLine := by sorry -- theorem ray_intersection_eq_line_intersection_of_rays {ray₁ ray₂ : Ray P} (h : ¬ (LinearObj.ray ray₁) ∥ ray₂) : RayInt h = LineInt (Ne.trans (ray_parallel_to_line_assoc_ray ray₁) h) := sorry +-/ + +end property -end intersection_theorem +end intersection_of_line end EuclidGeom \ No newline at end of file diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean index f00f38bb..6ed3abb8 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean @@ -72,7 +72,7 @@ section Perpendicular_constructions def perp_line (A : P) (l : Line P) := Line.mk_pt_proj A (l.toProj.perp) @[simp] -theorem toProj_of_perp_line_eq_toProj_perp (A : P) (l : Line P) : (perp_line A l).toProj = l.toProj.perp := (pt_lies_on_and_proj_eq_of_line_mk_pt_proj A _).2 +theorem toProj_of_perp_line_eq_toProj_perp (A : P) (l : Line P) : (perp_line A l).toProj = l.toProj.perp := (proj_eq_of_mk_pt_proj A _) theorem perp_foot_preparation (A : P) (l : Line P) : l.toProj ≠ (perp_line A l).toProj := by rw[toProj_of_perp_line_eq_toProj_perp] @@ -83,7 +83,7 @@ theorem perp_foot_preparation (A : P) (l : Line P) : l.toProj ≠ (perp_line A l exact mul_right_cancel h0 exact Proj.one_ne_I h1 -def perp_foot (A : P) (l : Line P) : P := intersection_of_nonparallel_line l (perp_line A l) (perp_foot_preparation A l) +def perp_foot (A : P) (l : Line P) : P := Line.intx l (perp_line A l) (perp_foot_preparation A l).symm def dist_pt_line (A : P) (l : Line P) := Seg.length (SEG A (perp_foot A l)) @@ -93,18 +93,18 @@ theorem perp_foot_eq_self_iff_lies_on (A : P) (l : Line P) : perp_foot A l = A intro h unfold perp_foot at h rw [← h] - apply intersection_of_nonparallel_line_lies_on_fst_line + apply (Line.intx_is_intx _).1 . intro A_on_l have A_on_perp_line_A_l:(A LiesOn perp_line A l) := by unfold perp_line - exact (pt_lies_on_and_proj_eq_of_line_mk_pt_proj A (Proj.perp (Line.toProj l))).1 + exact (pt_lies_on_of_mk_pt_proj A (Proj.perp (Line.toProj l))) have h:(perp_foot A l LiesOn l) := by unfold perp_foot - apply intersection_of_nonparallel_line_lies_on_fst_line + apply (Line.intx_is_intx _).1 have h':(perp_foot A l LiesOn perp_line A l) := by unfold perp_foot - apply intersection_of_nonparallel_line_lies_on_snd_line + apply (Line.intx_is_intx _).2 by_contra n have e : l = perp_line A l := by nth_rw 1 [← eq_line_of_pt_pt_of_ne n A_on_l h] @@ -117,8 +117,8 @@ theorem perp_foot_eq_self_iff_lies_on (A : P) (l : Line P) : perp_foot A l = A theorem line_of_self_perp_foot_eq_perp_line_of_not_lies_on {A : P} {l : Line P} (h : ¬ A LiesOn l) : LIN A (perp_foot A l) ((perp_foot_eq_self_iff_lies_on A l).mp.mt h) = perp_line A l := by have h0 : A LiesOn perp_line A l := by dsimp only [perp_line] - apply (pt_lies_on_and_proj_eq_of_line_mk_pt_proj A l.toProj.perp).1 - have h1 : perp_foot A l LiesOn perp_line A l := intersection_of_nonparallel_line_lies_on_snd_line (perp_foot_preparation A l) + apply (pt_lies_on_of_mk_pt_proj A l.toProj.perp) + have h1 : perp_foot A l LiesOn perp_line A l := (Line.intx_is_intx (perp_foot_preparation A l).symm).2 have h2 : perp_foot A l≠A := by rw[←perp_foot_eq_self_iff_lies_on A l] at h exact h diff --git a/EuclideanGeometry/Unused/Line.lean b/EuclideanGeometry/Unused/Line.lean new file mode 100644 index 00000000..9a39feb3 --- /dev/null +++ b/EuclideanGeometry/Unused/Line.lean @@ -0,0 +1,342 @@ +import EuclideanGeometry.Foundation.Axiom.Linear.Colinear + +noncomputable section +namespace EuclidGeom + +@[ext] +class Line (P : Type _) [EuclideanPlane P] where + carrier : Set P + linear : ∀ (A B C : P), (A ∈ carrier) → (B ∈ carrier) → (C ∈ carrier) → colinear A B C + maximal : ∀ (A B : P), (A ∈ carrier) → (B ∈ carrier) → (B ≠ A) → (∀ (C : P), colinear A B C → (C ∈ carrier)) + nontriv : ∃ (A B : P), (A ∈ carrier) ∧ (B ∈ carrier) ∧ (B ≠ A) + +namespace Line + +variable {P : Type _} [EuclideanPlane P] + +-- define a line from two points + +def mk_pt_pt (A B : P) (h : B ≠ A) : Line P where + carrier := {C : P | ∃ t : ℝ, VEC A C = t • VEC A B} + linear x y z:= by + unfold Membership.mem Set.instMembershipSet Set.Mem setOf + simp only [forall_exists_index] + intro tx hx ty hy tz hz + by_cases ty ≠ tx ∧ tz ≠ tx ∧ ty ≠ tz + · rcases h with ⟨h₁, _, _⟩ + have w₂ : ∃ t : ℝ, VEC x z = t • VEC x y := by + use (ty - tx)⁻¹ * (tz - tx) + rw [mul_smul] + symm + apply ((inv_smul_eq_iff₀ (Iff.mpr sub_ne_zero h₁)).2) + rw [← vec_sub_vec A x y, ← vec_sub_vec A x z, hx, hy, hz] + rw [← sub_smul, ← sub_smul, ← mul_smul, ← mul_smul, mul_comm] + apply colinear_of_vec_eq_smul_vec' + exact w₂ + · have h' : (ty = tx) ∨ (tz = tx) ∨ (ty = tz) := by tauto + by_cases ty = tx + · rw [pt_eq_pt_of_eq_smul_smul h hy hx] + exact triv_colinear _ _ + · by_cases tz = tx + · rw [pt_eq_pt_of_eq_smul_smul h hz hx] + exact flip_colinear_snd_trd $ triv_colinear _ _ + · have h : ty = tz := by tauto + rw [pt_eq_pt_of_eq_smul_smul h hy hz] + exact flip_colinear_fst_snd $ flip_colinear_snd_trd $ triv_colinear _ _ + maximal x y := by + unfold Membership.mem Set.instMembershipSet Set.Mem setOf + simp only [forall_exists_index] + intro tx hx ty hy hne z c + have e : VEC x y = (ty - tx) • VEC A B := by + rw [← vec_sub_vec A x y, hx, hy, sub_smul] + rcases (eq_mul_vec_iff_colinear_of_ne hne).1 c with ⟨t, ht⟩ + use tx + t * (ty - tx) + rw [← vec_add_vec A x z, ht, e, hx, ← mul_smul, ← add_smul] + nontriv := by + use A + use B + unfold Membership.mem Set.instMembershipSet Set.Mem setOf + simp only [forall_exists_index] + constructor + use 0 + simp only [vec_same_eq_zero, zero_smul] + constructor + use 1 + simp only [one_smul] + exact h + +end Line + +scoped notation "LIN" => Line.mk_pt_pt + +namespace Line + +variable {P : Type _} [EuclideanPlane P] + +/- Def of point lies on a line, LiesInt is not defined -/ +protected def IsOn (a : P) (l : Line P) : Prop := + a ∈ l.carrier + +instance : Carrier P (Line P) where + carrier := fun l => l.carrier + +end Line + +-- Now we introduce useful theorems to avoid using more unfolds in further proofs. +variable {P : Type _} [EuclideanPlane P] + +section Compaitiblity_of_coersions_of_mk_pt_pt + +-- The first point and the second point in Line.mk_pt_pt LiesOn the line it make. + +theorem fst_pt_lies_on_line_of_pt_pt {A B : P} (h : B ≠ A) : A LiesOn LIN A B h := by + unfold lies_on Carrier.carrier Line.instCarrierLine + simp only [Set.setOf_mem_eq] + unfold Line.carrier Line.mk_pt_pt + simp only [Set.mem_setOf_eq, vec_same_eq_zero] + use 0 + simp only [zero_smul] + +theorem snd_pt_lies_on_line_of_pt_pt {A B : P} (h : B ≠ A) : B LiesOn LIN A B h := by + unfold lies_on Carrier.carrier Line.instCarrierLine + simp only [Set.setOf_mem_eq] + unfold Line.carrier Line.mk_pt_pt + simp only [Set.mem_setOf_eq, vec_same_eq_zero] + use 1 + simp only [one_smul] + +theorem pt_lies_on_line_of_pt_pt_of_ne {A B : P} (h: B ≠ A) : A LiesOn LIN A B h ∧ B LiesOn LIN A B h := by + constructor + exact fst_pt_lies_on_line_of_pt_pt h + exact snd_pt_lies_on_line_of_pt_pt h + +theorem lies_on_line_of_pt_pt_iff_colinear {A B : P} (h : B ≠ A) : ∀ X : P, (X LiesOn (LIN A B h)) ↔ colinear A B X := by + intro X + constructor + intro hx + apply (LIN A B h).linear + exact fst_pt_lies_on_line_of_pt_pt h + exact snd_pt_lies_on_line_of_pt_pt h + exact hx + intro c + apply (LIN A B h).maximal A B + exact fst_pt_lies_on_line_of_pt_pt h + exact snd_pt_lies_on_line_of_pt_pt h + exact h + exact c + +end Compaitiblity_of_coersions_of_mk_pt_pt + +section Define_line_toProj + +/- examine a line has uniquely defined toProj -/ + +theorem vec_eq_smul_vec_of_lies_on {l : Line P} {A B X Y : P} (ha : A LiesOn l) (hb : B LiesOn l) (hx : X LiesOn l) (hy : Y LiesOn l) (hab : B ≠ A) : ∃ t : ℝ, VEC X Y = t • VEC A B := by + rcases (eq_mul_vec_iff_colinear_of_ne hab).1 (Line.linear A B X ha hb hx) with ⟨t₁, e₁⟩ + rcases (eq_mul_vec_iff_colinear_of_ne hab).1 (Line.linear A B Y ha hb hy) with ⟨t₂, e₂⟩ + use t₂ - t₁ + rw [← vec_sub_vec A, e₁, e₂, sub_smul] + +theorem toProj_eq_toProj_of_Seg_nd_lies_on {l : Line P} {A B X Y : P} (ha : A LiesOn l) (hb : B LiesOn l) (hx : X LiesOn l) (hy : Y LiesOn l) (hab : B ≠ A) (hxy : Y ≠ X) : Seg_nd.toProj ⟨SEG A B, hab⟩ = Seg_nd.toProj ⟨SEG X Y, hxy⟩ := by + rcases (vec_eq_smul_vec_of_lies_on ha hb hx hy hab) with ⟨t, e⟩ + exact eq_toProj_of_smul _ _ e + +/- define Line.toProj -/ + +theorem uniqueness_of_proj_of_line (l : Line P) : ∀ A B C D : P, (A LiesOn l) → (B LiesOn l) → (C LiesOn l) → (D LiesOn l) → (hab : B ≠ A) → (hcd : D ≠ C) → Seg_nd.toProj ⟨SEG A B, hab⟩ = Seg_nd.toProj ⟨SEG C D, hcd⟩ := by + intro A B C D ha hb hc hd hab hcd + exact toProj_eq_toProj_of_Seg_nd_lies_on ha hb hc hd hab hcd + +theorem exist_unique_proj_of_line (l : Line P) : ∃! pr : Proj, ∀ (A B : P) (ha : A LiesOn l) (hb : B LiesOn l) (h : B ≠ A), Seg_nd.toProj ⟨SEG A B, h⟩ = pr := by + rcases l.nontriv with ⟨x, ⟨y, c⟩⟩ + use Seg_nd.toProj ⟨SEG x y, c.2.2⟩ + simp + constructor + intro A B ha hb hab + exact toProj_eq_toProj_of_Seg_nd_lies_on ha hb c.1 c.2.1 hab c.2.2 + intro pr w + rw [← w] + exact c.1 + exact c.2.1 + +def Line.toProj (l : Line P) : Proj := + Classical.choose (exist_unique_proj_of_line l) + -- by choose pr _ using (exist_unique_proj_of_line l) + -- exact pr + +-- If you don't want to use Classical.choose, please use this theorem to simplify your Line.toProj. + +theorem line_toProj_eq_seg_nd_toProj_of_lies_on {A B : P} {l : Line P} (ha : A LiesOn l) (hb : B LiesOn l) (hab : B ≠ A) : Seg_nd.toProj ⟨SEG A B, hab⟩ = l.toProj := (Classical.choose_spec (exist_unique_proj_of_line l)).1 A B ha hb hab + +theorem line_of_pt_pt_toProj_eq_seg_nd_toProj {A B : P} (h : B ≠ A) : (LIN A B h).toProj = Seg_nd.toProj ⟨SEG A B, h⟩ := by + symm + apply line_toProj_eq_seg_nd_toProj_of_lies_on + exact fst_pt_lies_on_line_of_pt_pt h + exact snd_pt_lies_on_line_of_pt_pt h + +end Define_line_toProj + +section Compatibility_of_LiesOn + +-- This is also a typical proof that shows how to use the four conditions in the def of a line. Please write it shorter in future. + +theorem lies_on_iff_colinear_of_ne_lies_on_lies_on {A B : P} {l : Line P} (h : B ≠ A) (ha : A LiesOn l) (hb : B LiesOn l) : ∀ C : P, (C LiesOn l) ↔ colinear A B C := by + intro C + constructor + intro hc + apply l.linear + exact ha + exact hb + exact hc + intro c + apply l.maximal A B + exact ha + exact hb + exact h + exact c + +/- Two lines are equal iff they have the same carrier -/ + +theorem lies_on_iff_lies_on_iff_line_eq_line (l₁ l₂ : Line P) : (∀ A : P, A LiesOn l₁ ↔ A LiesOn l₂) ↔ l₁ = l₂ := by + constructor + intro hiff + exact Line.ext l₁ l₂ (Set.ext hiff) + intro e + rw [e] + simp only [forall_const] + +/- tautological theorems of Line.mk_pt_pt -/ + +theorem eq_line_of_pt_pt_of_ne {A B : P} {l : Line P} (h : B ≠ A) (ha : A LiesOn l) (hb : B LiesOn l) : LIN A B h = l := by + apply (lies_on_iff_lies_on_iff_line_eq_line (LIN A B h) l).1 + intro X + constructor + intro hx + apply (lies_on_iff_colinear_of_ne_lies_on_lies_on h ha hb X).2 + exact (lies_on_line_of_pt_pt_iff_colinear h X).1 hx + intro hx + exact (lies_on_line_of_pt_pt_iff_colinear h X).2 ((lies_on_iff_colinear_of_ne_lies_on_lies_on h ha hb X).1 hx) + +theorem eq_of_pt_pt_lies_on_of_ne {A B : P} (h : B ≠ A) {l₁ l₂ : Line P}(hA₁ : A LiesOn l₁) (hB₁ : B LiesOn l₁) (hA₂ : A LiesOn l₂) (hB₂ : B LiesOn l₂) : l₁ = l₂ := sorry + +theorem colinear_iff_exist_line_lies_on (A B C : P) : colinear A B C ↔ ∃ l : Line P, (A LiesOn l) ∧ (B LiesOn l) ∧ (C LiesOn l) := by + sorry + +end Compatibility_of_LiesOn +/- def coe from ray to line-/ + +def Ray.toLine (r : Ray P) := LIN r.source (r.toDir.toVec +ᵥ r.source) (by + simp only [ne_eq, vadd_eq_self_iff_vec_eq_zero] + exact Dir.toVec_ne_zero r.toDir) + +instance : Coe (Ray P) (Line P) where + coe := Ray.toLine + +theorem ray_toLine_toProj_eq_ray_toProj (r : Ray P) : r.toLine.toProj = r.toProj := by + sorry + +/- def coe from non trivial segment to line-/ + +def Seg_nd.toLine (seg_nd : Seg_nd P) := (LIN seg_nd.1.source seg_nd.1.target seg_nd.2) + +def Line.mk_pt_vec_nd (A : P) (vec_nd : Vec_nd) := (LIN A (vec_nd.1 +ᵥ A) (by + sorry)) + +section Compaitiblity_of_coersions + +-- If a point lies on a ray, then it lies on the line associated to the ray. +theorem Ray.lies_on_toLine_of_lie_on {A : P} {r : Ray P} (h : A LiesOn r) : A LiesOn (r.toLine) := sorry + +theorem Seg_nd.lies_on_toLine_of_lie_on {A : P} {s : Seg_nd P} (h : A LiesOn s.1) : A LiesOn (s.toLine) := sorry + +-- If A and B are two distinct points, they lie on the line AB +theorem Ray.source_lies_on_toLine (l : Ray P) : l.source LiesOn l.toLine := sorry + +theorem Seg_nd.source_lies_on_toLine (s : Seg_nd P) : s.1.source LiesOn s.toLine := sorry + +theorem Seg_nd.target_lies_on_toLine (s : Seg_nd P) : s.1.target LiesOn s.toLine := sorry + +-- The line defined from a nontrivial segment is equal to the line defined from the ray associated this nontrivial segment + +theorem Seg_nd.toLine_eq_toRay_toLine (seg_nd : Seg_nd P) : seg_nd.toLine = (seg_nd.toRay).toLine := sorry + +theorem line_of_pt_pt_eq_ray_toLine {A B : P} (h : B ≠ A) : LIN A B h = Ray.toLine (RAY A B h) := sorry + +theorem line_of_pt_pt_eq_seg_nd_toLine {A B : P} (h : B ≠ A) : LIN A B h = Seg_nd.toLine ⟨SEG A B, h⟩ := rfl + +end Compaitiblity_of_coersions + +section Archimedean_property + +-- there are two distinct points on a line + +theorem exists_ne_pt_pt_lies_on_of_line (A : P) (l : Line P) : ∃ B : P, B LiesOn l ∧ B ≠ A := by + rcases l.nontriv with ⟨X, ⟨Y, _⟩⟩ + by_cases A = X + · use Y + rw [h] + tauto + · use X + tauto + +theorem lies_on_of_Seg_nd_toProj_eq_toProj {A B : P} {l : Line P} (ha : A LiesOn l) (hab : B ≠ A) (hp : Seg_nd.toProj ⟨SEG A B, hab⟩ = l.toProj) : B LiesOn l := by + rcases exists_ne_pt_pt_lies_on_of_line A l with ⟨X, h⟩ + let g := line_toProj_eq_seg_nd_toProj_of_lies_on ha h.1 h.2 + rw [← hp] at g + unfold Seg_nd.toProj Seg_nd.toVec_nd at g + simp only [ne_eq] at g + have c : colinear A X B := by + rw [← iff_true (colinear A X B), ← eq_iff_iff] + unfold colinear colinear_of_nd + simp [g] + by_cases (B = X ∨ A = B ∨ X = A) + · simp only [h, dite_eq_ite] + · simp only [h, dite_eq_ite] + exact (lies_on_iff_colinear_of_ne_lies_on_lies_on h.2 ha h.1 B).2 c + +theorem Seg_nd_toProj_eq_toProj_iff_lies_on {A B : P} {l : Line P} (ha : A LiesOn l) (hab : B ≠ A) : B LiesOn l ↔ (Seg_nd.toProj ⟨SEG A B, hab⟩ = l.toProj) := by + constructor + exact fun a => line_toProj_eq_seg_nd_toProj_of_lies_on ha a hab + exact fun a => lies_on_of_Seg_nd_toProj_eq_toProj ha hab a + +-- Given distinct A B on a line, there exist C s.t. C LiesOn AB (a cor of Archimedean_property in Seg) and there exist D s.t. B LiesOn AD +theorem Line.exist_pt_beyond_pt {A B : P} {l : Line P} (hA : A LiesOn l) (hB : B LiesOn l) (h : B ≠ A) : (∃ C D : P, (C LiesOn l) ∧ (D LiesOn l) ∧ (A LiesInt (SEG C B)) ∧ (B LiesInt (SEG A D))) := sorry + +end Archimedean_property + +section Line_passing_point_with_given_Proj + +theorem exist_line_of_pt_proj (A : P) (pr : Proj) : ∃ l : Line P, A LiesOn l ∧ l.toProj = pr := by + rcases Quot.exists_rep pr with ⟨dir, hd⟩ + let r : Ray P := ⟨A, dir⟩ + use r.toLine + constructor + exact Ray.lies_on_toLine_of_lie_on (Ray.source_lies_on r) + rw [ray_toLine_toProj_eq_ray_toProj r] + exact hd + +theorem exist_unique_line_of_pt_proj (A : P) (pr : Proj) : ∃! l : Line P, A LiesOn l ∧ l.toProj = pr := by + rcases (exist_line_of_pt_proj A pr) with ⟨l₁, hl₁⟩ + use l₁ + constructor + exact hl₁ + intro l₂ hl₂ + rcases Quot.exists_rep pr with ⟨dir, _⟩ + have _ : dir.toVec +ᵥ A ≠ A := by + simp only [ne_eq, vadd_eq_self_iff_vec_eq_zero, Dir.toVec_ne_zero dir, not_false_eq_true] + apply (lies_on_iff_lies_on_iff_line_eq_line l₂ l₁).1 + intro X + by_cases X = A + · rw [h] + tauto + · rw [Seg_nd_toProj_eq_toProj_iff_lies_on hl₁.1 h, hl₁.2, Seg_nd_toProj_eq_toProj_iff_lies_on hl₂.1 h, hl₂.2] + +def Line.mk_pt_proj (A : P) (pr : Proj) : Line P := + Classical.choose (exist_unique_line_of_pt_proj A pr) + +theorem pt_lies_on_and_proj_eq_of_line_mk_pt_proj (A : P) (pr : Proj) : A LiesOn (Line.mk_pt_proj A pr) ∧ (Line.mk_pt_proj A pr).toProj = pr := by + exact (Classical.choose_spec (exist_unique_line_of_pt_proj A pr)).1 + +end Line_passing_point_with_given_Proj + +end EuclidGeom \ No newline at end of file diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel'.lean b/EuclideanGeometry/Unused/Parallel.lean similarity index 50% rename from EuclideanGeometry/Foundation/Axiom/Linear/Parallel'.lean rename to EuclideanGeometry/Unused/Parallel.lean index ddf16101..0c2229ec 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel'.lean +++ b/EuclideanGeometry/Unused/Parallel.lean @@ -1,6 +1,4 @@ -import EuclideanGeometry.Foundation.Axiom.Linear.Line' -import EuclideanGeometry.Foundation.Axiom.Linear.Ray_ex -import EuclideanGeometry.Foundation.Axiom.Linear.Line_ex +import EuclideanGeometry.Foundation.Axiom.Linear.Line noncomputable section namespace EuclidGeom @@ -16,6 +14,8 @@ variable {P : Type _} [EuclideanPlane P] section coersion +-- `Is this correct?` + instance : Coe Vec_nd (LinearObj P) where coe := fun v => LinearObj.vec_nd v @@ -43,10 +43,32 @@ def toProj (l : LinearObj P) : Proj := | seg_nd s => s.toProj | line l => l.toProj +/- No need to define this. Should never talk about a LinearObj directly in future. Only mention it for ∥ ⟂. +def IsOnLinearObj (a : P) (l : LinearObj P) : Prop := + match l with + | vec v h => False + | dir v => False + | ray r => a LiesOn r + | seg s nontriv => a LiesOn s + | line l => a ∈ l.carrier +-/ + end LinearObj +/- +scoped infix : 50 "LiesOnarObj" => LinearObj.IsOnLinearObj +-/ + -- Our definition of parallel for LinearObj is very general. Not only can it apply to different types of Objs, but also include degenerate cases, such as ⊆(inclusions), =(equal). +def parallel' {α β: Type _} (l₁ : α) (l₂ : β) [Coe α (LinearObj P)] [Coe β (LinearObj P)] : Prop := LinearObj.toProj (P := P) (Coe.coe l₁) = LinearObj.toProj (P := P) (Coe.coe l₂) + +-- class PlaneFigure' (P : Type _) [EuclideanPlane P] {α : Type _} where + +-- instance : PlaneFigure' P (LinearObj P) where + + + def parallel (l₁ l₂: LinearObj P) : Prop := l₁.toProj = l₂.toProj instance : IsEquiv (LinearObj P) parallel where @@ -61,82 +83,26 @@ scoped infix : 50 "∥" => parallel /- lots of trivial parallel relation of vec of 2 pt lies on Line, coersions, ... -/ section parallel_theorem ----- `eq_toProj theorems should be relocate to this file, they are in Line_ex now`. -theorem Ray.para_toLine (ray : Ray P) : (LinearObj.ray ray) ∥ ray.toLine := sorry - -theorem Seg_nd.para_toRay (seg_nd : Seg_nd P) : LinearObj.seg_nd seg_nd ∥ seg_nd.toRay := sorry -theorem Seg_nd.para_toLine (seg_nd : Seg_nd P) : LinearObj.seg_nd seg_nd ∥ seg_nd.toLine := sorry +theorem ray_parallel_to_line_assoc_ray (ray : Ray P) : parallel (LinearObj.ray ray) ray.toLine := sorry --- many more... - -theorem Ray.para_toLine_of_para (ray ray' : Ray P) (h : LinearObj.ray ray ∥ ray') : (LinearObj.line ray.toLine) ∥ ray'.toLine := h - -theorem Ray.not_para_of_not_para_toLine (ray ray' : Ray P) (h : ¬ (LinearObj.line ray.toLine) ∥ ray'.toLine ) : ¬ LinearObj.ray ray ∥ ray' := h +theorem seg_parallel_to_ray_assoc_seg_of_nontriv (seg_nd : Seg_nd P) : LinearObj.seg_nd seg_nd ∥ seg_nd.toRay := sorry end parallel_theorem -section intersection_of_line - -section construction - -def intx_of_extn_line (r₁ r₂ : Ray P) (h : r₂.toProj ≠ r₁.toProj) : P := (cu r₁.toDir.toVec_nd r₂.toDir.toVec_nd (VEC r₁.source r₂.source) • r₁.toDir.toVec +ᵥ r₁.source) -theorem intx_lies_on_fst_extn_line (r₁ r₂ : Ray P) (h : r₂.toProj ≠ r₁.toProj) : ((intx_of_extn_line r₁ r₂ h) ∈ r₁.carrier ∪ r₁.reverse.carrier) := sorry +section intersection_theorem -theorem intx_lies_on_snd_extn_line (r₁ r₂ : Ray P) (h : r₂.toProj ≠ r₁.toProj) : ((intx_of_extn_line r₁ r₂ h) ∈ r₂.carrier ∪ r₂.reverse.carrier) := sorry +-- Let us consider the intersection of lines first. +-- If two lines l₁ and l₂ are parallel, then there is a unique point on l₁ ∩ l₂. The definition of the point uses the ray intersection by first picking a point --- `key theorem` -theorem intx_eq_of_same_extn_line {a₁ b₁ a₂ b₂ : Ray P} (g₁ : same_extn_line a₁ a₂) (g₂ : same_extn_line b₁ b₂) (h₁ : b₁.toProj ≠ a₁.toProj) (h₂ : b₂.toProj ≠ a₂.toProj) : intx_of_extn_line a₁ b₁ h₁ = intx_of_extn_line a₂ b₂ h₂ := by - sorry - --- This theorem deals only with `HEq` -theorem heq_funext {c₁ c₂ d: Sort _} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := Function.hfunext e (fun _ _ _ => (heq_of_eq (h _ _))) - -theorem heq_of_intx_of_extn_line (a₁ b₁ a₂ b₂ : Ray P) (h₁ : a₁ ≈ a₂) (h₂ : b₁ ≈ b₂) : HEq (fun h => intx_of_extn_line a₁ b₁ h) (fun h => intx_of_extn_line a₂ b₂ h) := by - have e : (Ray.toProj b₁ ≠ Ray.toProj a₁) = (Ray.toProj b₂ ≠ Ray.toProj a₂) := by - rw [h₁.1, h₂.1] - exact @heq_funext (Ray.toProj b₁ ≠ Ray.toProj a₁) (Ray.toProj b₂ ≠ Ray.toProj a₂) P e (fun h => intx_of_extn_line a₁ b₁ h) (fun h => intx_of_extn_line a₂ b₂ h) (intx_eq_of_same_extn_line h₁ h₂) - -/- the construction of the intersection point of two lines-/ -def Line.intx (l₁ l₂ : Line P) (h : l₂.toProj ≠ l₁.toProj) : P := @Quotient.hrecOn₂ (Ray P) (Ray P) same_extn_line.setoid same_extn_line.setoid (fun l l' => (Line.toProj l' ≠ Line.toProj l) → P) l₁ l₂ intx_of_extn_line heq_of_intx_of_extn_line h - -theorem Line.intx_is_intx {l₁ l₂ : Line P} (h : l₂.toProj ≠ l₁.toProj) : is_intx (Line.intx l₁ l₂ h) l₁ l₂ := sorry - -end construction - -section property - --- In this section, we discuss the property of intersection point using `is_intx` instead of `Line.intx`. As a corollory, we deduce the symmetry of Line.intx. - -theorem unique_of_intx_of_line_of_not_para {A B : P} {l₁ l₂ : Line P} (h : l₂.toProj ≠ l₁.toProj) (a : is_intx A l₁ l₂) (b : is_intx B l₁ l₂) : B = A := by - by_contra d - let p := (SEG_nd A B d).toProj - have : Line.toProj l₂ = Line.toProj l₁ := by - apply Eq.trans (b := p) - · exact (line_toProj_eq_seg_nd_toProj_of_lies_on a.2 b.2 d).symm - · exact line_toProj_eq_seg_nd_toProj_of_lies_on a.1 b.1 d - tauto - -theorem Line.intx.symm {l₁ l₂ : Line P} (h : l₂.toProj ≠ l₁.toProj) : Line.intx l₂ l₁ h.symm = Line.intx l₁ l₂ h := unique_of_intx_of_line_of_not_para h (Line.intx_is_intx h) $ is_intx.symm (Line.intx_is_intx h.symm) - -theorem eq_of_parallel_and_pt_lies_on {A : P} {l₁ l₂ : Line P} (h₁ : A LiesOn l₁) (h₂ : A LiesOn l₂) (h : LinearObj.line l₁ ∥ l₂) : l₁ = l₂ := sorry - - -/-! theorem exists_intersection_of_nonparallel_lines {l₁ l₂ : Line P} (h : ¬ (l₁ ∥ (LinearObj.line l₂))) : ∃ p : P, p LiesOn l₁ ∧ p LiesOn l₂ := by rcases l₁.nontriv with ⟨A, ⟨B, hab⟩⟩ rcases l₂.nontriv with ⟨C, ⟨D, hcd⟩⟩ have e' : Seg_nd.toProj ⟨SEG A B, hab.2.2⟩ ≠ Seg_nd.toProj ⟨SEG C D, hcd.2.2⟩ := by rw [line_toProj_eq_seg_nd_toProj_of_lies_on hab.1 hab.2.1 hab.2.2, line_toProj_eq_seg_nd_toProj_of_lies_on hcd.1 hcd.2.1 hcd.2.2] exact h - have w : ∃ x y, VEC A C = x • VEC A B + y • VEC C D := by - let u := VEC A B - use ((VEC A B).1 * (VEC C D).2 - (VEC A B).2 * (VEC C D).1)⁻¹ * ((VEC A C).1 * (VEC C D).2 - (VEC C D).1 * (VEC A C).2) - use ((VEC A B).1 * (VEC C D).2 - (VEC A B).2 * (VEC C D).1)⁻¹ * ((VEC A C).1 * (VEC A B).2 - (VEC A B).1 * (VEC A C).2) - have cal := linear_combination_of_not_colinear (VEC A C) e' - simp only at cal - exact cal + have w : ∃ x y, VEC A C = x • VEC A B + y • VEC C D := linear_combination_of_not_colinear _ e' rcases w with ⟨x, ⟨y, e⟩⟩ let X := x • VEC A B +ᵥ A use X @@ -182,10 +148,7 @@ scoped notation "RayIntx" => Intersection_of_Lines_of_Rays theorem ray_intersection_lies_on_lines_of_rays {ray₁ ray₂ : Ray P} (h : ¬ (LinearObj.ray ray₁) ∥ ray₂) : (RayIntx h) LiesOn ray₁.toLine ∧ (RayIntx h) LiesOn ray₂.toLine := by sorry -- theorem ray_intersection_eq_line_intersection_of_rays {ray₁ ray₂ : Ray P} (h : ¬ (LinearObj.ray ray₁) ∥ ray₂) : RayInt h = LineInt (Ne.trans (ray_parallel_to_line_assoc_ray ray₁) h) := sorry --/ - -end property -end intersection_of_line +end intersection_theorem end EuclidGeom \ No newline at end of file diff --git a/EuclideanGeometry/Unused.lean b/EuclideanGeometry/Unused/Unused.lean similarity index 100% rename from EuclideanGeometry/Unused.lean rename to EuclideanGeometry/Unused/Unused.lean diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector'.lean b/EuclideanGeometry/Unused/Vector.lean similarity index 94% rename from EuclideanGeometry/Foundation/Axiom/Basic/Vector'.lean rename to EuclideanGeometry/Unused/Vector.lean index 63fafdb3..ad9ef2c1 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector'.lean +++ b/EuclideanGeometry/Unused/Vector.lean @@ -742,8 +742,7 @@ def cu (u v w: Vec) : ℝ := (det u v)⁻¹ * (w.1 * v.2 - v.1 * w.2) def cv (u v w: Vec) : ℝ := (det u v)⁻¹ * (u.1 * w.2 - w.1 * u.2) -theorem det_eq_zero_iff_eq_smul (u v : Vec) (hu : u ≠ 0) : det u v = 0 ↔ (∃ (t : ℝ), v = t • u) := by - unfold det +theorem det_eq_zero_iff_eq_smul (u v : Vec) (hu : u ≠ 0) : u.1 * v.2 - u.2 * v.1 = 0 ↔ (∃ (t : ℝ), v = t • u) := by have h : (u.1 ≠ 0) ∨ (u.2 ≠ 0) := by by_contra _ have h₁ : u.1 = 0 := by tauto @@ -782,52 +781,34 @@ theorem det_eq_zero_iff_eq_smul (u v : Vec) (hu : u ≠ 0) : det u v = 0 ↔ ( rcases e ring -theorem det'_ne_zero_of_not_colinear {u v : Vec} (hu : u ≠ 0) (h' : ¬(∃ (t : ℝ), v = t • u)) : det' u v ≠ 0 := by - unfold det' +theorem linear_combination_of_not_colinear' {u v w : Vec} (hu : u ≠ 0) (h' : ¬(∃ (t : ℝ), v = t • u)) : ∃ (cu cv : ℝ), w = cu • u + cv • v := by have h₁ : (¬ (∃ (t : ℝ), v = t • u)) → (¬ (u.1 * v.2 - u.2 * v.1 = 0)) := by intro _ by_contra h₂ let _ := (det_eq_zero_iff_eq_smul u v hu).1 h₂ tauto + let d := u.1 * v.2 - u.2 * v.1 + have h₃ : d ≠ 0 := h₁ h' + use d⁻¹ * (w.1 * v.2 - v.1 * w.2) + use d⁻¹ * (u.1 * w.2 - w.1 * u.2) symm - field_simp - have trivial : ((u.re : ℂ) * v.im - u.im * v.re) = ((Sub.sub (α := ℝ) (Mul.mul (α := ℝ) u.re v.im) (Mul.mul (α := ℝ) u.im v.re)) : ℂ) := by - symm - calc - ((Sub.sub (α := ℝ) (Mul.mul (α := ℝ) u.re v.im) (Mul.mul (α := ℝ) u.im v.re)) : ℂ) = ((Mul.mul u.re v.im) - (Mul.mul u.im v.re)) := Complex.ofReal_sub _ _ - _ = ((Mul.mul u.re v.im) - (u.im * v.re)) := by - rw [← Complex.ofReal_mul u.im v.re] - rfl - _ = ((u.re * v.im) - (u.im * v.re)) := by - rw [← Complex.ofReal_mul u.re _] - rfl - rw [trivial, ← ne_eq] - symm - rw [ne_eq, Complex.ofReal_eq_zero] - exact h₁ h' - -theorem linear_combination_of_not_colinear' {u v w : Vec} (hu : u ≠ 0) (h' : ¬(∃ (t : ℝ), v = t • u)) : w = (cu u v w) • u + (cv u v w) • v := by - unfold cu cv det - have : ((u.re : ℂ) * v.im - u.im * v.re) ≠ 0 := det'_ne_zero_of_not_colinear hu h' - field_simp + rw [mul_smul, mul_smul, ← smul_add] + apply ((inv_smul_eq_iff₀ h₃).2) + unfold HSMul.hSMul instHSMul SMul.smul MulAction.toSMul Complex.mulAction Complex.instSMulRealComplex + simp only [smul_eq_mul, zero_mul, sub_zero] apply Complex.ext - simp + simp only [add_zero, Complex.add_re] ring - simp + simp only [add_zero, Complex.add_im] ring -theorem linear_combination_of_not_colinear_vec_nd {u v : Vec_nd} (w : Vec) (h' : Vec_nd.toProj u ≠ Vec_nd.toProj v) : w = (cu u.1 v.1 w) • u.1 + (cv u.1 v.1 w) • v.1 := by +theorem linear_combination_of_not_colinear {u v : Vec_nd} (w : Vec) (h' : Vec_nd.toProj u ≠ Vec_nd.toProj v) : ∃ (cᵤ cᵥ : ℝ), w = cᵤ • u.1 + cᵥ • v.1 := by have h₁ : (Vec_nd.toProj u ≠ Vec_nd.toProj v) → ¬(∃ (t : ℝ), v.1 = t • u.1) := by intro _ by_contra h₂ let _ := (Vec_nd.eq_toProj_iff u v).2 h₂ tauto - exact @linear_combination_of_not_colinear' u.1 v.1 w u.2 (h₁ h') - -theorem linear_combination_of_not_colinear_dir {u v : Dir} (w : Vec) (h' : u.toProj ≠ v.toProj) : w = (cu u.1 v.1 w) • u.1 + (cv u.1 v.1 w) • v.1 := by - have h₁ : (u.toProj ≠ v.toProj) → ¬(∃ (t : ℝ), v.1 = t • u.1) := by - sorry - exact @linear_combination_of_not_colinear' u.1 v.1 w u.toVec_nd.2 (h₁ h') + exact linear_combination_of_not_colinear' u.2 (h₁ h') end Linear_Algebra