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

changeset 754:db177d911091

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 Sat, 23 Jul 2022 18:40:35 +0900
parents b96491f7c775
children b22327e78b03
files src/zorn.agda
diffstat 1 files changed, 31 insertions(+), 30 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Jul 22 16:52:17 2022 +0900
+++ b/src/zorn.agda	Sat Jul 23 18:40:35 2022 +0900
@@ -293,8 +293,7 @@
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
-      sup=u : {b : Ordinal} → {ab : odef A b} → b o< z → IsSup A chain ab → supf b ≡ b 
-      order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → z1 << supf b
+      csupf : {z : Ordinal } → odef chain (supf z) 
 
 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
@@ -453,6 +452,8 @@
            px = Oprev.oprev op
            zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
            zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
+           fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u
+           fcy<sup {u} {w} u<x fc = ?
            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 →
@@ -577,7 +578,7 @@
           c = & (SUP.sup sp1)
 
      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
+     inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = ?
       ; 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
           isupf : Ordinal → Ordinal
           isupf z = y
@@ -641,31 +642,19 @@
           pcy : odef pchain y
           pcy = ⟪ ay , ch-init (init ay)    ⟫
 
-          supf0 = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))
+          supf0 = ZChain.supf zc
+
+          csupf : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) (supf0 z)
+          csupf {z} with ZChain.csupf zc {z}
+          ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+          ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u (ordtrans u<px px<x ) is-sup fc ⟫ 
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extension : ZChain A f mf ay x
           no-extension = record { supf = supf0
-               ; initial = pinit ; chain∋init = pcy  ; sup=u = sup=u 
-              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ;  order = order } where
-              sup=u :  {b : Ordinal} {ab : odef A b} → b o< x 
-                    → IsSup A (UnionCF A f mf ay supf0 x) ab 
-                    → supf0 b ≡ b
-              sup=u {b} {ab} b<x is-sup with trio< b px
-              ... | tri< a ¬b ¬c = ZChain.sup=u zc {b} {ab} a record { x<sup = pc20 } where
-                     pc20 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b)
-                     pc20 {z} ⟪ az , ch-init fc  ⟫ = 
-                         IsSup.x<sup is-sup ⟪ az ,  ch-init fc  ⟫ 
-                     pc20 {z} ⟪ az , ch-is-sup u u<x is-sup-c fc  ⟫ = IsSup.x<sup is-sup 
-                         ⟪ az , ch-is-sup u (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc)) is-sup-c fc  ⟫ 
-              ... | tri≈ ¬a refl ¬c = ?
-              ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
-              order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b → FClosure A f (supf0 sup1) z1 → z1 << supf0 b
-              order {b} {s} {z1} b<x s<b fc with trio< b px 
-              ... | tri< a ¬b ¬c = ZChain.order zc a s<b fc
-              ... | tri≈ ¬a refl ¬c = ?
-              ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
+               ; initial = pinit ; chain∋init = pcy  ; csupf = csupf
+              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } 
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* px)
@@ -675,8 +664,8 @@
           ... | 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 {  supf = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ?
-                     ; initial = ? ; chain∋init  = ? ; sup=u = ? ; order = ? }  where
+                record {  supf = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ? ; csupf = ?
+                     ; initial = ? ; chain∋init  = ? }  where
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x 
              ... | tri< a ¬b ¬c = ZChain.supf zc z
@@ -723,10 +712,6 @@
           pcy : odef pchain y
           pcy = ⟪ ay , ch-init (init ay)    ⟫
 
-          no-extension : ZChain A f mf ay x
-          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf0 
-              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; sup=u = ? ; order = ? }
-
           usup : SUP A pchain
           usup = supP pchain (λ lt → proj1 lt) ptotal
           spu = & (SUP.sup usup)
@@ -736,6 +721,22 @@
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
 
+
+          csupf :{z : Ordinal} → odef (UnionCF A f mf ay psupf x) (psupf z)
+          csupf {z} with trio< z x
+          ... | tri< a ¬b ¬c = zc11 where
+                zc11 : odef A (ZChain.supf (pzc z a) z) ∧ UChain A f mf ay psupf x (ZChain.supf (pzc z a) z)
+                zc11 with  ZChain.csupf (pzc z a) {z}
+                ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                ... | ⟪ az , ch-is-sup u u<z is-sup fc ⟫ = ⟪ az , ch-is-sup u (ordtrans u<z a)  ? (pfc a fc)  ⟫ 
+          ... | tri≈ ¬a b ¬c = ?
+          ... | tri> ¬a ¬b c = ?
+
+          no-extension : ZChain A f mf ay x
+          no-extension  = record { initial = ? ; chain∋init = ?  ; supf = psupf  ; csupf = ?
+              ;  chain⊆A = ? ;  f-next = ? ;  f-total = ? }
+
+
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extension -- ¬ A ∋ p, just skip
@@ -743,7 +744,7 @@
                -- 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  ; sup=u = ? ; order = ?
+          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; csupf = ?
               ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = ? } where -- x is a sup of (zc ?) 
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x