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

changeset 756:60a2340e892d

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, 24 Jul 2022 12:07:11 +0900
parents b22327e78b03
children 359f1577f947
files src/zorn.agda
diffstat 1 files changed, 38 insertions(+), 50 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Jul 24 09:42:02 2022 +0900
+++ b/src/zorn.agda	Sun Jul 24 12:07:11 2022 +0900
@@ -258,11 +258,10 @@
 
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where
    field
-      fcy<sup  : {z : Ordinal } → FClosure A f y z → z << supf u
       csupz    : FClosure A f (supf u) z 
+      supfu=u  : supf u ≡ u 
+      fcy<sup  : {z : Ordinal } → FClosure A f y z → z << supf u   -- not a initial chain
       order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → z1 << supf u
-      y<s      : y << supf u  -- not a initial chain
-      supfu=u  : supf u ≡ u 
 
 -- Union of supf z which o< x
 --
@@ -270,7 +269,7 @@
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
        (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where 
     ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
-    ch-is-sup  : (u : Ordinal) {z : Ordinal } (u<x : u o≤ x ) ( is-sup : ChainP A f mf ay supf u z) 
+    ch-is-sup  : (u : Ordinal) {z : Ordinal } (u≤x : u o≤ x ) ( is-sup : ChainP A f mf ay supf u z) 
         ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -293,19 +292,19 @@
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
+
       csupf : {z : Ordinal } → odef chain (supf 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 
+      fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → w << supf u     -- different from order because y o< supf 
+      order : {b sup1 z1 : Ordinal} → b o< z → sup1 o≤ b → FClosure A f (supf sup1) z1 → z1 << supf b
+
 
 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
-      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
-      fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → w << (ZChain.supf zc) u
-      sup=u : {b : Ordinal} → {ab : odef A b} → b o< z  → IsSup A (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) ab → (ZChain.supf zc) b ≡ b 
-      order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f ((ZChain.supf zc) sup1) z1 → z1 << (ZChain.supf zc) b
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -357,7 +356,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<s = ChainP.y<s cp ; supfu=u  = ChainP.supfu=u cp  
+ChainP-next A f mf {y} ay supf {x} {z} cp = record { supfu=u  = ChainP.supfu=u cp  
      ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
 
 Zorn-lemma : { A : HOD } 
@@ -427,33 +426,33 @@
             odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
         chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , ch-init fc  ⟫ = 
             ⟪ ua , ch-init fc  ⟫ 
-        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ uaa ,  ch-is-sup ua u<x is-sup fc  ⟫ = 
-            ⟪ uaa , ch-is-sup ua (OrdTrans u<x a≤b) is-sup fc  ⟫ 
+        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ uaa ,  ch-is-sup ua u≤x is-sup fc  ⟫ = 
+            ⟪ uaa , ch-is-sup ua (OrdTrans u≤x a≤b) is-sup fc  ⟫ 
         chain<ZA : {x : Ordinal } → UnionCF A f mf ay (ZChain.supf zc) x ⊆' UnionCF A f mf ay (ZChain.supf zc) (& A)
         chain<ZA {x} ux with proj2 ux
         ... | ch-init fc = ⟪ proj1 ux , ch-init fc ⟫
-        ... | ch-is-sup u pu<x is-sup fc = ⟪ proj1 ux , ch-is-sup u (o<→≤ u<x) is-sup fc ⟫ where
+        ... | ch-is-sup u pu≤x is-sup fc = ⟪ proj1 ux , ch-is-sup u (o<→≤ u≤x) is-sup fc ⟫ where
             u<A : (& ( * ( ZChain.supf zc u)))  o< & A
             u<A = c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fcs _ f mf fc) )
-            u<x :  u o< & A
-            u<x = subst (λ k → k o< & A ) (trans &iso (ChainP.supfu=u is-sup)) u<A
+            u≤x :  u o< & A
+            u≤x = subst (λ k → k o< & A ) (trans &iso (ChainP.supfu=u is-sup)) u<A
         is-max-hp : (x : Ordinal) {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 → 
             * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
         is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
         ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 
-        ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , 
+        ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , 
                  subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
-                      (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
+                      (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
         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 with Oprev-p x
-        ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = ? ; sup=u = ? ; order = ? } where
+        ... | yes op = record { is-max = is-max } where
            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 = ?
+           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 →
@@ -471,7 +470,7 @@
                     m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a
                     m03 with proj2 ua
                     ... | ch-init fc = ⟪ proj1 ua ,  ch-init fc ⟫
-                    ... | ch-is-sup u u<x is-sup fc with trio< u px
+                    ... | ch-is-sup u u≤x is-sup fc with trio< u px
                     ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup fc ⟫ -- u o< osuc x
                     ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup fc ⟫
                     ... | tri> ¬a ¬b c = ?   -- u = x
@@ -479,16 +478,7 @@
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
                  ... | tri≈ ¬a b=px ¬c = ? -- b = px case,  u = px  u< osuc x 
-        ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = fcy<sup ; sup=u = sup=u ; order = order  }  where
-           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 = ZChain1.fcy<sup (prev (osuc u) (ob<x lim u<x)) <-osuc fc
-           sup=u :  {b : Ordinal} {ab : odef A b} → b o< x →
-                IsSup A (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) ab →
-                ZChain.supf zc b ≡ b
-           sup=u {b} {ab} b<x is-sup = ZChain1.sup=u (prev (osuc b) (ob<x lim b<x)) <-osuc is-sup
-           order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b →
-                FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
-           order {b} b<x s<b fc = ZChain1.order (prev (osuc b) (ob<x lim b<x)) <-osuc s<b fc
+        ... | no lim = record { is-max = is-max }  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 →
@@ -498,17 +488,15 @@
            ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA (chain-mono2 (osuc x) (o<→≤ <-osuc ) o≤-refl ua )) )
                        (subst (λ k → * a < * k ) (sym b=y) a<b ) )
            ... | case2 y<b = chain-mono2 x (o<→≤ (ob<x lim b<x) ) o≤-refl m04 where
-                 y<s : y << ZChain.supf zc b
-                 y<s = y<s 
                  m07 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b
-                 m07 {z} fc = ZChain1.fcy<sup (prev (osuc b) (ob<x lim b<x)) <-osuc fc
+                 m07 {z} fc = ZChain.fcy<sup zc ? fc
                  m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
-                 m08 {sup1} {z1} s<b fc = ZChain1.order (prev (osuc b) (ob<x lim b<x) ) <-osuc s<b fc
+                 m08 {sup1} {z1} s<b fc = ZChain.order zc ? ?  fc
                  m05 : b ≡ ZChain.supf zc b
-                 m05 = sym (ZChain1.sup=u (prev (osuc b) (ob<x lim b<x)) {_} {ab} <-osuc 
-                        record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<x)) o≤-refl lt )} )   -- ZChain on x
+                 m05 = sym (ZChain.sup=u zc {_} {ab} ?
+                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<x)) o≤-refl lt )} )   -- ZChain on x
                  m06 : ChainP A f mf ay (ZChain.supf zc) b b
-                 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 ; y<s = y<s 
+                 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 
                        ; supfu=u = sym m05 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
                  m04 = ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc) m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
@@ -577,20 +565,20 @@
           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 ; csupf = ?
+     inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = ? ; fcy<sup = ? 
       ; 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
+          isupf z = ? ---  Sup of fc y, is in chain, and fcy<sup
           cy : odef (UnionCF A f mf ay isupf o∅) y
           cy = ⟪ ay , ch-init (init ay)  ⟫
           isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
           isy {z} ⟪ az , uz ⟫ with uz 
           ... | ch-init fc = s≤fc y f mf fc 
-          ... | ch-is-sup u u<x is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
+          ... | ch-is-sup u u≤x is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
           inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
           inext {a} ua with (proj2 ua)
           ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫
-          ... | ch-is-sup u u<x is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
+          ... | ch-is-sup u u≤x is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
           itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 
           itotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
@@ -631,11 +619,11 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-          pnext {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u<x (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc ) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc ) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
+          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
                zc7 : y << (ZChain.supf zc) u 
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
@@ -646,13 +634,13 @@
           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 ? ) is-sup fc ⟫ 
+          ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u (OrdTrans u<px (o<→≤ 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  ; csupf = csupf
+               ; initial = pinit ; chain∋init = pcy  ; csupf = csupf ; sup=f = ? ; order = ? ; fcy<sup = ?
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } 
 
           zc4 : ZChain A f mf ay x 
@@ -663,7 +651,7 @@
           ... | 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 = ? ; csupf = ?
+                record {  supf = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ? ; csupf = ? ; sup=f = ? ; order = ? ; fcy<sup = ?
                      ; initial = ? ; chain∋init  = ? }  where
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x 
@@ -747,11 +735,11 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫
-          pnext {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u u<x (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u u≤x (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
+          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
                zc7 : y << psupf ?
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
@@ -762,7 +750,7 @@
                uz01 = chain-total A f mf ay psupf ( (proj2 ca)) ( (proj2 cb)) 
 
           no-extension : ZChain A f mf ay x
-          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; csupf = csupf
+          no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; csupf = csupf ; sup=u = ? ; order = ? ; fcy<sup = ?
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 
           zc5 : ZChain A f mf ay x 
@@ -772,7 +760,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  ; csupf = ?
+          ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; csupf = ? ; sup=u = ? ; order = ? ; fcy<sup = ?
               ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = ? } where -- x is a sup of (zc ?) 
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x