Hierarchy Classes of Linear Objects

Recall we have the following linear objects:

• Vec in Basic.Vector
• VecND in Basic.Vector
• Dir in Basic.Vector
• Proj in Basic.Vector
• Seg in Linear.Ray
• SegND in Linear.Ray DirFig
• Ray in Linear.Ray DirFig
• DirLine in Linear.Line DirFig
• Line in Linear.Line Fig In this file, we assign linear objects into different abstract classes so that properties holds for the whole classes can be proved in a single theorem.

Main Definitions

• LinFig : The class of linear figures, i.e. every three points in the carrier is collinear.
• DirObj : The class of objects with direction, i.e. equipped with a toDir method. It does not have to be a plane figure, e.g. VecND and Dir itself.
• DirFig : The class of linear figures with direction. Each figure is equipped with a toDirLine method.
• ProjObj : The class of objects with projective direction, i.e. equipped with a toProj method. It does not have to be a plane figure, e.g. VecND and Proj itself.
• ProjFig : The class of linear figures with projective direction. Each figure is equipped with a toLine method.

Usage of Classes

• LinFig : A basic class.
• DirObj : Every two objects has a angle between them. This angle should be saved as Dir and has 3 representations, AngValue (mod 2π), (-π, π], [0, 2π).
• DirFig : toDirLine method, can define odist, odist_sign, Left, Right, OnLine, OffLine.
• ProjObj : parallel and perpendicular.
• ProjFig : toLine method, compatibility of carrier to Line.

Only theorems about ProjFig will be dealt in this file.

Further Work

class EuclidGeom.LinFig (α : Type u_1) (P : outParam (Type u_2)) [outParam (EuclidGeom.EuclideanPlane P)] extends EuclidGeom.Fig : Type (max u_1 u_2)

• carrier : α → Set P
• collinear' : ∀ {A B C : P} {F : α}, EuclidGeom.lies_on A F → EuclidGeom.lies_on B F → EuclidGeom.lies_on C F → EuclidGeom.Collinear A B C

class EuclidGeom.ProjObj (β : Type u_1) : Type u_1

• toProj : β → EuclidGeom.Proj

class EuclidGeom.ProjFig (α : Type u_1) (P : outParam (Type u_2)) [outParam (EuclidGeom.EuclideanPlane P)] extends EuclidGeom.LinFig , EuclidGeom.ProjObj : Type (max u_1 u_2)

• carrier : α → Set P
• collinear' : ∀ {A B C : P} {F : α}, EuclidGeom.lies_on A F → EuclidGeom.lies_on B F → EuclidGeom.lies_on C F → EuclidGeom.Collinear A B C
• toProj : α → EuclidGeom.Proj
• toLine : α → EuclidGeom.Line P
• carrier_subset_toLine : ∀ {F : α}, EuclidGeom.Fig.carrier F ⊆ EuclidGeom.Line.carrier (EuclidGeom.toLine F)
• toLine_toProj_eq_toProj : ∀ {F : α}, (EuclidGeom.toLine F).toProj = EuclidGeom.toProj F

class EuclidGeom.DirObj (β : Type u_1) extends EuclidGeom.ProjObj : Type u_1

• toProj : β → EuclidGeom.Proj
• toDir : β → EuclidGeom.Dir
• toDir_toProj_eq_toProj : ∀ {G : β}, (EuclidGeom.toDir G).toProj = EuclidGeom.toProj G

class EuclidGeom.DirFig (α : Type u_1) (P : outParam (Type u_2)) [outParam (EuclidGeom.EuclideanPlane P)] extends EuclidGeom.ProjFig : Type (max u_1 u_2)

• carrier : α → Set P
• collinear' : ∀ {A B C : P} {F : α}, EuclidGeom.lies_on A F → EuclidGeom.lies_on B F → EuclidGeom.lies_on C F → EuclidGeom.Collinear A B C
• toProj : α → EuclidGeom.Proj
• toLine : α → EuclidGeom.Line P
• carrier_subset_toLine : ∀ {F : α}, EuclidGeom.Fig.carrier F ⊆ EuclidGeom.Line.carrier (EuclidGeom.toLine F)
• toLine_toProj_eq_toProj : ∀ {F : α}, (EuclidGeom.toLine F).toProj = EuclidGeom.toProj F
• toDir : α → EuclidGeom.Dir
• toDir_toProj_eq_toProj : ∀ {G : α}, (EuclidGeom.DirFig.toDir G).toProj = EuclidGeom.toProj G
• toDirLine : α → EuclidGeom.DirLine P
• toDirLine_toDir_eq_toDir : ∀ {F : α}, (EuclidGeom.toDirLine F).toDir = EuclidGeom.DirFig.toDir F
• toDirLine_toLine_eq_toLine : ∀ {F : α}, (EuclidGeom.toDirLine F).toLine = EuclidGeom.toLine F
• reverse : α → α
• rev_rev : ∀ {F : α}, EuclidGeom.DirFig.reverse (EuclidGeom.DirFig.reverse F) = F
• toDirLine_rev_eq_to_rev_toDirLine : ∀ {F : α}, (EuclidGeom.toDirLine F).reverse = EuclidGeom.toDirLine (EuclidGeom.DirFig.reverse F)

instance EuclidGeom.instDirObjVecND : EuclidGeom.DirObj EuclidGeom.VecND

Equations

• EuclidGeom.instDirObjVecND = EuclidGeom.DirObj.mk EuclidGeom.VecND.toDir @EuclidGeom.instDirObjVecND.proof_1

instance EuclidGeom.instDirObjDir : EuclidGeom.DirObj EuclidGeom.Dir

Equations

• EuclidGeom.instDirObjDir = EuclidGeom.DirObj.mk id @EuclidGeom.instDirObjDir.proof_1

instance EuclidGeom.instProjObjProj : EuclidGeom.ProjObj EuclidGeom.Proj

Equations

• EuclidGeom.instProjObjProj = { toProj := id }

instance EuclidGeom.instLinFigSeg {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.LinFig (EuclidGeom.Seg P) P

Equations

• One or more equations did not get rendered due to their size.

instance EuclidGeom.instDirFigSegND {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.DirFig (EuclidGeom.SegND P) P

Equations

• One or more equations did not get rendered due to their size.

instance EuclidGeom.instDirFigRay {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.DirFig (EuclidGeom.Ray P) P

Equations

• One or more equations did not get rendered due to their size.

instance EuclidGeom.instDirFigDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.DirFig (EuclidGeom.DirLine P) P

Equations

• One or more equations did not get rendered due to their size.

instance EuclidGeom.instProjFigLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.ProjFig (EuclidGeom.Line P) P

Equations

• One or more equations did not get rendered due to their size.

theorem EuclidGeom.carrier_toProj_eq_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} {A : P} {B : P} [EuclidGeom.ProjFig α P] {F : α} [_h : EuclidGeom.PtNe B A] (ha : EuclidGeom.lies_on A F) (hb : EuclidGeom.lies_on B F) : (SEG_nd A B).toProj = EuclidGeom.toProj F

theorem EuclidGeom.line_of_pt_toProj_eq_to_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} {A : P} [EuclidGeom.ProjFig α P] {F : α} (h : EuclidGeom.lies_on A F) : EuclidGeom.Line.mk_pt_proj A (EuclidGeom.toProj F) = EuclidGeom.toLine F

theorem EuclidGeom.DirFig.rev_toDir_eq_neg_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.DirFig α P] (l : α) : EuclidGeom.DirFig.toDir (EuclidGeom.DirFig.reverse l) = -EuclidGeom.DirFig.toDir l

theorem EuclidGeom.DirFig.rev_toProj_eq_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.DirFig α P] (l : α) : EuclidGeom.toProj (EuclidGeom.DirFig.reverse l) = EuclidGeom.toProj l