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

comparison src/zorn.agda @ 795:408e7e8a3797

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
csupf depends on order cyclicly
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Aug 2022 16:21:46 +0900
parents 0acbc2b102e9
children 171123c92007
comparison
equal deleted inserted replaced
794:0acbc2b102e9 795:408e7e8a3797
308 initial : {z : Ordinal } → odef chain z → * y ≤ * z 308 initial : {z : Ordinal } → odef chain z → * y ≤ * z
309 f-next : {a : Ordinal } → odef chain a → odef chain (f a) 309 f-next : {a : Ordinal } → odef chain a → odef chain (f a)
310 f-total : IsTotalOrderSet chain 310 f-total : IsTotalOrderSet chain
311 311
312 sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x) 312 sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x)
313 supf-is-sup : {x : Ordinal } → (x<z : x o≤ z) → supf x ≡ & (SUP.sup (sup x<z) )
314 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 313 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
315 csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 314 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
316 supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
317 fcy<sup : {u w : Ordinal } → u o< z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 315 fcy<sup : {u w : Ordinal } → u o< z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
318 fcy<sup {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) 316 fcy<sup {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)
319 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 317 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
320 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) )) 318 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
321 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt ) 319 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
320
321 csupf : {b : Ordinal } → b o< z → odef (UnionCF A f mf ay supf b) (supf b)
322 csupf {b} b<z = ⟪ asb , ch-is-sup b o≤-refl is-sup (init asb refl) ⟫ where
323 asb : odef A (supf b)
324 asb = subst (λ k → odef A k ) (sym (supf-is-sup ? )) (SUP.A∋maximal (sup ? ))
325 is-sup : ChainP A f mf ay supf b
326 is-sup = record { fcy<sup = fcy<sup b<z ; order = ? ; supu=u = ? }
327 supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
328 supf-mono = ?
329 -- supf-is-sup {x} x≤z = ? where
330 -- zc51 : * (supf x) ≡ SUP.sup (sup x≤z )
331 -- zc51 = ==→o≡ record { eq→ ? ; eq← = ? }
332 -- zc50 : supf x ≡ & (SUP.sup (sup x<z) )
333 -- zc50 = ?
322 order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) 334 order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
323 order {b} {s} {z1} b<z sf<sb fc = zc04 where 335 order {b} {s} {z1} b<z sf<sb fc = zc04 where
324 zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 336 zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
325 zc01 (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03 where 337 zc01 (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03 where
326 s<b : s o< b 338 s<b : s o< b
331 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sf<sb ) 343 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sf<sb )
332 ... | case2 lt = ⊥-elim ( o<> lt sf<sb ) 344 ... | case2 lt = ⊥-elim ( o<> lt sf<sb )
333 s<z : s o< z 345 s<z : s o< z
334 s<z = ordtrans s<b b<z 346 s<z = ordtrans s<b b<z
335 zc03 : odef (UnionCF A f mf ay supf b) (supf s) 347 zc03 : odef (UnionCF A f mf ay supf b) (supf s)
336 zc03 with csupf (o<→≤ s<z) 348 zc03 with csupf s<z
337 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 349 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫
338 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u≤x (osucc s<b)) is-sup fc ⟫ 350 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u≤x (osucc s<b)) is-sup fc ⟫
339 zc01 (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where 351 zc01 (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where
340 zc04 : odef (UnionCF A f mf ay supf b) (f x) 352 zc04 : odef (UnionCF A f mf ay supf b) (f x)
341 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc ) 353 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc )
880 subst (λ k → UChain A f mf ay supf x k ) 892 subst (λ k → UChain A f mf ay supf x k )
881 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ 893 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫
882 894
883 no-extension : ¬ spu ≡ x → ZChain A f mf ay x 895 no-extension : ¬ spu ≡ x → ZChain A f mf ay x
884 no-extension ¬sp=x = record { initial = pinit ; chain∋init = pcy ; supf = supf1 ; sup=u = {!!} 896 no-extension ¬sp=x = record { initial = pinit ; chain∋init = pcy ; supf = supf1 ; sup=u = {!!}
885 ; supf-is-sup = ? 897 ; sup = ? ; supf-is-sup = ?
886 ; csupf = ? ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; supf-mono = ? } where 898 ; csupf = ? ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; supf-mono = ? } where
887 UnionCF⊆ : UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay ? x 899 supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
888 900 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
901 UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay (supfu a) x
902 UnionCF⊆ = ?
889 zc5 : ZChain A f mf ay x 903 zc5 : ZChain A f mf ay x
890 zc5 with ODC.∋-p O A (* x) 904 zc5 with ODC.∋-p O A (* x)
891 ... | no noax = no-extension ? -- ¬ A ∋ p, just skip 905 ... | no noax = no-extension ? -- ¬ A ∋ p, just skip
892 ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f ) 906 ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )
893 -- we have to check adding x preserve is-max ZChain A y f mf x 907 -- we have to check adding x preserve is-max ZChain A y f mf x
894 ... | case1 pr = no-extension ? 908 ... | case1 pr = no-extension ?
895 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax ) 909 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
896 ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!} ; supf = supf1 ; sup=u = {!!} 910 ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!} ; supf = supf1 ; sup=u = {!!}
897 ; supf-is-sup = ? 911 ; sup = ? ; supf-is-sup = ?
898 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = ? ; supf-mono = ? } where -- x is a sup of (zc ?) 912 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = ? ; supf-mono = ? } where -- x is a sup of (zc ?)
899 ... | case2 ¬x=sup = no-extension ? -- x is not f y' nor sup of former ZChain from y -- no extention 913 ... | case2 ¬x=sup = no-extension ? -- x is not f y' nor sup of former ZChain from y -- no extention
900 914
901 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A) 915 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A)
902 SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) (& A) 916 SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) (& A)