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

changeset 964:0bee632db679

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, 04 Nov 2022 20:48:00 +0900
parents a8c3ccf8f9d9
children 1c1c6a6ed4fa
files src/zorn.agda
diffstat 1 files changed, 9 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Nov 04 20:27:31 2022 +0900
+++ b/src/zorn.agda	Fri Nov 04 20:48:00 2022 +0900
@@ -488,7 +488,7 @@
    supf = ZChain.supf zc
    field
       is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → supf b o< supf z  → (ab : odef A b) 
-          → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsMinSUP A (UnionCF A f mf ay supf b) f ab  
+          → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsSUP A (UnionCF A f mf ay supf b) ab  
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
       order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
 
@@ -663,7 +663,7 @@
            zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt  )
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
               ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
-              HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsMinSUP A (UnionCF A f mf ay supf b) f ab →
+              HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
               * a < * b → odef (UnionCF A f mf ay supf x) b
            is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
            is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b 
@@ -677,7 +677,7 @@
               m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = 
                     chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
-              m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsMinSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫ 
+              m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫ 
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
@@ -688,11 +688,11 @@
         ... | no lim = record { is-max = is-max ; order = order }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
               ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
-              HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsMinSUP A (UnionCF A f mf ay supf b) f ab →
+              HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
               * a < * b → odef (UnionCF A f mf ay supf x) b
            is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P
            is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b 
-           is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsMinSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
+           is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
            ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
            ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
               m09 : b o< & A
@@ -709,7 +709,7 @@
                       chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) 
                  ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
-              m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
+              m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
               m06 : ChainP A f mf ay supf b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
@@ -1363,7 +1363,7 @@
            asp : odef A sp
            asp = MinSUP.asm sp1
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) 
-              →  HasPrev A chain f b  ∨  IsMinSUP A (UnionCF A f mf as0 (ZChain.supf zc) b) f ab
+              →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) b) ab
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
            z22 : sp o< & A
@@ -1376,24 +1376,8 @@
                z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne eq )
                ... | case2 lt = lt 
-               z19 : IsMinSUP A (UnionCF A f mf as0 (ZChain.supf zc) sp) f asp
-               z19 = record {   x≤sup = z20 ; minsup = z21  ; not-hp = ZChain.IsMinSUP→NotHasPrev zc ? z20 ? }  where
-                   z23 : {z : Ordinal } → odef chain z → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) z 
-                   z23 {z} ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-                   z23 {z} ⟪ au , ch-is-sup u u<x is-sup fc ⟫ = ⟪ au , ch-is-sup u z24 is-sup fc ⟫ where
-                       --  to prove sp is minsup , supf sp ≡ sp is necessary
-                       --  to prove supf s ≡ sp , sp is minsup is necessary
-                       z26 : supf sp ≡ sp
-                       z26 = ZChain.sup=u zc asp (o<→≤ z22) ⟪ record { x≤sup = ? } , ? ⟫
-                       z25 : u <= sp
-                       z25 = MinSUP.x≤sup sp1 ⟪ subst (λ k → odef A k) (ChainP.supu=u is-sup) (ZChain.asupf zc) 
-                           , ch-is-sup u u<x is-sup (init (ZChain.asupf zc) (ChainP.supu=u is-sup))  ⟫ 
-                       z24 : supf u o< supf sp
-                       z24 = ? -- with ZChain.supf-<= zc z25
-                   z21 : {sup1 : Ordinal} → odef A sup1 
-                       → ({z : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) z → (z ≡ sup1) ∨ (z << sup1)) 
-                       → sp o≤ sup1
-                   z21 {s} as s-sup = MinSUP.minsup sp1 as ( λ uz → s-sup (z23 uz) )
+               z19 : IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) sp) asp
+               z19 = record {   x≤sup = z20 }  where
                    z20 : {y : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
                    z20 {y} zy with MinSUP.x≤sup sp1 
                        (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22)  zy ))