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

comparison src/zorn.agda @ 1068:f24f4de4d459

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add 0<supfz
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 13 Dec 2022 02:59:01 +0900
parents 074b6a506b1b
children 99df080f4fdb
comparison
equal deleted inserted replaced
1067:074b6a506b1b 1068:f24f4de4d459
348 348
349 asupf : {x : Ordinal } → odef A (supf x) 349 asupf : {x : Ordinal } → odef A (supf x)
350 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y 350 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y
351 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z 351 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
352 zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x 352 zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x
353 0<supfz : {x : Ordinal } → o∅ o< supf x
353 354
354 is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) 355 is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x)
355 356
356 chain : HOD 357 chain : HOD
357 chain = UnionCF A f ay supf z 358 chain = UnionCF A f ay supf z
883 m13 spx<x = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where 884 m13 spx<x = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where
884 m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1) 885 m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1)
885 m14 {z} uz = MinSUP.x≤sup sup1 (case1 uz) 886 m14 {z} uz = MinSUP.x≤sup sup1 (case1 uz)
886 887
887 zc41 : ZChain A f mf< ay x 888 zc41 : ZChain A f mf< ay x
888 zc41 = record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order 889 zc41 = record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order ; 0<supfz = ?
889 ; zo≤sz = zo≤sz ; supfmax = supfmax ; is-minsup = is-minsup ; cfcs = cfcs } where 890 ; zo≤sz = zo≤sz ; supfmax = supfmax ; is-minsup = is-minsup ; cfcs = cfcs } where
890 891
891 supf1 : Ordinal → Ordinal 892 supf1 : Ordinal → Ordinal
892 supf1 z with trio< z px 893 supf1 z with trio< z px
893 ... | tri< a ¬b ¬c = supf0 z 894 ... | tri< a ¬b ¬c = supf0 z
1236 z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa) 1237 z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa)
1237 b≤x (subst (λ k → supf1 a o< k ) (sym sf1b=sp1) sa<sb ) ) ) sf1b=sp1 1238 b≤x (subst (λ k → supf1 a o< k ) (sym sf1b=sp1) sa<sb ) ) ) sf1b=sp1
1238 1239
1239 ... | no lim with trio< x o∅ 1240 ... | no lim with trio< x o∅
1240 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 1241 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
1241 ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) 1242 ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = ?
1242 ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s ) 1243 ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s )
1243 ; zo≤sz = ? ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ? } where 1244 ; zo≤sz = ? ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ? } where
1244 mf : ≤-monotonic-f A f 1245 mf : ≤-monotonic-f A f
1245 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where 1246 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
1246 mf00 : * x < * (f x) 1247 mf00 : * x < * (f x)
1247 mf00 = proj1 ( mf< x ax ) 1248 mf00 = proj1 ( mf< x ax )
1248 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? 1249 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = ?
1249 ; zo≤sz = ? ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where 1250 ; zo≤sz = ? ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where
1250 1251
1251 -- mf : ≤-monotonic-f A f 1252 -- mf : ≤-monotonic-f A f
1252 -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫ will result memory exhaust 1253 -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫ will result memory exhaust
1253 1254
1318 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( begin 1319 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( begin
1319 ZChain.supf (pzc (pic<x ib)) (IChain-i ib) ≡⟨ zeq _ _ (o<→≤ (osucc c)) (o<→≤ <-osuc) ⟩ 1320 ZChain.supf (pzc (pic<x ib)) (IChain-i ib) ≡⟨ zeq _ _ (o<→≤ (osucc c)) (o<→≤ <-osuc) ⟩
1320 ZChain.supf (pzc (pic<x ia)) (IChain-i ib) ≤⟨ ZChain.supf-mono (pzc (pic<x ia)) (o<→≤ c) ⟩ 1321 ZChain.supf (pzc (pic<x ia)) (IChain-i ib) ≤⟨ ZChain.supf-mono (pzc (pic<x ia)) (o<→≤ c) ⟩
1321 ZChain.supf (pzc (pic<x ia)) (IChain-i ia) ∎ ) sa<sb ) where open o≤-Reasoning O 1322 ZChain.supf (pzc (pic<x ia)) (IChain-i ia) ∎ ) sa<sb ) where open o≤-Reasoning O
1322 1323
1324 IC⊆ : {a b : Ordinal } (ia : IChain ay supfz a ) (ib : IChain ay supfz b )
1325 → IChain-i ia o≤ IChain-i ib → odef (ZChain.chain (pzc (pic<x ib))) a
1326 IC⊆ {a} {b} (ic-init fc ) ib ia≤ib = ⟪ A∋fc _ f mf fc , ch-init fc ⟫
1327 IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia≤ib = ⊥-elim ( o≤> ia≤ib ic01 ) where
1328 ic02 : o∅ o< supfz i<x
1329 ic02 = ZChain.0<supfz (pzc (ob<x lim i<x))
1330 ic01 : o∅ o< i
1331 ic01 = ordtrans<-≤ ic02 sa<x
1332 IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia≤ib
1333 = ZChain.cfcs (pzc (ob<x lim j<x) ) ia≤ib o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) ia≤ib) sb<x)
1334 (subst (λ k → FClosure A f k a) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc)) fc )
1335
1323 ptotalx : IsTotalOrderSet pchainx 1336 ptotalx : IsTotalOrderSet pchainx
1324 ptotalx {a} {b} ia ib with trio< (ZChain.supf (pzc (pic<x (proj2 ia))) (IChain-i (proj2 ia))) 1337 ptotalx {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib))
1325 (ZChain.supf (pzc (pic<x (proj2 ib))) (IChain-i (proj2 ib))) 1338 ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainx⊆chain ib)
1326 ... | tri< ia<ib ¬b ¬c = uz01 where 1339 ... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainx⊆chain ib)
1327 uz01 : Tri (a < b) (a ≡ b) (b < a ) 1340 ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) (o<→≤ ib<ia))
1328 uz01 with pchainx⊆chain ia
1329 ... | ⟪ ai , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-init fc ⟫ (pchainx⊆chain ib)
1330 ... | ⟪ ai , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-is-sup u uz02 uz03 uz04 ⟫ (pchainx⊆chain ib) where
1331 a<b : IChain-i (proj2 ia) o< IChain-i (proj2 ib)
1332 a<b = ichain-inject {_} {_} {proj2 ia} {proj2 ib} ia<ib
1333 uz02 : u o< osuc (IChain-i (proj2 ib))
1334 uz02 = ordtrans<-≤ u<x (o<→≤ (osucc a<b))
1335 uz03 : ZChain.supf (pzc (pic<x (proj2 ib))) u ≡ u
1336 uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) )) su=u
1337 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a)
1338 uz04 = subst (λ k → FClosure A f k (& a)) ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) ) fc
1339 ... | tri≈ ¬a ia=ib ¬c = ? where
1340 uz01 : Tri (* (& a ) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a ))
1341 uz01 with proj2 ia | proj2 ib
1342 ... | ic-init fca | ic-init fcb = fcn-cmp y f mf fca fcb
1343 ... | ic-isup ia ia<x sa<x fca | ic-init fcb = ?
1344 ... | ic-init fca | ic-isup ib ib<x sb<x fcb = ?
1345 ... | ic-isup ia ia<x sa<x fca | ic-isup ib ib<x sb<x fcb = fcn-cmp ? f mf ? ?
1346 ... | tri> ¬a ¬b ib<ia = uz01 where
1347 uz01 : Tri (a < b) (a ≡ b) (b < a )
1348 uz01 with pchainx⊆chain ib
1349 ... | ⟪ bi , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) ⟪ bi , ch-init fc ⟫
1350 ... | ⟪ bi , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) ⟪ bi , ch-is-sup u uz02 uz03 uz04 ⟫ where
1351 b<a : IChain-i (proj2 ib) o< IChain-i (proj2 ia)
1352 b<a = ichain-inject {_} {_} {proj2 ib} {proj2 ia} ib<ia
1353 uz02 : u o< osuc (IChain-i (proj2 ia))
1354 uz02 = ordtrans<-≤ u<x (o<→≤ (osucc b<a))
1355 uz03 : ZChain.supf (pzc (pic<x (proj2 ia))) u ≡ u
1356 uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc b<a)) (o<→≤ u<x) )) su=u
1357 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ia))) u) (& b)
1358 uz04 = subst (λ k → FClosure A f k (& b)) ( zeq _ _ (o<→≤ (osucc b<a)) (o<→≤ u<x) ) fc
1359 1341
1360 usup : MinSUP A pchainx 1342 usup : MinSUP A pchainx
1361 usup = minsupP pchainx (λ ic → ? ) ptotalx 1343 usup = minsupP pchainx (λ ic → ? ) ptotalx
1362 spu = MinSUP.sup usup 1344 spu = MinSUP.sup usup
1363 1345