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

changeset 805:9d97134d0a93

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 Fri, 12 Aug 2022 09:02:51 +0900
parents 2d84411a636e
children 473825abd767
files src/zorn.agda
diffstat 1 files changed, 35 insertions(+), 47 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Aug 11 14:07:57 2022 +0900
+++ b/src/zorn.agda	Fri Aug 12 09:02:51 2022 +0900
@@ -692,62 +692,40 @@
           -- 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 : ¬  sp1 ≡ supf1 x → ZChain A f mf ay x
-          no-extension ¬sp=x = record { supf = supf1 ;  sup = sup
-               ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = {!!} ; csupf = csupf
-              ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
-                 UnionCF⊆ : {z : Ordinal } → z o≤ x →  UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf0 x 
-                 UnionCF⊆ {z} z≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-                 UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤z record { fcy<sup = fc<s ; order = o1 ; supu=u = sp=u }  (init  au1 refl) ⟫ = zc30 where
-                     zc30 : odef (UnionCF A f mf ay supf0 x) (supf1 u1 )
-                     zc30 with trio< u1 px
-                     ... | tri< a ¬b ¬c = ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x)  ? (init au1 refl) ⟫ 
-                     ... | tri≈ ¬a b ¬c = ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x)  ? (init au1 refl) ⟫ 
-                     ... | tri> ¬a ¬b px<u1 = ? where
-                          zc31 : u1 ≡ x
-                          zc31 with trio< u1 x
-                          ... | tri< a ¬b ¬c = ⊥-elim (¬p<x<op ⟪ px<u1 , subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) a ⟫ )
-                          ... | tri≈ ¬a b ¬c = b
-                          ... | tri> ¬a ¬b c =  ⊥-elim (¬p<x<op ⟪ c , ordtrans≤-< u1≤z z≤x  ⟫ )
-                 UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (fsuc xp fcu1) ⟫ with
-                      UnionCF⊆ {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤z u1-is-sup fcu1 ⟫ 
-                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
-                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
-                 UnionCF⊆R : {z : Ordinal } → z o≤ x →  UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay supf1 x 
-                 UnionCF⊆R {z} z≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-                 UnionCF⊆R {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (init  au1 refl) ⟫   
-                     = ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x) ? (init ? ?) ⟫
-                 UnionCF⊆R {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (fsuc xp fcu1) ⟫ with
-                      UnionCF⊆R {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤z u1-is-sup fcu1 ⟫ 
-                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
-                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
-                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
+
+          record xSUP : Set n where
+            field
+               ax : odef A x
+               not-sup : IsSup A (UnionCF A f mf ay supf0 x) ax
+
+          no-extension : ¬ xSUP → ZChain A f mf ay x
+          no-extension ¬sp=x = record { supf = supf0 ;  sup = sup
+               ; initial = pinit ; chain∋init = pcy ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
+              ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext ;  f-total = ptotal }  where
+                 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⊆ (UnionCF⊆ ? ) (ZChain.sup zc ? )
-                 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCF⊆ ? ) (ZChain.sup zc ? )
-                 ... | tri> ¬a ¬b c = SUP⊆ (λ lt  → chain-mono f mf ay _ ? (UnionCF⊆ ? lt )) sup1
+                 ... | tri< a ¬b ¬c = ZChain.sup zc (o<→≤ a)
+                 ... | tri≈ ¬a b ¬c = ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl )
+                 ... | tri> ¬a ¬b c = ZChain.sup zc ?
                  sup=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
+                    b o≤ x → IsSup A (UnionCF A f mf ay supf0 (osuc b)) ab → supf0 b ≡ b
                  sup=u {b} ab b<x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ? where
-                     zc11 = ZChain.sup=u zc ab ? ?
-                 ... | tri≈ ¬a b ¬c = ? 
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) is-sup
+                 ... | tri≈ ¬a b ¬c =  ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) is-sup
                  ... | tri> ¬a ¬b c = ?
-                 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)) 
-                 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
-                 csupf {b} b≤x with trio< b px | inspect supf1 b
-                 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫
-                 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫
-                 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ supf1 k ) (sym zc30) (sym eq1) )) where  
+                 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 b) (supf0 b)
+                 csupf {b} b≤x with trio< b px 
+                 ... | tri< a ¬b ¬c =  ZChain.csupf zc (o<→≤ a)
+                 ... | tri≈ ¬a b ¬c =  ZChain.csupf zc (subst (λ k → k o≤ px) (sym b) o≤-refl )
+                 ... | tri> ¬a ¬b px<b =  ? where
                      --   px< b ≤ x
                      -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1
                      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) → supf0 z ≡ & (SUP.sup (sup z≤x))
+                 sis = ?
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
@@ -787,6 +765,11 @@
           pzc z z<x = prev z z<x
           ysp =  & (SUP.sup (ysup f mf ay))
 
+          record SupE ( z : Ordinal ) : Set n where
+             field
+                z<x : z o< x
+                z=supfz : z ≡  ZChain.supf (pzc z z<x) z
+
           psupf0 : (z : Ordinal) → Ordinal
           psupf0 z with trio< z x
           ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
@@ -842,7 +825,12 @@
                      subst (λ k → UChain A f mf ay supf x k )
                           (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫ 
 
-          no-extension : ¬ spu ≡ x → ZChain A f mf ay x
+          record xSUP : Set n where
+            field
+               ax : odef A x
+               not-sup : IsSup A (UnionCF A f mf ay psupf0 x) ax
+
+          no-extension : ¬ xSUP → ZChain A f mf ay x
           no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = sup=u
                ; sup = sup ; supf-is-sup = sis
                ; csupf = csupf ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where