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

changeset 572:427e36467a18

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ZChain is monotonic on x, should be in record ZFChain
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 02 May 2022 23:23:12 +0900
parents 2ade91846f57
children 9ec37757a5a5
files src/zorn.agda
diffstat 1 files changed, 24 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon May 02 19:51:51 2022 +0900
+++ b/src/zorn.agda	Mon May 02 23:23:12 2022 +0900
@@ -522,11 +522,13 @@
                 s-ismax {a} {b} (case2 sa) b<ox ab (case1 p)  a<b | case2 b<x with HasPrev.ay p
                 ... | case1 zy = case1 (subst (λ k → odef chain k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc0 zy ))               -- in previous closure of f
                 ... | case2 sy = case2 (subst (λ k → FClosure A f (& (* x)) k ) (sym (HasPrev.x=fy p)) (fsuc (HasPrev.y p) sy ))  -- in current  closure of f
-                s-ismax {a} {b} (case2 sa) b<ox ab (case2 p)  a<b | case2 b<x = {!!} where -- closure of f cannot be a sup
+                s-ismax {a} {b} (case2 sa) b<ox ab (case2 p)  a<b | case2 b<x = case1 z23 where -- sup o< x is already in zc0
                      z24 : IsSup A schain ab → IsSup A (ZChain.chain zc0) ab 
                      z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
-                     z23 : FClosure A f (& (* x)) a → ¬ ( IsSup A schain ab )
-                     z23 = {!!}
+                     z23 : odef chain b
+                     z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc0 )
+                     ... | case1 y=b  = subst (λ k → odef chain k )  y=b ( ZChain.chain∋x zc0 )
+                     ... | case2 y<b  = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b
           ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
                    record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
                      ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 }  where -- no extention
@@ -539,14 +541,30 @@
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox =  {!!}  where --- limit ordinal case
+     ... | no ¬ox = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next
+                     ; initial = u-initial ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} }  where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field
                u : Ordinal
                u<x : u o< x
-               zuy : odef (ZChain.chain (prev u u<x {y} ay )) z
+               chain∋z : odef (ZChain.chain (prev u u<x {y} ay )) z
+         Uz⊆A : {z : Ordinal} → UZFChain z → odef A z
+         Uz⊆A {z} u = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) {y} ay ) (UZFChain.chain∋z u)
+         uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A ay f mf supO  (UZFChain.u u)
+         uzc {z} u =  prev (UZFChain.u u) (UZFChain.u<x u) {y} ay
          Uz : HOD
-         Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A ; <odmax = {!!} }
+         Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A
+             ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
+         u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
+         u-next {z} u = record { u = UZFChain.u u ; u<x = UZFChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UZFChain.chain∋z u)  }
+         u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z 
+         u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
+         u-chain∋x :  odef Uz y
+         u-chain∋x = {!!}
+         Uz-mono : { a b : Ordinal } → (ua : odef Uz a) (ub : odef Uz b )  → a o< b → ZChain.chain (uzc ua) ⊆' ZChain.chain (uzc ub)
+         Uz-mono {a} {b} ua ub a<b ca = ZChain.is-max (uzc ub) (ZChain.chain∋x (uzc ub)) {!!}  {!!} {!!} {!!} where
+             z30 : odef A b
+             z30 = (ZChain.chain⊆A (uzc ub) (UZFChain.chain∋z ub))
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy = {!!}
          --- ux ⊆ uy ∨ uy ⊆ ux