open import Level
open import Ordinals
open import logic
open import Relation.Nullary
module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) where

open import zf
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
open import  Relation.Binary.PropositionalEquality
open import Data.Nat.Properties 
open import Data.Empty
open import Relation.Binary
open import Relation.Binary.Core

open import nat
import OD

open inOrdinal O
open OD O
open OD.OD
open OD._==_
open ODAxiom odAxiom

open import zfc

--- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
---
record choiced  ( X : OD) : Set (suc n) where
  field
     a-choice : OD
     is-in : X ∋ a-choice

open choiced

OD→ZFC : ZFC
OD→ZFC   = record { 
    ZFSet = OD 
    ; _∋_ = _∋_ 
    ; _≈_ = _==_ 
    ; ∅  = od∅
    ; Select = Select
    ; isZFC = isZFC
 } where
    -- infixr  200 _∈_
    -- infixr  230 _∩_ _∪_
    isZFC : IsZFC (OD )  _∋_  _==_ od∅ Select 
    isZFC = record {
       choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
       choice = λ A {X} A∋X not → is-in (choice-func X not)
     } where
         choice-func :  (X : OD ) → ¬ ( X == od∅ ) → choiced X
         choice-func  X not = have_to_find where
                 ψ : ( ox : Ordinal ) → Set (suc n)
                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ def X x )) ∨ choiced X
                 lemma-ord : ( ox : Ordinal  ) → ψ ox
                 lemma-ord  ox = TransFinite {ψ} induction ox where
                    ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
                    ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
                    ∋-p A x | case1 (lift t)  = yes t
                    ∋-p A x | case2 t  = no (λ x → t (lift x ))
                    ∀-imply-or :  {A : Ordinal  → Set n } {B : Set (suc n) }
                        → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
                    ∀-imply-or  {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
                    ∀-imply-or  {A} {B} ∀AB | case1 (lift t) = case1 t
                    ∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x (lift not ))) where
                         lemma : ¬ ((x : Ordinal ) → A x) →  B
                         lemma not with p∨¬p B
                         lemma not | case1 b = b
                         lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
                    induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
                    induction x prev with ∋-p X ( ord→od x) 
                    ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
                    ... | no ¬p = lemma where
                         lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
                         lemma1 y with ∋-p X (ord→od y)
                         lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
                         lemma = ∀-imply-or lemma1
                 have_to_find : choiced X
                 have_to_find = dont-or  (lemma-ord (od→ord X )) ¬¬X∋x where
                     ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
                     ¬¬X∋x nn = not record {
                            eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt) 
                          ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
                        }
         record Minimal (x : OD) (ne : ¬ (x == od∅ ) )  : Set (suc n) where
           field
               min : OD
               x∋min :   x ∋ min 
               min-empty :  (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
         open Minimal
         open _∧_
         induction : {x : OD} → ({y : OD} → x ∋ y → (ne : ¬ (y == od∅ )) → Minimal y ne ) →  (ne : ¬ (x == od∅ )) → Minimal x ne
         induction {x} prev ne = c2
            where
             ch : choiced x
             ch = choice-func x ne 
             c1 : OD
             c1 = a-choice ch   -- x ∋ c1
             c2 : Minimal x ne
             c2 with p∨¬p ( (y : OD ) → ¬ ( def c1 (od→ord y) ∧ (def x (od→ord  y)))  )
             c2 | case1 Yes = record {
                  min = c1
               ;  x∋min = is-in ch 
               ;  min-empty = Yes
               }
             c2 | case2 No = c3 where
                y1 : OD
                y1 =  record { def = λ y → ( def c1 y ∧ def x y) } 
                noty1 : ¬ (y1 == od∅ )
                noty1 not = ⊥-elim ( No (λ z n → ∅< n not ) )
                ch1 : choiced y1 --  a-choice ch1 ∈ c1 , a-choice ch1 ∈ x
                ch1 = choice-func y1 noty1
                c3 : Minimal x ne
                c3 with is-o∅ (od→ord (a-choice ch1))
                ... | yes eq =  record {
                      min = od∅
                   ;  x∋min = def-subst {x} {od→ord (a-choice ch1)} {x} (proj2 (is-in ch1)) refl (trans eq (sym ord-od∅) ) 
                   ;  min-empty = λ z p → ⊥-elim ( ¬x<0 (proj1 p) )
                  } 
                ... | no n =  record {
                      min = min min3
                   ;  x∋min = x∋min3 (x∋min min3)
                   ;  min-empty = min3-empty -- λ y p → min3-empty min3 y p    -- p : (min min3 ∋ y) ∧ (x ∋ y)
                  }  where
                       lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅ 
                       lemma eq = begin 
                           od→ord (a-choice ch1) 
                         ≡⟨ cong (λ k → od→ord k ) (==→o≡ eq ) ⟩
                           od→ord od∅  
                         ≡⟨ ord-od∅ ⟩
                           o∅
                         ∎ where open ≡-Reasoning 
                       --  Minimal (a-choice ch1) ch1not
                       --      min ∈ a-choice ch1 ,  min ∩ a-choice ch1  ≡ ∅
                       ch1not : ¬ (a-choice ch1 == od∅)
                       ch1not ch1=0 = n (lemma ch1=0)
                       min3 : Minimal (a-choice ch1) ch1not
                       min3 =  prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0))
                       x∋min3 : a-choice ch1 ∋ min min3 → x ∋ min min3
                       x∋min3 lt = {!!}
                       min3-empty : (y : OD ) → ¬ ((min min3 ∋ y) ∧ (x ∋ y))
                       min3-empty y p = min-empty min3 y record { proj1 = proj1 p ; proj2 = ? } --  (min min3 ∋ y) ∧ (a-choice ch1 ∋ y)
                           -- p : (min min3 ∋ y) ∧ (x ∋ y)

                   
         Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne
         Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne ) 
         minimal : (x : OD  ) → ¬ (x == od∅ ) → OD 
         minimal x not = min (Min1 x not ) 
         x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
         x∋minimal x ne = x∋min (Min1 x ne) 
         minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
         minimal-1 x ne y = min-empty (Min1 x ne ) y