From 352811d45b721d19a15493beb260f2d583b37544 Mon Sep 17 00:00:00 2001 From: jjdishere Date: Thu, 21 Sep 2023 20:26:29 +0800 Subject: [PATCH] parallel --- .../Foundation/Axiom/Basic/Class.lean | 5 ++- .../Foundation/Axiom/Linear/Line_ex.lean | 2 +- .../Foundation/Axiom/Linear/Parallel'.lean | 40 ++++++------------- 3 files changed, 16 insertions(+), 31 deletions(-) diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Class.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Class.lean index 24c76e03..394e0091 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Class.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Class.lean @@ -22,7 +22,7 @@ def lies_int {P : Type _} [EuclideanPlane P] {α : Type _} [Interior P α] (p : def is_intx {P : Type _} [EuclideanPlane P] {α β: Type _} [Carrier P α] [Carrier P β] (p : P) (F : α) (G : β) := p ∈ (Carrier.carrier F) ∧ p ∈ (Carrier.carrier G) -theorem is_intx.symm {P : Type _} [EuclideanPlane P] {α β: Type _} [Carrier P α] [Carrier P β] (p : P) (F : α) (G : β) (h : is_intx p F G) : is_intx p G F := And.symm h +theorem is_intx.symm {P : Type _} [EuclideanPlane P] {α β: Type _} [Carrier P α] [Carrier P β] {p : P} {F : α} {G : β} (h : is_intx p F G) : is_intx p G F := And.symm h scoped infix : 50 "LiesOn" => lies_on scoped infix : 50 "LiesInt" => lies_int @@ -38,7 +38,8 @@ class Convex2D (P: Type _) [EuclideanPlane P] (α : Type _) extends (Carrier P /- Intersection -/ -/- -- scoped notation p "LiesInt" F => HasLiesInt.lies_int p F +/-! +-- scoped notation p "LiesInt" F => HasLiesInt.lies_int p F def IsFallsOn {α β : Type _} (A : α) (B : β) [HasLiesOn P α] [HasLiesOn P β] : Prop := ∀ (p : P), (p LiesOn A) → (p LiesOn B) diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line_ex.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line_ex.lean index 15118c1b..53ccde5f 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line_ex.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line_ex.lean @@ -7,7 +7,7 @@ namespace EuclidGeom variable {P : Type _} [EuclideanPlane P] section compatibility - +-- `eq_toProj theorems should be relocate to file parallel using parallel`. variable (A B : P) (h : B ≠ A) (ray : Ray P) (seg_nd : Seg_nd P) section pt_pt diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel'.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel'.lean index bce7316a..ddf16101 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel'.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel'.lean @@ -1,5 +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 @@ -15,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 @@ -44,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 @@ -84,7 +61,7 @@ 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 @@ -124,7 +101,7 @@ theorem heq_of_intx_of_extn_line (a₁ b₁ a₂ b₂ : Ray P) (h₁ : a₁ ≈ /- 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 +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 @@ -135,9 +112,16 @@ section property 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 - sorry + 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 unique_of_intx_of_not_para /-! theorem exists_intersection_of_nonparallel_lines {l₁ l₂ : Line P} (h : ¬ (l₁ ∥ (LinearObj.line l₂))) : ∃ p : P, p LiesOn l₁ ∧ p LiesOn l₂ := by