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

changeset 728:e864471a818f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 18 Jul 2022 21:50:17 +0900
parents 322dd6569072
children ac6b4d200f27
files src/zorn.agda
diffstat 1 files changed, 56 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jul 18 16:26:01 2022 +0900
+++ b/src/zorn.agda	Mon Jul 18 21:50:17 2022 +0900
@@ -295,12 +295,23 @@
    chain : HOD
    chain = UnionCF A f mf ay supf z
    field
+      chain-mono : {z1 : Ordinal} → z1 o≤ z → UnionCF A f mf ay supf z1 ⊆' UnionCF A f mf ay supf z 
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
 
+record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
+        {init : Ordinal} (ay : odef A init)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
+   field
+      b<x→chain : { b : Ordinal } → b o< z → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) b → odef (UnionCF A f mf ay (ZChain.supf zc) z) b
+      chain-mono2 : { a b c : Ordinal }  → 
+          a o≤ b → b o≤ z → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
+      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) z) a ) →  b o< z  → (ab : odef A b) 
+          → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) z) ab f ∨  IsSup A (UnionCF A f mf ay (ZChain.supf zc) z) ab  
+          → * a < * b  → odef ((UnionCF A f mf ay (ZChain.supf zc) z)) b
+
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
@@ -347,7 +358,7 @@
 
 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 { y-init = ChainP.y-init cp ; asup = ChainP.asup cp  ; au = ChainP.au cp
+ChainP-next A f mf {y} ay supf {x} {z} cp = {!!} --record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp  ; au = ChainP.au cp
      -- ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
 
 Zorn-lemma : { A : HOD } 
@@ -410,14 +421,35 @@
      zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
      zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
 
-     ZChain-is-max :( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
-        {init : Ordinal} (ay : odef A init)   (zc : ZChain A f mf ay (& A)) → 
-         {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) a ) →  b o< & A  → (ab : odef A b) 
-          → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) (& A)) ab f ∨  IsSup A (UnionCF A f mf ay (ZChain.supf zc) (& A)) ab  
-          → * a < * b  → odef ((UnionCF A f mf ay (ZChain.supf zc) (& A))) b
-     ZChain-is-max A f mf {y} ay zc {a} {b} ca b<a ab (case1 has-prev) a<b = 
-          subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) k ) (sym (HasPrev.x=fy has-prev)) ( ZChain.f-next zc (HasPrev.ay has-prev) )
-     ZChain-is-max A f mf {y} ay zc {a} {b} ca b<a ab (case2 is-sup) a<b = ?
+     SZ1 :( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
+        {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
+     SZ1 A f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
+        zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
+        zc1 x prev = {!!} where
+           is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
+              b o< x → (ab : odef A b) →
+              HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
+              * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
+           is-max {a} {b} ua b<x ab (case1 has-prev) a<b = {!!}
+           is-max {a} {b} ua b<x ab (case2 is-sup) a<b with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ab f )
+           ... | case1 has-prev = m03 (subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) k ) {!!} m02 ) {!!} where
+                 m03 : odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) b → b o< x → odef (UnionCF A f mf ay (ZChain.supf zc) x) b 
+                 m03 = {!!}
+                 m02 : odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) (f (HasPrev.y has-prev))
+                 m02 = ZChain.f-next zc (HasPrev.ay has-prev) 
+           ... | case2  ¬fy<x  with Oprev-p x
+           ... | yes op = {!!} where
+                 px = Oprev.oprev op
+                 m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
+                 m01 with trio< px b
+                 ... | tri< a ¬b ¬c = ZChain1.chain-mono2 (prev px ?) ? ? m04 where
+                    m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
+                    m04 = ZChain1.is-max (prev px ?) {!!} {!!} ab {!!} a<b
+                 ... | tri≈ ¬a b ¬c = {!!}
+                 ... | tri> ¬a ¬b c = {!!}
+           ... | no  lim = ZChain1.chain-mono2 (prev b b<x ) ? {!!} m04  where
+                    m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
+                    m04 = ZChain1.is-max (prev (osuc b) ? ) {!!} {!!} ab {!!} a<b
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -431,7 +463,7 @@
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) 
               →  HasPrev A chain ab f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
               → * a < * b  → odef chain b
-           z10 = ZChain-is-max A f mf as0 zc
+           z10 = ZChain1.is-max (SZ1 A f mf as0 zc (& A) )
            z11 : & (SUP.sup sp1) o< & A
            z11 = c<→o< ( SUP.A∋maximal sp1)
            z12 : odef chain (& (SUP.sup sp1))
@@ -484,7 +516,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
-      ; initial = isy ; f-next = inext ; f-total = itotal ; is-max = imax } where
+      ; initial = isy ; f-next = inext ; f-total = itotal ; chain-mono = {!!} } where
           isupf : Ordinal → Ordinal
           isupf z = y
           cy : odef (UnionCF A f mf ay isupf o∅) y
@@ -508,11 +540,6 @@
           imax {a} {b} ua b<x ab (case1 hasp) a<b = subst (λ k → odef  (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
           imax {a} {b} ua b<x ab (case2 sup)  a<b = ⊥-elim ( ¬x<0 b<x )
 
-     -- exor-sup : (B : HOD) 
-     --    → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → 
-     --    → {x : Ordinal } (xa : odef A x) → HasPrev A B xa → IsSup A B xa → ⊥
-     -- exor-sup B f mf {y} ay {x} xa hasp is-sup with trio< 
-
      --
      -- create all ZChains under o< x
      --
@@ -560,7 +587,7 @@
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extension : ZChain A f mf ay x
-          no-extension = record { initial = pinit ; chain∋init = pcy 
+          no-extension = record { supf = {!!} ; initial = pinit ; chain∋init = pcy 
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 
           chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain
@@ -594,10 +621,10 @@
           ... | case1 pr = no-extension -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
+                record {  supf = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
                      ; initial = pinit ; chain∋init  = pcy } 
           ... | case2 ¬x=sup =  no-extension -- px is not f y' nor sup of former ZChain from y -- no extention
-     ... | no op = zc5 where
+     ... | no lim = zc5 where
 
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
           pzc z z<x = prev z z<x
@@ -643,7 +670,7 @@
           pcy = ⟪ ay , record { u =  o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
 
           no-extension : ZChain A f mf ay x
-          no-extension  = record { initial = pinit ; chain∋init = pcy 
+          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf0 ; chain-mono = ?
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 
           usup : SUP A pchain
@@ -655,18 +682,14 @@
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
 
-          uzc : {a : Ordinal } → (za : odef pchain a) → ZChain A f mf ay (UChain.u (proj2 za))
-          uzc {a} za with UChain.u<x (proj2 za)
-          ... | case1 u<x = pzc _ u<x
-          ... | case2 u=0 =  subst (λ k → ZChain A f mf ay k ) (sym u=0) (inititalChain f mf {y} ay )
 
           chain-mono : pchain ⊆'  UnionCF A f mf ay psupf x  
           chain-mono {a} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ = 
                    ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ 
           chain-mono {.(psupf0 u)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (init x) } ⟫ = 
-                   ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup ? ? } ⟫ 
+                   ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup {!!} {!!} } ⟫ 
           chain-mono {.(f x)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (fsuc x fc) } ⟫ = 
-                   ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup ? (fsuc x ?) } ⟫ 
+                   ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup {!!} (fsuc x {!!}) } ⟫ 
           
           chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain 
              → UnionCF A f mf ay psupf x ≡ pchain 
@@ -679,19 +702,6 @@
           fc-conv {.(p0 u)} {u}  {p0} {p1} p0u=p1u (init ap0u) = subst (λ k → FClosure A f (p1 u) k) (sym p0u=p1u) ( init (subst (λ k → odef A k) p0u=p1u ap0u ))
           fc-conv {_} {u}  {p0} {p1} p0u=p1u (fsuc z fc) = fsuc z (fc-conv {_} {u}  {p0} {p1} p0u=p1u fc)
 
-          uzc-mono : {b : Ordinal } → {ob<x : osuc b o< x }
-             → odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b → odef pchain b
-          uzc-mono {b} {ob<x} ⟪ ab , record { u = x=0 ; u<x = u<x ; uchain = ch-init .b fc } ⟫ = 
-               ⟪ ab , record { u = x=0 ; u<x = case2 refl ; uchain = ch-init b fc } ⟫ 
-          uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case2 x=0 ; uchain = ch-is-sup is-sup fc } ⟫ = ?
-          uzc-mono {b} {ob<x} ⟪ ab , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 
-               ⟪ ab , record { u = u ; u<x = case1 (ordtrans u<x ob<x) ; uchain = ch-is-sup uzc00 
-                       (fc-conv {b} {u} {ZChain.supf (prev (osuc b) ob<x)} {psupf0} uzc01 fc) } ⟫ where
-                   uzc01 : ZChain.supf (prev (osuc b) ob<x) u  ≡ psupf0 u
-                   uzc01 = ? -- trans (sym (psupf0=pzc (ordtrans u<x ob<x ) )) ?
-                   uzc00 : ChainP A f mf ay psupf0 u b
-                   uzc00 = ?
-
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extension where -- ¬ A ∋ p, just skip
@@ -699,7 +709,13 @@
                -- 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 = {!!} -- x is a sup of (zc ?) 
+          ... | case1 is-sup = record { initial = ? ; chain∋init = ?  ; supf = psupf1  ; chain-mono = ?
+              ;  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
           ... | case2 ¬x=sup =  no-extension -- x is not f y' nor sup of former ZChain from y -- no extention
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)