search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
27 stars 56 forks source link

Reorganization of classes, Add class `Fig` `LinearFig` #183

Open jjdishere opened 1 year ago

jjdishere commented 1 year ago

There is a problem of DirFig.toDir, it may be not def equal to Ray.toDir otherclass.toDir. Do we need to force they are the same? Is everything ok if we keep this def equal? Or do we need to bring DirFig into Class.lean then define toDir as early as that? (so there will be no other defs of toDir)

jjdishere commented 1 year ago

It is possible to reorganize whole class structure.

  1. Fig means have carrier,
  2. Linear means any 3 pts in Carrier is colinear,
  3. DirFig means Fig + has toDir
  4. ProjFig is LinearObj (which cannot extends DirFig, instead Coe DirFig ProjFig, Line is only ProjFig) Maybe ProjFig is exactly Linear?
  5. Intersect should be defined for any 2 Carrier. In Circle files, show it is equiv to r >= d.