Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 785:7472e3dc002b

order done

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 01 Aug 2022 18:51:27 +0900
parents	d83b0f7ece32
children	1db222b676d8

comparison

equal deleted inserted replaced

-:d83b0f7ece32
+:7472e3dc002b
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where
 field
 fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u )
 order    : {sup1 z1 : Ordinal} → (lt : supf sup1 o< supf u ) → FClosure A f (supf sup1 ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
+ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
+→ {x z : Ordinal } →  ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
+ChainP-next A f mf {y} ay supf {x} {z} cp = record {  fcy<sup = ChainP.fcy<sup cp ; order = ChainP.order cp }
 -- Union of supf z which o< x
 --
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
 (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where
 f-total : IsTotalOrderSet chain
 sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
 sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b
 csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b)
-csupf = ?
+supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
 fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
-fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  , ? ⟫
+fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)
-... | case1 eq = ?
+, ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
-... | case2 lt = ?
+... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
+... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
 order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-order {b} {s} {.(f x)} b<z sf<sb (fsuc x fc) with proj1 (mf x (A∋fc _ f mf fc)) | order b<z sf<sb fc
+order {b} {s} {z1} b<z sf<sb fc = zc04 where
-... | case1 eq | t = ?
+zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
-... | case2 lt | t = ?
+zc01  (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03  where
-order {b} {s} {z1} b<z sf<sb (init x refl) = ? where
+s<z : s o< z
-zc01 : s o≤ z
+s<z with trio< s z
-zc01 = ?
+... | tri< a ¬b ¬c = a
-zc00 : ( * (supf s)  ≡  SUP.sup (sup (o<→≤ b<z ))) ∨ ( * (supf s)  < SUP.sup ( sup (o<→≤ b<z )) )
+... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (cong supf b)  (ordtrans<-≤ sf<sb (supf-mono b<z)  ))
-zc00 with csupf zc01
+... | tri> ¬a ¬b c with osuc-≡< ( supf-mono c )
-... | ⟪ ss , ch-init fc ⟫ = SUP.x<sup (sup (o<→≤ b<z)) ⟪ ? , ch-init ? ⟫
+... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) (ordtrans<-≤ sf<sb (supf-mono b<z)  ))
-... | ⟪ ss , ch-is-sup us is-sup fc  ⟫ = SUP.x<sup (sup (o<→≤ b<z)) ⟪ ? , ch-is-sup us ? ? ⟫
+... | case2 lt = ⊥-elim ( o<> lt (ordtrans<-≤ sf<sb (supf-mono b<z)  ))
+zc03 : odef (UnionCF A f mf ay supf b)  (supf s)
+zc03 with csupf (o<→≤ s<z)
+... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫
+... | ⟪ as , ch-is-sup u is-sup fc ⟫ = ⟪ as , ch-is-sup u is-sup fc ⟫
+zc01  (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
+zc04 : odef (UnionCF A f mf ay supf b) (f x)
+zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc  )
+... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫
+... | ⟪ as , ch-is-sup u is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) ⟫
+zc00 : ( * z1  ≡  SUP.sup (sup (o<→≤ b<z ))) ∨ ( * z1  < SUP.sup ( sup (o<→≤ b<z )) )
+zc00 = SUP.x<sup (sup (o<→≤ b<z)) (zc01 fc )
+zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
+zc04 with zc00
+... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup (o<→≤ b<z )) ) (cong (&) eq) )
+... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup (o<→≤ b<z )) )))  lt )
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
 {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
 field
 ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
 init-uchain : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y )
 { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y
 init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl)   ⟫
-ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
-→ {x z : Ordinal } →  ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
-ChainP-next A f mf {y} ay supf {x} {z} cp = record {  fcy<sup = ChainP.fcy<sup cp ; order = ChainP.order cp }
 Zorn-lemma : { A : HOD }
 → o∅ o< & A
 → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
 → Maximal A
 →  SUP A (uchain f mf ay)
 ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay)
 inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
 inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy
-; csupf = λ z → csupf z ; fcy<sup = λ u<0 → ⊥-elim ( ¬x<0 u<0 ) ; supf-mono = λ _ → o≤-refl
+; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) } where
-; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
 spi =  & (SUP.sup (ysup f mf ay))
 isupf : Ordinal → Ordinal
 isupf z = spi
 sp = ysup f mf ay
 asi = SUP.A∋maximal sp
 zc20 {z} z=x with trio< z x | inspect psupf z
 ... | tri< a ¬b ¬c | _ = ⊥-elim ( ¬b z=x)
 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = subst (λ k → spu ≡ psupf k) b (sym eq1)
 ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬b z=x)
+csupf : (z : Ordinal) → odef (UnionCF A f mf ay psupf x) (psupf z)
+csupf z with trio< z x | inspect psupf z
+... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where
+ozc = pzc (osuc z) (ob<x lim z<x)
+zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
+zc12  = ? -- ZChain.csupf ozc ?
+zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
+zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az refl) ) ⟫ where
+az : odef A ( ZChain.supf ozc z )
+az = proj1 zc12
+zc20 : {z1  : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
+zc20 {z1} fc with ZChain.fcy<sup ozc <-osuc fc
+... | case1 eq = case1 (trans eq (sym eq1) )
+... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
+cp1 : ChainP A f mf ay psupf z (ZChain.supf ozc z)
+cp1 = record {  fcy<sup = zc20   ; order = ? }
+---  u = supf u = supf z
+... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup {!!} {!!} {!!} ⟫ where
+sa = SUP.A∋maximal usup
+... | tri> ¬a ¬b c | record { eq = eq1 } = {!!}
 fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ psupf u) ∨ (w << psupf u)
 fcy<sup {u} {w} u<x fc with trio< u x
 ... | tri< a ¬b ¬c = ZChain.fcy<sup uzc <-osuc fc where
 uzc = pzc (osuc u) (ob<x lim a)
 subst (λ k → UChain A f mf ay supf x k )
 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫
 no-extension : ZChain A f mf ay x
 no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; sup=u = {!!}
-; supf-mono = {!!} ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
+; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 zc5 : ZChain A f mf ay x
 zc5 with ODC.∋-p O A (* x)
 ... | no noax = no-extension -- ¬ A ∋ p, just skip
 ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )
 -- we have to check adding x preserve is-max ZChain A y f mf x
 ... | case1 pr = no-extension
 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; csupf = {!!} ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!}
+... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; sup=u = {!!}
-; supf-mono = {!!} ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} } where -- x is a sup of (zc ?)
+;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} } where -- x is a sup of (zc ?)
 psupf1 : Ordinal → Ordinal
 psupf1 z with trio< z x
 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
 ... | tri≈ ¬a b ¬c = x
 ... | tri> ¬a ¬b c = x

Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/zorn.agda @ 785:7472e3dc002b