6 kyu

Incidence Geometry #1

46donaldsebleung
Description
Loading description...
Theorem Proving
Mathematics
Fundamentals
View
AllIssuesQuestionsSuggestions1Show Resolved
  • Please sign in or sign up to leave a comment.
  • Opabinia Avatar

    Looks like a cool little series.

    BRB, learning Lean!

  • monadius Avatar

    Approved. I changed class incidence to structure incidence in both Preloaded and Description but I didn't change [incidence point line incident_with] to (s : incidence point line incident_with).

    • donaldsebleung Avatar

      Thanks for approving my Kata :+1:

      That being said, my comment below about changing class to structure as an improvement was misleading - I only made that change initially because I couldn't figure out how to make the square brackets used for typeclass resolution work with the Kata setup so I changed [incidence point line incident_with] to (s : incidence point line incident_with) with incidence a class which @kbuzzard mentioned was bad practice. Once I figured out how to make the square brackets work with the Kata setup, I changed it back into a class since @kckennylau said that that would be more suitable.

      Would you mind changing structure back into class for me? Cheers :-)

    • monadius Avatar

      Changed structure back into class.

  • donaldsebleung Avatar

    Possible improvements:

    • Change incidence into a structure (currently a class)
    • Move point, line, incident_with and the incidence instance before the colon to avoid unnecessary intro(s) initially
  • kbuzzard Avatar

    incidence is defined as a class, but no instances of it are ever created, and so it may as well be a structure. Note that changing it to a structure may change some () to {} in the fields, so s.I_1 might now have slightly different behaviour.

    In the submission

    def SUBMISSION := ∀ (point line : Type) (incident_with : point → line → Prop)
  (s : incidence point line incident_with) l m,
  l ≠ m →

    I would be tempted to move point, line, incident_with and s before the colon, so the user is not asked to intro them. 

    def SUBMISSION (point line : Type) (incident_with : point → line → Prop)
  (s : incidence point line incident_with) : \forall l m,
  l ≠ m → ...