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

changeset 1028:d1eecfc6cdfa

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 Sun, 27 Nov 2022 20:19:18 +0900
parents 91988ae176ab
children 07ffcf16a3d4
files src/zorn.agda
diffstat 1 files changed, 47 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Nov 26 16:34:38 2022 +0900
+++ b/src/zorn.agda	Sun Nov 27 20:19:18 2022 +0900
@@ -383,6 +383,13 @@
 UnionCF A f mf ay supf x
    = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
+UnionCF' : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
+    ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
+UnionCF' A f mf ay supf x
+   = record { od = record { def = λ z → odef A z ∧ ( { s : Ordinal} → s o< x → FClosure A f (supf s) z ) } ;   
+       odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+
+
 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
    → supf x o< supf y → x o<  y
 supf-inject0 {x} {y} {supf} supf-mono sx<sy with trio< x y
@@ -428,13 +435,14 @@
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf :  Ordinal → Ordinal
+
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
            → IsSUP A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b
       cfcs : (mf< : <-monotonic-f A f)
          {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f mf ay supf b) w
+      order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y
 
       asupf :  {x : Ordinal } → odef A (supf x)
-      supf-<= : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 
@@ -624,6 +632,18 @@
                         z55 : FClosure A f (ZChain.supf zb u) z
                         z55 = subst (λ k → FClosure A f k z ) (sym ub=ua) fc
 
+UChain-eq : { A : HOD }    { f : Ordinal → Ordinal }  {mf : ≤-monotonic-f A f}
+        {z y : Ordinal} {ay : odef A y}  { supf0 supf1 : Ordinal → Ordinal }
+        → (seq : {x : Ordinal } →  x o<  z  → supf0 x ≡ supf1 x )
+        → UnionCF A f mf ay supf0 z ≡ UnionCF A f mf ay supf1 z
+UChain-eq {A} {f} {mf} {z} {y} {ay} {supf0} {supf1} seq = ==→o≡  record { eq← = ueq← ; eq→ = ueq→ } where
+      ueq← :  {x : Ordinal} → odef A x ∧ UChain A f mf ay supf1 z x → odef A x ∧ UChain A f mf ay supf0 z x
+      ueq← {z} ⟪ ab , ch-init fc ⟫ = ⟪ ab , ch-init fc ⟫
+      ueq← {z} ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , ch-is-sup u u<x ? ? ⟫ 
+      ueq→  : {x : Ordinal} → odef A x ∧ UChain A f mf ay supf0 z x → odef A x ∧ UChain A f mf ay supf1 z x
+      ueq→ {z} ⟪ ab , ch-init fc ⟫ = ⟪ ab , ch-init fc ⟫
+      ueq→ {z} ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , ch-is-sup u u<x ? ? ⟫ 
+
 Zorn-lemma : { A : HOD }
     → o∅ o< & A
     → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
@@ -845,11 +865,6 @@
      SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B
      SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x≤sup = λ lt → SUP.x≤sup sup (B⊆C lt)    }
 
-     record xSUP (B : HOD) (f : Ordinal → Ordinal ) (x : Ordinal) : Set n where
-        field
-           ax : odef A x
-           is-sup : IsMinSUP A B f ax
-
      zc43 : (x sp1 : Ordinal ) → ( x o< sp1 ) ∨ ( sp1 o≤ x )
      zc43 x sp1 with trio< x sp1
      ... | tri< a ¬b ¬c = case1 a
@@ -958,7 +973,7 @@
 
           zc41 : ZChain A f mf ay x
           zc41 with zc43 x sp1
-          zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf1-mono 
+          zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf1-mono ; order = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs  }  where
 
                  supf1 : Ordinal → Ordinal
@@ -1227,7 +1242,8 @@
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where
                     m = ZChain.minsup zc (o<→≤ a)
                     ms00 :  {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
-                    ms00 {x} ux = MinSUP.x≤sup m ?
+                    ms00 {w} ⟪ az , ch-init fc ⟫ = MinSUP.x≤sup m ?
+                    ms00 {w} ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = MinSUP.x≤sup m ⟪ az , ch-is-sup u ? ? ? ⟫ 
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
                         odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m us ?
@@ -1249,7 +1265,7 @@
                     ms01 {sup2} us P = MinSUP.minsup m us ?
 
 
-          zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ZChain.asupf zc ; supf-mono = ZChain.supf-mono zc 
+          zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ZChain.asupf zc ; supf-mono = ZChain.supf-mono zc ; order = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs    }  where
 
                  --  supf0 px not is included by the chain
@@ -1376,8 +1392,8 @@
 
                  sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
                  sup {z} z≤x with trio< z px
-                 ... | tri< a ¬b ¬c = ? -- jrecord { tsup = ZChain.minsup zc (o<→≤ a)  ; tsup=sup = ZChain.supf-is-minsup zc (o<→≤ a) }
-                 ... | tri≈ ¬a b ¬c = ? -- record { tsup = ZChain.minsup zc (o≤-refl0 b)  ; tsup=sup = ZChain.supf-is-minsup zc (o≤-refl0 b) }
+                 ... | tri< a ¬b ¬c = record { tsup = ZChain.minsup zc (o<→≤ a)  ; tsup=sup = ZChain.supf-is-minsup zc (o<→≤ a) }
+                 ... | tri≈ ¬a b ¬c = record { tsup = ZChain.minsup zc (o≤-refl0 b)  ; tsup=sup = ZChain.supf-is-minsup zc (o≤-refl0 b) }
                  ... | tri> ¬a ¬b px<z = zc35 where
                      zc30 : z ≡ x
                      zc30 with osuc-≡< z≤x
@@ -1396,31 +1412,23 @@
                      ... | tri> ¬a ¬b c = zc36 ¬b
                      ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ?  } where
                           zc37 : MinSUP A (UnionCF A f mf ay supf0 z)
-                          zc37 = record { sup = ? ; asm = ? ; x≤sup = ? }
+                          zc37 = record { sup = ? ; asm = ? ; x≤sup = ? ; minsup = ? }
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsMinSUP A (UnionCF A f mf ay supf0 b) supf0 ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) f b ) → supf0 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
                  ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫
                  ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫
-                 ... | tri> ¬a ¬b px<b = zc31 ? where
+                 ... | tri> ¬a ¬b px<b = ? where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
                      ... | case1 eq = sym (eq)
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
-                     --  x o< sp      supf0 b ≡ supf0 x o≤ supf0 sp
-                     --      supf0 sp ≡ sp (?)
-                     zcsup : xSUP (UnionCF A f mf ay supf0 px) supf0 x
-                     zcsup with zc30
-                     ... | refl = record { ax = ab ; is-sup = record { x≤sup = λ {w} lt →
-                        IsMinSUP.x≤sup (proj1 is-sup) ? ; minsup = ? } }
-                     zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) supf0 x ) ∨  HasPrev A (UnionCF A f mf ay supf0 px) f x ) → supf0 b ≡ b
-                     zc31 (case1 ¬sp=x) with zc30
-                     ... | refl = ⊥-elim (¬sp=x zcsup )
-                     zc31 (case2 hasPrev ) with zc30
-                     ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev
-                                ; ay = ? ; x=fy = HasPrev.x=fy hasPrev } )
-
-     ... | no lim = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono 
+                     zc31 : sp1 o≤ b
+                     zc31 = MinSUP.minsup sup1 ab zc32 where 
+                         zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b) 
+                         zc32 = ?
+                     
+     ... | no lim = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs    }  where
 
           pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z
@@ -1457,14 +1465,14 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 with trio< (IChain.i ia)  (IChain.i ib)
                ... | tri< ia<ib ¬b ¬c with 
-                    <=-trans (ZChain.supf-<= (pzc (ob<x lim (IChain.i<x ib))) ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (≤to<= (s≤fc _ f mf (IChain.fc ib)))
+                    <=-trans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (≤to<= (s≤fc _ f mf (IChain.fc ib)))
                ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                    ct00 : * (& a) ≡ * (& b)
                    ct00 = cong (*) eq1
                ... | case2 lt = tri< lt  (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)  
                uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib)) 
                uz01 | tri> ¬a ¬b ib<ia  with
-                    <=-trans (ZChain.supf-<= (pzc (ob<x lim (IChain.i<x ia))) ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (≤to<= (s≤fc _ f mf (IChain.fc ia)))
+                    <=-trans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (≤to<= (s≤fc _ f mf (IChain.fc ia)))
                ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                    ct00 : * (& a) ≡ * (& b)
                    ct00 = sym (cong (*) eq1)
@@ -1606,6 +1614,16 @@
                               (subst (λ k → FClosure A f k z) (sb=sa s<b ) fc )) where
                               s<b : s o< b 
                               s<b = ordtrans (supf-inject0 supf-mono  s<u ) u<x
+
+          sup=u : {b : Ordinal} (ab : odef A b) →
+                b o≤ x → IsMinSUP A (UnionCF A f mf ay supf1 b) supf1 ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) f b ) → supf1 b ≡ b
+          sup=u {b} ab b≤x is-sup with osuc-≡< b≤x
+          ... | case1 b=x = ? where
+                 zc31 : spu o≤ b
+                 zc31 = MinSUP.minsup usup ab zc32 where 
+                     zc32 : {w : Ordinal } → odef pchainx w → (w ≡ b) ∨ (w << b) 
+                     zc32 = ?
+          ... | case2 b<x = trans (sf1=sf ?) (ZChain.sup=u (pzc (ob<x lim b<x)) ab ? ? )
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---