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

changeset 785:7472e3dc002b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
order done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Aug 2022 18:51:27 +0900
parents d83b0f7ece32
children 1db222b676d8
files src/zorn.agda
diffstat 1 files changed, 59 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Aug 01 10:46:21 2022 +0900
+++ b/src/zorn.agda	Mon Aug 01 18:51:27 2022 +0900
@@ -278,6 +278,10 @@
       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
 --
 
@@ -311,23 +315,39 @@
       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 = ?
+      csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
+      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)  , ? ⟫ 
-   ... | case1 eq = ?
-   ... | case2 lt = ?
+   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)  
+       , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
+   ... | 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
-   ... | case1 eq | t = ?
-   ... | case2 lt | t = ?
-   order {b} {s} {z1} b<z sf<sb (init x refl) = ? where
-        zc01 : s o≤ z
-        zc01 = ?
-        zc00 : ( * (supf s)  ≡  SUP.sup (sup (o<→≤ b<z ))) ∨ ( * (supf s)  < SUP.sup ( sup (o<→≤ b<z )) )
-        zc00 with csupf zc01 
-        ... | ⟪ ss , ch-init fc ⟫ = SUP.x<sup (sup (o<→≤ b<z)) ⟪ ? , ch-init ? ⟫
-        ... | ⟪ ss , ch-is-sup us is-sup fc  ⟫ = SUP.x<sup (sup (o<→≤ b<z)) ⟪ ? , ch-is-sup us ? ? ⟫
+   order {b} {s} {z1} b<z sf<sb fc = zc04 where
+        zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
+        zc01  (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03  where
+            s<z : s o< z
+            s<z with trio< s z
+            ... | tri< a ¬b ¬c = a
+            ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (cong supf b)  (ordtrans<-≤ sf<sb (supf-mono b<z)  ))
+            ... | tri> ¬a ¬b c with osuc-≡< ( supf-mono c )
+            ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) (ordtrans<-≤ sf<sb (supf-mono b<z)  ))
+            ... | 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) 
@@ -418,10 +438,6 @@
     { 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
@@ -650,8 +666,7 @@
 
      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) ; order = λ 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) } where
           spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
           isupf z = spi
@@ -797,6 +812,26 @@
               ... | 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 
@@ -838,7 +873,7 @@
 
           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
@@ -846,8 +881,8 @@
                -- 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 = {!!}
-              ; supf-mono = {!!} ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} } where -- x is a sup of (zc ?) 
+          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; sup=u = {!!} 
+              ;  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