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

changeset 784:d83b0f7ece32

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, 01 Aug 2022 10:46:21 +0900
parents 195c3c7de021
children 7472e3dc002b
files src/zorn.agda
diffstat 1 files changed, 9 insertions(+), 91 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Aug 01 10:37:39 2022 +0900
+++ b/src/zorn.agda	Mon Aug 01 10:46:21 2022 +0900
@@ -265,8 +265,6 @@
       sup : HOD
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
-      min-sup : {z : HOD } → B ∋ z → ( {x : HOD } → B ∋ x → (x ≡ z ) ∨ (x < z ) ) 
-          → (z ≡ sup ) ∨ (sup < z )  
 
 --
 --  sup and its fclosure is in a chain HOD
@@ -313,27 +311,21 @@
       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 : (z : Ordinal ) → odef chain (supf z) 
-      csupf' : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
-      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 
-      order : {b sup1 z1 : Ordinal} → b o< z → supf sup1 o< supf b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-   supf∈A : {u : Ordinal } → odef A (supf u)
-   supf∈A = ?
-   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)  , ? ⟫ 
+   csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
+   csupf = ?
+   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 = ?
-   fc∈A : {s z1 : Ordinal} → FClosure A f (supf s) z1 → odef chain z1
-   fc∈A {s} (fsuc x fc) = f-next (fc∈A {s} fc )  -- (supf s) ≡ z1 → init (supf s)
-   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 : 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
+   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 
+        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 ? ? ⟫
 
@@ -351,26 +343,6 @@
       A∋maximal : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
--- 
-
-supf-unique : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)  
-        → {a b : Ordinal } → a o< b
-        → (za : ZChain A f mf ay (osuc a) ) → (zb : ZChain A f mf ay (osuc b) )
-        → odef (UnionCF A f mf ay (ZChain.supf za) (osuc a)) (ZChain.supf za a) 
-        → odef (UnionCF A f mf ay (ZChain.supf zb) (osuc b)) (ZChain.supf zb a) → ZChain.supf za a ≡ ZChain.supf zb a 
-supf-unique A f mf {y} ay {a} {b} a<b za zb ⟪ aa , ch-init fca ⟫ ⟪ ab , ch-init fcb ⟫ = ? where
-       supf = ZChain.supf za
-       supb = ZChain.supf zb
-       su00 :  {u w : Ordinal } → u o< osuc a  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) 
-       su00 = ZChain.fcy<sup za
-       su01 :  (supf a ≡ supb b ) ∨ ( supf a << supb b ) 
-       su01 = ZChain.fcy<sup zb <-osuc fca
-       su02 :  (supb a ≡ supf a ) ∨ ( supb a << supf a ) 
-       su02 = ZChain.fcy<sup za <-osuc fcb
-supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-init fca ⟫ ⟪ ab , ch-is-sup ub is-supb fcb ⟫ = ?
-supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-is-sup ua is-supa fca ⟫ ⟪ ab , ch-init fcb ⟫ = ?
-supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-is-sup ua is-supa fca ⟫ ⟪ ab , ch-is-sup ub is-supb fcb ⟫ = ?
-
 -- data UChain is total
 
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
@@ -758,11 +730,6 @@
 
           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 is-sup fc ⟫ = ⟪ az , ch-is-sup u is-sup fc ⟫ 
-
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extension : ZChain A f mf ay x
@@ -830,55 +797,6 @@
               ... | tri≈ ¬a b ¬c | record { eq = eq1 } = subst (λ k → spu ≡ psupf k) b (sym eq1)
               ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬b z=x)
 
-          order :  {b sup1 z1 : Ordinal} → b o< x →
-            psupf sup1 o< psupf b →
-            FClosure A f (psupf sup1) z1 → (z1 ≡ psupf b) ∨ (z1 << psupf b)
-          order {b} {s} {z1}  b<x ps<pb fc with trio< b x
-          ... | tri< a ¬b ¬c = ZChain.order uzc <-osuc zc21 zc20 where
-               uzc = pzc (osuc b) (ob<x lim a)
-               zc22 : psupf s ≡ ZChain.supf uzc s 
-               zc22 with trio< s x
-               ... | tri< s<x ¬b ¬c = zc23 where
-                   szc = pzc (osuc s) (ob<x lim s<x)
-                   zc23 :  ZChain.supf (pzc (osuc s) (ob<x lim s<x)) s ≡ ZChain.supf (pzc (osuc b) (ob<x lim a)) s
-                   zc23 = ?
-                   zc24 : odef (UnionCF A f mf ay (ZChain.supf (pzc (osuc s) (ob<x lim s<x))) (osuc s)) 
-                                (ZChain.supf (pzc (osuc s) (ob<x lim s<x)) s )
-                   zc24 = ZChain.csupf (pzc (osuc s) (ob<x lim s<x)) s
-                   zc25 : odef (UnionCF A f mf ay (ZChain.supf (pzc (osuc b) (ob<x lim a))) (osuc b)) 
-                                (ZChain.supf (pzc (osuc b) (ob<x lim a)) b )
-                   zc25 = ZChain.csupf (pzc (osuc b) (ob<x lim a)) b
-
-               ... | tri≈ ¬a b ¬c = ?
-               ... | tri> ¬a ¬b c = ?
-               zc21 :  ZChain.supf uzc s o< ZChain.supf uzc b
-               zc21 = subst (λ k → k o< _) zc22 ps<pb
-               zc20 : FClosure A f (ZChain.supf uzc s ) z1
-               zc20 = subst (λ k → FClosure A f k z1) zc22 fc
-          ... | tri≈ ¬a b ¬c = ⊥-elim (¬a b<x)
-          ... | tri> ¬a ¬b c = ⊥-elim (¬a b<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 z
-                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 = order z<x  }
-                     ---  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 
@@ -919,7 +837,7 @@
                           (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 = {!!} ; order = order ; fcy<sup = fcy<sup
+          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; sup=u = {!!} 
               ; supf-mono = {!!} ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)