/- Clara L"oh 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     

-- exercise: 
/- Tests whether (x,y,z) is an anti-triangle -/
-- def is_anti_triangle

/- 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
/- If (x,y,z) is a triangle, then also (z,x,y) is a triangle. -/
-- lemma triangle_cyc

/- Some examples of Mini Geometry models -/

/- The empty model: 
   It has no points, no lines and the trivial lies_on relation; 
   in addition to the definition of these components, we have 
   to supply proofs for the axioms MG1 and MG2.
   -/
def empty_lies_on 
    (x : empty)
    (g : empty)
:= false    

lemma empty_satisfies_MG1 
: satisfies_MG1 empty empty empty_lies_on
:= 
begin -- this is so simple that it can be checked automatically
  by tauto, 
end 

lemma empty_satisfies_MG2
: satisfies_MG2 empty empty empty_lies_on
:=
begin -- this is also almost automatic; found via hint
  by {unfold satisfies_MG2,  
      simp at *, 
      exact dec_trivial},
end

-- Thus: The empty model indeed is a Mini Geometry: 
instance empty_MG : MG empty empty 
:= MG.mk empty_lies_on
         empty_satisfies_MG1 
         empty_satisfies_MG2


/- The I model:
   We consider the Mini Geometry associated with the graph 
    0 --- 1    2 
-/

inductive I_P : Type 
| I_0 
| I_1
| I_2

inductive I_G : Type
| I_01

def I_lies_on
    (x : I_P)
    (y : I_G) 
  : Prop  
:= 
begin
   -- thanks to the special structure of the I model, 
   -- we only need to check  whether x is I_0 or I_1;
   -- we use a case distinction:
   cases x,
     case I_P.I_0 : {exact true},
     case I_P.I_1 : {exact true},
     case I_P.I_2 : {exact false}, 
end

-- in the I model, all lines are equal (there is only one line)
lemma I_G_all_equal 
      (g : I_G)
      (h : I_G)
    : (g = h)
:= 
begin
  -- we use a case distinction:   
  cases g,       -- only one possible case for g: g = I_01
    cases h,     -- only one possible case for h: h = I_01
      exact rfl, -- thus, g = h, by reflexivity
end         

lemma I_satisfies_MG1
: satisfies_MG1 I_P I_G I_lies_on
:= 
begin
  -- in order to show this forall-statement,
  -- we prove the statement for each member 
  assume x y : I_P,
  assume g h : I_G,
  show ( x ≠ y 
       ∧ I_lies_on x g ∧ I_lies_on y g 
       ∧ I_lies_on x h ∧ I_lies_on y h)
       → g = h, 
  by {intro, -- adding the assumption on the left hand side of the implication 
      exact I_G_all_equal g h}, -- there is only one line!
end

lemma I_satisfies_MG2
: satisfies_MG2 I_P I_G I_lies_on
:= 
begin
  assume g : I_G, -- there is only one possibility! I_G.I_01
  show ∃ x y : I_P, x ≠ y 
                  ∧ I_lies_on x g ∧ I_lies_on y g,
  begin
    use I_P.I_0, -- take x as "0"
    use I_P.I_1, -- take y as "1"
    by tauto,    -- now it can simply be checked automatically
  end
end

-- The I model indeed is a Mini Geometry
instance I_MG : MG I_P I_G
:= MG.mk I_lies_on
         I_satisfies_MG1
         I_satisfies_MG2


/- Parallel postulate -/
def is_parallel_through
    (P : Type*) (G : Type*) [MG P G]
    (x : P)
    (g : G)
    (h : G)
:=  MG.lies_on x h ∧ are_parallel P G g h   

def parallel_postulate
    (P : Type*) (G : Type*) [MG P G]
:= ∀ x : P, ∀ g : G, 
     (¬ MG.lies_on x g) 
   → (∃ h : G, is_parallel_through P G x g h
               ∧ (∀ k : G, is_parallel_through P G x g k → k = h ))

/- The parallel postulate is independent of the Mini Geometry axioms,
   i.e., there exist models of Mini Geometry that satisfy it 
     and there exist models of Mini Geometry that do not satisfy it. -/

-- The empty model satisfies the parallel postulate
lemma pp_empty_MG
: parallel_postulate empty empty
:=
begin 
  -- again, this is so simple 
  -- that this can be basically solved automatically
  assume x,
  show _, 
       by {cases x}
end

-- The I model does not satisfy the parallel postulate
lemma not_pp_I_MG
: ¬ parallel_postulate I_P I_G
:=
begin
  -- these will be our witnesses:   
  let x : I_P := I_P.I_2,
  let g : I_G := I_G.I_01,   

  -- x does not lie on g
  have x_not_on_g: ¬ MG.lies_on x g, 
       by {exact not_of_eq_false rfl},
                    
  -- but there is no parallel through x
  have no_parallel_through_x: 
       ¬ (∃ h : I_G, is_parallel_through I_P I_G x g h),
  begin -- by exhaustive search
    exact (finset.exists_mem_empty_iff (λ (x : I_G), are_parallel I_P I_G g x)).mp,
  end,

  -- we can now combine these properties into establishing that
  -- the parallel postulate is not satisfied, because of x and g
  by {unfold parallel_postulate, 
      refine not_forall.mpr _, 
      use x, 
      refine not_forall.mpr _, 
      use g,
      finish}, 
end

-- Thus, the parallel postulate is independent of MG
theorem pp_is_independent_of_MG
: (∃ P G : Type, ∃ MGPG : MG P G,   @parallel_postulate P G MGPG)
∧ (∃ P G : Type, ∃ MGPG : MG P G, ¬ @parallel_postulate P G MGPG)
:=
begin
  have pp_example: ∃ P G : Type, ∃ MGPG : MG P G, @parallel_postulate P G MGPG,
       begin -- the empty MG is such an example
         use empty,
         use empty,
         use empty_MG,
         exact pp_empty_MG,
       end,     
  
  have pp_nonexample: (∃ P G : Type, ∃ MGPG : MG P G, ¬ @parallel_postulate P G MGPG),
       begin -- the I MG is such a non-example
         use I_P,
         use I_G,
         use I_MG,
         exact not_pp_I_MG,
       end,

  -- it remains to combine both parts into the and-statement
  by {exact and.intro pp_example pp_nonexample},   
end