{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Ordinals
import OD 
module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) where

open import zf
open import logic
-- open import partfunc {n} O

open import Relation.Nullary 
open import Relation.Binary 
open import Data.Empty 
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
import BAlgbra 


open inOrdinal O
open OD O
open OD.OD
open ODAxiom odAxiom
import OrdUtil
import ODUtil
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O


import ODC


open _∧_
open _∨_
open Bool


open HOD

record Element (A : HOD) : Set (suc n) where
    field
       elm : HOD
       is-elm : A ∋ elm

open Element

IsPartialOrderSet : ( A : HOD ) → Set (suc n)
IsPartialOrderSet A = IsStrictPartialOrder _≡A_ _<A_  where
   _<A_ : (x y : Element A ) → Set n
   x <A y = elm x < elm y
   _≡A_ : (x y : Element A ) → Set (suc n)
   x ≡A y = elm x ≡ elm y

open _==_
open _⊆_

isA : { A B  : HOD } → B ⊆ A → (x : Element B) → Element A
isA B⊆A x = record { elm = elm x ; is-elm = incl B⊆A (is-elm x) }

⊆-IsPartialOrderSet : { A B  : HOD } → B ⊆ A → IsPartialOrderSet A → IsPartialOrderSet B 
⊆-IsPartialOrderSet {A} {B} B⊆A  PA = record {
       isEquivalence = record { refl = refl ; sym = sym ; trans = trans } ;  trans = λ {x} {y} {z} → trans1 {x} {y} {z} 
     ; irrefl = λ {x} {y} → irrefl1 {x} {y} ; <-resp-≈ = resp0 
   } where
   _<B_ : (x y : Element B ) → Set n
   x <B y = elm x < elm y
   trans1 : {x y z : Element B} → x <B y → y <B z → x <B z 
   trans1 {x} {y} {z} x<y y<z  = IsStrictPartialOrder.trans PA {isA B⊆A x} {isA B⊆A y} {isA B⊆A z} x<y y<z 
   irrefl1 : {x y : Element B} → elm x ≡ elm y → ¬ ( x <B y  )
   irrefl1 {x} {y} x=y x<y = IsStrictPartialOrder.irrefl PA {isA B⊆A x} {isA B⊆A y} x=y x<y 
   open import Data.Product
   resp0 : ({x y z : Element B} → elm y ≡ elm z → x <B y → x <B z) × ({x y z : Element B} → elm y ≡ elm z → y <B x → z <B x) 
   resp0 = Data.Product._,_  (λ {x} {y} {z} → proj₁ (IsStrictPartialOrder.<-resp-≈ PA) {isA B⊆A x } {isA B⊆A y }{isA B⊆A z }) 
                             (λ {x} {y} {z} → proj₂ (IsStrictPartialOrder.<-resp-≈ PA) {isA B⊆A x } {isA B⊆A y }{isA B⊆A z })

-- open import Relation.Binary.Properties.Poset as Poset

IsTotalOrderSet : ( A : HOD ) →  Set (suc n)
IsTotalOrderSet A = IsStrictTotalOrder  _≡A_ _<A_ where
   _<A_ : (x y : Element A ) → Set n
   x <A y = elm x < elm y
   _≡A_ : (x y : Element A ) → Set (suc n)
   x ≡A y = elm x ≡ elm y

me : { A a : HOD } → A ∋ a → Element A
me {A} {a} lt = record { elm = a ; is-elm = lt }

record SUP ( A B : HOD )  : Set (suc n) where
   field
      sup : HOD
      A∋maximal : A ∋ sup
      x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive

record Maximal ( A : HOD )  : Set (suc n) where
   field
      maximal : HOD
      A∋maximal : A ∋ maximal
      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative

record ZChain ( A : HOD ) (y : Ordinal)   : Set (suc n) where
   field
      max : HOD
      A∋max : A ∋ max
      y<max : y o< & max
      chain : HOD
      chain⊆A : chain ⊆ A  
      total : IsTotalOrderSet chain 
      chain-max : (x : HOD) → chain ∋ x → (x ≡ max ) ∨ ( x < max )

data IChain  (A : HOD) : Ordinal → Set n where
    ifirst : {ox : Ordinal} → odef A ox → IChain A ox
    inext  : {ox oy : Ordinal} → odef A oy → * ox < * oy → IChain A ox → IChain A oy

ic-connet :  {A : HOD} {x : Ordinal} → (x : IChain A x) → Ordinal →  Set n
ic-connet {A} (ifirst {ox} ax) oy = ox ≡ oy
ic-connet {A} (inext {ox} {oy} ay x<y iy) oz = (ox ≡ oz) ∨ ic-connet iy oz

IChainSet : {A : HOD} → Element A → HOD
IChainSet {A} ax = record { od = record { def = λ y → odef A y ∧ ( (iy : IChain A y ) → ic-connet iy (& (elm ax)))  }
    ; odmax = & A ; <odmax = λ {y} lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k) (sym &iso) (proj1 lt))) } 

-- there is a y, & y > & x

record Sup> {A : HOD} (x : Element A) : Set (suc n) where
   field
      y : Element A
      y>x : IChainSet x ∋ elm y → & (elm x) o< & (elm y)

-- finite IChain

record InFiniteIChain {A : HOD} (x : Element A) (z : Ordinal) : Set (suc n) where
   field
      ny : (y : Element A ) → & (elm y) o< z → Element A
      y>x : {y : Element A} → (lt : & (elm y) o< z )→ IChainSet x ∋ elm y → elm y < elm (ny y lt )
      
Zorn-lemma-case : { A : HOD } 
    → o∅ o< & A 
    → IsPartialOrderSet A 
    → (x : Element A) → Sup> x ∨ Dec ( InFiniteIChain x (& A))
Zorn-lemma-case {A}  0<A PO x = zc2 where
    Gtx : HOD
    Gtx = record { od = record { def = λ y → odef ( IChainSet x ) y ∧  ( & (elm x) o< y ) } ; odmax = & A
        ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k) (sym &iso) (proj1 (proj1 lt))))  }
    zc2 :  Sup> x ∨ Dec (InFiniteIChain x (& A))
    zc2 with  is-o∅ (& Gtx)
    ... | no not = case1 record { y = record { elm = ODC.minimal O Gtx (λ eq → not (=od∅→≡o∅ eq) ); is-elm = {!!} }  ; y>x = {!!} }
    ... | yes nogt = case2 {!!} where
        zc3 : {y : Element A} → IChainSet x ∋ elm y → ¬ (& (elm x) o< & (elm y))
        zc3 = {!!}
        zcind : (z : Ordinal ) → ((y : Ordinal) → y o< z → Dec (InFiniteIChain x y ) ) → Dec (InFiniteIChain x z)
        zcind z prev = {!!}
        zc4 : Dec (InFiniteIChain x (& A))
        zc4 = TransFinite zcind (& A)


Zorn-lemma : { A : HOD } 
    → o∅ o< & A 
    → IsPartialOrderSet A 
    → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
    → Maximal A 
Zorn-lemma {A}  0<A PO supP = zorn00 where
     someA : HOD
     someA = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 
     isSomeA : A ∋ someA
     isSomeA =  ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 
     HasMaximal : HOD
     HasMaximal = record { od = record { def = λ y → odef A y ∧ ((m : Ordinal) →  odef A m → ¬ (* y < * m))} ; odmax = & A ; <odmax = z08 } where
         z08 : {y : Ordinal} → (odef A y ∧ ((m : Ordinal) →  odef A m → ¬ (* y < * m)))  → y o< & A
         z08 {y} P = subst (λ k → k o< & A) &iso (c<→o< {* y} (subst (λ k → odef A k) (sym &iso) (proj1 P)))
     no-maximal : HasMaximal =h= od∅ → (y : Ordinal) →  (odef A y ∧ ((m : Ordinal) →  odef A m → ¬ (* y < * m))) →  ⊥
     no-maximal nomx y P = ¬x<0 (eq→ nomx {y} ⟪ proj1 P , (λ m am → (proj2 P) m am ) ⟫ ) 
     Gtx : { x : HOD} → A ∋ x → HOD
     Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = z09 }  where
         z09 : {y : Ordinal} → (odef A y ∧ (x < (* y)))  → y o< & A
         z09 {y} P = subst (λ k → k o< & A) &iso (c<→o< {* y} (subst (λ k → odef A k) (sym &iso) (proj1 P)))
     z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
     z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋a} (sym a=b) b<a
     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋b} refl (IsStrictPartialOrder.trans PO {me A∋b} {me A∋a} {me A∋b}  b<a a<b)
     -- ZChain is not compatible with the SUP condition
     record BX (x y : Ordinal) (fb : ( x : Ordinal ) → HOD ) : Set n where
        field
            bx : Ordinal
            bx<y : bx o< y
            is-fb : x ≡ & (fb bx )
     bx<A : (z : ZChain A (& A) ) → {x : Ordinal } → (bx : BX x (& A) {!!})  → BX.bx bx o< & A
     bx<A z {x} bx = BX.bx<y bx
     z12 : (z : ZChain A (& A) ) →  {y : Ordinal} → BX y (& A) {!!} → y o< & A
     z12 z {y} bx = subst (λ k → k o< & A) (sym (BX.is-fb bx)) (c<→o< {!!})  
     B :  (z : ZChain A (& A) ) → HOD
     B z = {!!}
     z11 :  (z : ZChain A (& A) ) → (x : Element (B z)) → elm x ≡  {!!} 
     z11 z x = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong (*) (BX.is-fb (is-elm x)) )
     obx : (z : ZChain A (& A) ) → {x : HOD} → B z ∋ x → Ordinal
     obx z {x} bx = BX.bx bx
     obx=fb : (z : ZChain A (& A) ) → {x : HOD} → (bx : B z ∋ x ) → x ≡ {!!}
     obx=fb z {x} bx = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (BX.is-fb bx)) 
     B⊆A : (z : ZChain A (& A) ) → B z ⊆ A
     B⊆A z = record { incl = λ {x} bx → subst (λ k → odef A k ) (sym (BX.is-fb bx)) {!!}  }
     -- PO-B : (z : ZChain A (& A) ) → IsPartialOrderSet (B z) _<_
     -- PO-B z = ⊆-IsPartialOrderSet (B⊆A z) PO
     bx-monotonic : (z : ZChain A (& A) ) → {x y : Element (B z)} → obx z (is-elm x) o< obx z (is-elm y) → elm x < elm y 
     bx-monotonic z {x} {y} a = subst₂ (λ j k → j < k ) (sym (z11 z x)) (sym (z11 z y)) {!!}  
     bcmp : (z : ZChain A (& A) ) → Trichotomous (λ (x : Element (B z)) y → elm x ≡ elm y ) (λ x y → elm x < elm y )
     bcmp z x y with trio< (obx z (is-elm x)) (obx z (is-elm y))
     ... | tri< a ¬b ¬c = tri< z15 (λ eq → z01 (incl (B⊆A z) (is-elm y)) (incl (B⊆A z) (is-elm x))(case1 (sym eq)) z15 ) z17 where
          z15 :  elm x < elm y
          z15 =  bx-monotonic z {x} {y} a
          z17 : elm y < elm x → ⊥
          z17 lt =  z01 (incl (B⊆A z) (is-elm y)) (incl (B⊆A z) (is-elm x))(case2 lt) z15 
     ... | tri≈ ¬a b ¬c = tri≈ (IsStrictPartialOrder.irrefl PO {isA (B⊆A z) x} {isA (B⊆A z) y} z14) z14 z16 where
          z14 :  elm x ≡ elm y
          z14 = {!!}
          z16 = IsStrictPartialOrder.irrefl PO {isA (B⊆A z) y} {isA (B⊆A z) x} (sym z14)
     ... | tri> ¬a ¬b c = tri> z17 (λ eq → z01 (incl (B⊆A z) (is-elm x)) (incl (B⊆A z) (is-elm y))(case1 eq) z15 ) z15 where
          z15 :  elm y < elm x
          z15 =  bx-monotonic z {y} {x} c
          z17 : elm x < elm y → ⊥
          z17 lt =  z01 (incl (B⊆A z) (is-elm x)) (incl (B⊆A z) (is-elm y))(case2 lt) z15 
     B-is-total :  (z : ZChain A (& A) ) → IsTotalOrderSet (B z) 
     B-is-total zc = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
         ; trans = λ {x} {y} {z} x<y y<z → IsStrictPartialOrder.trans PO {isA (B⊆A zc) x} {isA (B⊆A zc) y} {isA (B⊆A zc) z} x<y y<z
         ; compare = bcmp zc }
     ind : (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y ∨ Maximal A )
         →  ZChain A x ∨ Maximal A 
     --     has previous ordinal
     --        has maximal          use this
     --        else has chain
     --        & A < y              A is a counter example of assumption
     --          chack y is maximal 
     --          y < max              use previous chain
     --          y = max  (  y > max  cannot happen )
     --              ¬ A ∋ y           use previous chain
     --              A ∋ y is use oridinaly min of y or previous
     --     y is limit ordinal    
     --        has maximal in some lower   use this
     --        no maximal in all lower
     --          & A < y              A is a counter example of assumption
     --          A ∋ y is maximal      use this            
     --          ¬ A ∋ y           use previous chain
     --          check some y ≤ max 
     --              if none A < y is the counter example
     --              else use the ordinaly smallest max as next chain
     ind x prev with Oprev-p x
     ... | yes op with ODC.∋-p O A (* x)
     ... | no ¬Ax = zc1 where
          -- we have previous ordinal and ¬ A ∋ x, use previous Zchain
          px = Oprev.oprev op
          zc1 : ZChain A x ∨ Maximal A
          zc1 with prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
          ... | case2 x = case2 x  -- we have the Maximal
          ... | case1 z with trio< x (& (ZChain.max z))
          ... | tri< a ¬b ¬c = case1 record { max = ZChain.max z ; y<max = a }
          ... | tri≈ ¬a b ¬c = {!!} -- x = max so ¬ A ∋ max 
          ... | tri> ¬a ¬b c = {!!} -- can't happen
     ... | yes ax = zc1 where -- we have previous ordinal and A ∋ x
          px = Oprev.oprev op
          zc1 : ZChain A x ∨ Maximal A
          zc1 with  prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
          ... | case2 x = case2 x
          ... | case1 x with is-o∅ ( & (Gtx ax ))
          ... | yes no-sup = case2 {!!}
          ... | no sup = case1 {!!}
     ind x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
     ... | tri< a ¬b ¬c = {!!} where
          zc1 : ZChain A (& A) 
          zc1 with prev (& A) a 
          ... | t = {!!}
     ... | tri≈ ¬a b ¬c = {!!} where
     ... | tri> ¬a ¬b c with ODC.∋-p O A (* x)
     ... | no ¬Ax = {!!} where
     ... | yes ax with is-o∅ (& (Gtx ax))
     ... | yes nogt = ⊥-elim {!!} where -- no larger element, so it is maximal
              x-is-maximal :  (m : Ordinal) → odef A m → ¬ (* x < * m)
              x-is-maximal m am  =  ¬x<m   where
                 ¬x<m :  ¬ (* x < * m)
                 ¬x<m x<m = ∅< {Gtx ax} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫  (≡o∅→=od∅ nogt) 
     ... | no not = {!!} where
     zorn03 : (x : Ordinal) → ZChain A x  ∨ Maximal A 
     zorn03 x with TransFinite ind  x
     ... | t = {!!}
     zorn04 : Maximal A 
     zorn04 with zorn03 (& A)
     ... | case1 chain = {!!}
     ... | case2 m = m
     zorn00 : Maximal A 
     zorn00 with is-o∅ ( & HasMaximal )
     ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where
         -- yes we have the maximal
         hasm :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
         hasm =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))
         zorn01 :  A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))
         zorn01 =  proj1 hasm
         zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
         zorn02 {x} ax m<x = ((proj2 hasm) (& x) ax) (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
     ... | yes ¬Maximal = {!!} where
         -- if we have no maximal, make ZChain, which contradict SUP condition
         z : (x : Ordinal) → HasMaximal =h= od∅  → ZChain A x  ∨ Maximal A 
         z x nomx with TransFinite {!!} x
         ... | t = {!!}

-- _⊆'_ : ( A B : HOD ) → Set n
-- _⊆'_ A B = (x : Ordinal ) → odef A x → odef B x

-- MaximumSubset : {L P : HOD} 
--        → o∅ o< & L →  o∅ o< & P → P ⊆ L
--        → IsPartialOrderSet P _⊆'_
--        → ( (B : HOD) → B ⊆ P → IsTotalOrderSet B _⊆'_ → SUP P B _⊆'_ )
--        → Maximal P (_⊆'_)
-- MaximumSubset {L} {P} 0<L 0<P P⊆L PO SP  = Zorn-lemma {P} {_⊆'_} 0<P PO SP