/- Clara Löh 2023 -/

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 
https://loeh.app.ur.de/teaching/geometrie_ss23/lecture_notes.pdf
-/

/- Mini Geometry models -/

/-
MG 1: Zu je zwei verschiedenen Punkten gibt es höchstens 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 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 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 y 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 line g
  rcases line_xy with ⟨g : G, xy_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},     

  -- recombining x_in_g and y_in_g in the other order
  show lie_on_a_common_line P G y x,
       by {unfold lie_on_a_common_line,
           use g,
           exact and.intro y_in_g x_in_g},
end

/- 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,  -- unfold the definition
      simp,                  -- simplify
      exact dec_trivial},    -- the remaining decision problem is 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)
    (g : 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: g = I_G.I_01
    cases h,     -- only one possible case: h = I_G.I_01
      exact rfl, -- thus g = h by reflexivity of equality; "simp" would also work
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,
  assume x_neq_y_xy_on_gh : 
    x ≠ y ∧ I_lies_on x g ∧ I_lies_on y g 
          ∧ I_lies_on x h ∧ I_lies_on y h,
  show g = h,
       by {exact I_G_all_equal g h},         
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,
  from 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
  -- by a case distinction (there is no case)
  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

  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_in_g : ¬ MG.lies_on x g,
       by {exact not_of_eq_false rfl},

  -- but there is no parallel to through x
  have no_parallel_through_x : 
       ¬ (∃ h : I_G, is_parallel_through I_P I_G x g h), 
  from begin 
         -- proof "by contradiction"
         assume ex_parallel_through_x,
         rcases ex_parallel_through_x with 
                ⟨ h, h_parallel_through_x ⟩,
         have h_is_g : g = h, 
              by {exact I_G_all_equal g h}, 
         have x_in_g : I_lies_on x g,
              by {simp[h_is_g],
                  apply h_parallel_through_x.1},
         show false,
              by tauto,
         -- alternatively: by exhaustive search
         -- exact (finset.exists_meme_empty_iff (λ (h : I_G), are_parallel I_P I_G g h)).mp,              
       end,     

  -- we use x and g and the fact no_parallel_through_x, 
  -- together with basic manipulation of all/existential quantifiers and negations
  show _, 
       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
  show _, 
       by {exact and.intro pp_example pp_nonexample},   
end