/- -- todo! add your name, 2021 -/

import tactic  -- standard proof tactics
open classical -- we want to work in classical logic

/-
# Mini Geometry

This is a basic implementation of Mini Geometry, 
as described in 
http://www.mathematik.uni-r.de/loeh/teaching/geometrie_ss21/lecture_notes.pdf
-/

/- Mini Geometry models -/

/-
MG 1: Zu je zwei verschiedenen Punkten gibt es h"ochstens eine Gerade, so
dass beide Punkte auf dieser Geraden liegen.

For each two different points, there exists at most one line 
such that both points lie on this line.
-/
def satisfies_MG1 
    (P : Type*) -- "points"
    (G : Type*) -- "lines"
    (lies_on : P → G → Prop)
:= ∀ x y : P, ∀ g h : G,
   ( x ≠ y 
   ∧ lies_on x g ∧ lies_on y g 
   ∧ lies_on x h ∧ lies_on y h)
   → g = h

/-
MG 2: Auf jeder Geraden liegen mindestens zwei verschiedene Punkte.

For each line, there exist at least two points that lie on this line.
-/
def satisfies_MG2
    (P : Type*) -- "points"
    (G : Type*) -- "lines"
    (lies_on : P → G → Prop)
:= ∀ g : G, ∃ x y : P,
   x ≠ y
   ∧ lies_on x g ∧ lies_on y g

/-
Lean version of Mini Geometry models:
-/
class MG
      (P : Type*) -- "points"
      (G : Type*) -- "lines"
:= (lies_on : P → G → Prop)  
   (MG1 : satisfies_MG1 P G lies_on)
   (MG2 : satisfies_MG2 P G lies_on)          


/- Some basic notions -/

/- Tests whether x is an intersection of g and h -/
def is_intersection_of
    (P : Type*) (G : Type*) [MG P G]
    (x : P)
    (g : G)
    (h : G)
:= MG.lies_on x g 
 ∧ MG.lies_on x h    

/- Tests whether g and h are parallel -/
def are_parallel
    (P : Type*) (G : Type*) [MG P G]
    (g : G)
    (h : G)
:= ¬ (∃ x : P, is_intersection_of P G x g h)
    
/- Tests whether x and y lie on a common line -/    
def lie_on_a_common_line
    (P : Type*) (G : Type*) [MG P G]
    (x : P)
    (y : P)
:= ∃ g : G, ( MG.lies_on x g
            ∧ MG.lies_on y g )    

/- Tests whether (x,y,z) is a triangle -/
def is_triangle
    (P : Type*) (G : Type*) [MG P G]
    (x : P)
    (y : P)
    (z : P)
:= lie_on_a_common_line P G x y
 ∧ lie_on_a_common_line P G y z
 ∧ lie_on_a_common_line P G z x     

/- Some very simple properties -/

/- If x and y lie on a common line, 
   then y and x lie on a common line. -/
lemma lie_on_a_common_line_sym 
    (P : Type*) (G : Type*) [MG P G]
    (x : P)
    (y : P)
    (line_xy: lie_on_a_common_line P G x y)
  : lie_on_a_common_line P G y x
:= 
begin
  /- extracting a witness g for the fact that x and y 
     lie on a common line -/
  rcases line_xy with ⟨ g : G, xy_in_g ⟩, 
  /- xy_in_g shows that x_in_g and y_in_g -/
  have x_in_g : MG.lies_on x g, 
       by {apply xy_in_g.1},
  have y_in_g : MG.lies_on y g,
       by {apply xy_in_g.2},
  -- we now only recombine the statements in a different order     
  show lie_on_a_common_line P G y x, 
       by {unfold lie_on_a_common_line,    -- unfolding the definition 
           use g,                          -- taking care of ∃
           exact and.intro y_in_g x_in_g}, -- reassembling the ∧-statement
end

/- Exercise 2.3 -/
-- todo! complete this definition!
def is_tripod
   -- todo! complete this definition!
:= -- todo! complete this definition!

/- Exercise 2.4 

If (m,x,y,z) is a tripod with "centre m" and if (x,y,z) 
is a triangle, then (m,x,y) is also a triangle.

-/
lemma tritri
      -- todo! add the hypotheses
    : -- todo! add the claim
:=
begin

  -- todo! add the proof (if you are stuck: proceed as in the lecture of 20.04.2021)
  sorry,

end