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

changeset 840:52bff0b4cb37

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, 29 Aug 2022 10:18:08 +0900
parents 710574600659
children 01361e10ad96
files src/zorn.agda
diffstat 1 files changed, 67 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Aug 28 14:46:18 2022 +0900
+++ b/src/zorn.agda	Mon Aug 29 10:18:08 2022 +0900
@@ -732,20 +732,41 @@
           supf1 : Ordinal → Ordinal
           supf1 z with trio< z px
           ... | tri< a ¬b ¬c = ZChain.supf zc z
-          ... | tri≈ ¬a b ¬c = sp1 
+          ... | tri≈ ¬a b ¬c = ZChain.supf zc z
           ... | tri> ¬a ¬b c = sp1 
 
           pchain1 : HOD
           pchain1  = UnionCF A f mf ay supf1 x
 
+          ptotal1 : IsTotalOrderSet pchain1
+          ptotal1 {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) )
+               uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) 
+          pchain⊆A1 : {y : Ordinal} → odef pchain1 y →  odef A y
+          pchain⊆A1 {y} ny = proj1 ny
+          pnext1 : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a)
+          pnext1 {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
+          pnext1 {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
+          pinit1 :  {y₁ : Ordinal} → odef pchain1 y₁ → * y ≤ * y₁
+          pinit1 {a} ⟪ aa , ua ⟫  with  ua
+          ... | ch-init fc = s≤fc y f mf fc
+          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
+               zc7 : y <= supf1 u 
+               zc7 = ChainP.fcy<sup is-sup (init ay refl)
+          pcy1 : odef pchain1 y
+          pcy1 = ⟪ ay , ch-init (init ay refl)    ⟫
+
+          -- zc100  : xSUP (UnionCF A f mf ay supf0 px) x → x ≡ sp1
+          -- zc100  = ?
+
           -- if previous chain satisfies maximality, we caan reuse it
           --
           --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
 
           no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x
-          no-extension ¬sp=x = record { supf = supf1 ;  sup = ? ; supf-mono = {!!}
-               ; initial = ? ; chain∋init = ? ; sup=u = ? ; supf-is-sup = ? ; csupf = {!!}
-              ;  chain⊆A = λ lt → proj1 lt ;  f-next = ? ;  f-total = ? }  where
+          no-extension ¬sp=x = record { supf = supf1 ;  sup = sup ; supf-mono = ?
+               ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
+              ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
                  pchain0=1 : pchain ≡ pchain1
                  pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
                      zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
@@ -771,18 +792,22 @@
                           ... | tri< a ¬b ¬c = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u (subst (λ k → u o< k) (sym (Oprev.oprev=x op))  a) ? (init ? ? ) ⟫ 
                           ... | tri≈ ¬a b ¬c = ?
                           ... | tri> ¬a ¬b c = ⊥-elim ( o≤> u≤x c )
-                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf0 z)
-                 sup {z} z≤x with trio< z px
-                 ... | tri< a ¬b ¬c = SUP⊆ ? ( ZChain.sup zc (o<→≤   a) ) 
-                 ... | tri≈ ¬a b ¬c = record { sup = SUP.sup ? ; as = SUP.as ? ; x<sup = ? } where
-                     zc61 : {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup ?) ∨ (w < SUP.sup ? )
-                     zc61 {w} lt = ? -- SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) z<x  lt )
-                 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) ? ⟫ )
+                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
+                 sup {z} z≤x with trio< z px | inspect supf1 z
+                 ... | tri< a ¬b ¬c | record { eq = eq1} = ? -- ZChain.sup zc (o<→≤   a) 
+                 ... | tri≈ ¬a b ¬c | record { eq = eq1} = ?  -- ZChain.sup zc (o≤-refl0 b) 
+                 ... | tri> ¬a ¬b px<z | record { eq = eq1} = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc31 } where
+                     zc30 : z ≡ x
+                     zc30 with osuc-≡< z≤x
+                     ... | case1 eq = eq
+                     ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
+                     zc31 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w  → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
+                     zc31 = ?
                  sup=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab → supf0 b ≡ b
+                    b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 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 → IsSup.x<sup is-sup ? } 
-                 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } 
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup ? } 
                  ... | tri> ¬a ¬b px<b = ? where -- ⊥-elim (¬sp=x zcsup ) where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -791,16 +816,32 @@
                      zcsup : ?
                      zcsup = ? -- with zc30
                      -- ... | refl = case1 record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup ? } } 
-                 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 b) (supf0 b)
-                 csupf {b} b<x with trio< b px | inspect supf0 b
-                 ... | tri< a ¬b ¬c | _ = ? -- UnionCF⊆ o≤-refl a {!!}
-                 ... | tri≈ ¬a refl ¬c | _ = {!!} -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl )
-                 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = {!!} --  UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) 
-                 sis : {z : Ordinal} (z≤x : z o≤ x) → supf0 z ≡ & (SUP.sup (sup z≤x))
-                 sis {z} z<x with trio< z px
-                 ... | tri< a ¬b ¬c = ZChain.supf-is-sup zc (o<→≤ a )
-                 ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) ?  ⟫ )
+                 csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
+                 csupf {b} b≤x with trio< b px | inspect supf0 b
+                 ... | tri< a ¬b ¬c | _ = ? -- ZChain.csupf zc (o<→≤ a )
+                 ... | tri≈ ¬a refl ¬c | _ = ? -- ZChain.csupf zc o≤-refl 
+                 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = ? 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 ⟫ )
+                 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x))
+                 sis {z} z≤x  = zc40 where
+                      zc40 : supf1 z ≡ & (SUP.sup (sup z≤x))
+                      zc40 with trio< z px | inspect supf1 z | inspect sup z≤x
+                      ... | tri< a ¬b ¬c | record { eq = eq1 } | record { eq = eq2 } = ?
+                      ... | tri≈ ¬a b ¬c | record { eq = eq1 } | record { eq = eq2 } = ?
+                      ... | tri> ¬a ¬b c | record { eq = eq1 } | record { eq = eq2 } = ?
+--                 ... | tri< a ¬b ¬c = ? -- jZChain.supf-is-sup zc (o<→≤ a )
+--                 ... | tri≈ ¬a b ¬c = ? -- jZChain.supf-is-sup zc (o≤-refl0 b )
+--                 ... | tri> ¬a ¬b px<z = ? 
+--                 ... | tri< a ¬b ¬c | _ = ? -- jZChain.supf-is-sup zc (o<→≤ a )
+--                 ... | tri≈ ¬a b ¬c | _ = ? -- jZChain.supf-is-sup zc (o≤-refl0 b )
+--                 ... | tri> ¬a ¬b px<z | record { eq = eq1 } = ? where
+--                     zc30 : z ≡ x
+--                     zc30 with osuc-≡< z≤x
+--                     ... | case1 eq = eq
+--                     ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
@@ -852,6 +893,9 @@
           ... | tri≈ ¬a b ¬c = ysp
           ... | tri> ¬a ¬b c = ysp
 
+          
+          -- Union of UnionCF z, z o< x undef initial-segment condition                                                                 
+          --   this is not a ZChain because supf0 is not monotonic
           pchain : HOD
           pchain = UnionCF A f mf ay supf0 x