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

comparison src/zorn.agda @ 934:ebcad8e5ae55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
resync zorn.agda
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Oct 2022 09:36:07 +0900
parents 0e0608b1953b
children ed711d7be191
comparison
equal deleted inserted replaced
933:409ac0af7b3b 934:ebcad8e5ae55
411 411
412 chain : HOD 412 chain : HOD
413 chain = UnionCF A f mf ay supf z 413 chain = UnionCF A f mf ay supf z
414 chain⊆A : chain ⊆' A 414 chain⊆A : chain ⊆' A
415 chain⊆A = λ lt → proj1 lt 415 chain⊆A = λ lt → proj1 lt
416
416 sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x) 417 sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x)
417 sup {x} x≤z = M→S supf (minsup x≤z) 418 sup {x} x≤z = M→S supf (minsup x≤z)
418 -- supf-sup<minsup : {x : Ordinal } → (x≤z : x o≤ z) → & (SUP.sup (M→S supf (minsup x≤z) )) o≤ supf x ... supf-mono 419
420 s=ms : {x : Ordinal } → (x≤z : x o≤ z ) → & (SUP.sup (sup x≤z)) ≡ MinSUP.sup (minsup x≤z)
421 s=ms {x} x≤z = &iso
419 422
420 chain∋init : odef chain y 423 chain∋init : odef chain y
421 chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ 424 chain∋init = ⟪ ay , ch-init (init ay refl) ⟫
422 f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a) 425 f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a)
423 f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ 426 f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫
1329 uzctotal f mf ay supf {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (uz01 ca cb) where 1332 uzctotal f mf ay supf {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (uz01 ca cb) where
1330 uz01 : {ua ub : Ordinal } → ZChainP f mf ay supf ua → ZChainP f mf ay supf ub 1333 uz01 : {ua ub : Ordinal } → ZChainP f mf ay supf ua → ZChainP f mf ay supf ub
1331 → Tri (* ua < * ub) (* ua ≡ * ub) (* ub < * ua ) 1334 → Tri (* ua < * ub) (* ua ≡ * ub) (* ub < * ua )
1332 uz01 {ua} {ub} (zchain uza uca) (zchain uzb ucb) = chain-total A f mf ay supf (proj2 uca) (proj2 ucb) 1335 uz01 {ua} {ub} (zchain uza uca) (zchain uzb ucb) = chain-total A f mf ay supf (proj2 uca) (proj2 ucb)
1333 1336
1334 usp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) 1337 msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
1335 → ( supf : Ordinal → Ordinal )
1336 → SUP A (UnionZF f mf ay supf )
1337 usp0 f mf ay supf = supP (UnionZF f mf ay supf ) (λ lt → auzc f mf ay supf lt ) (uzctotal f mf ay supf )
1338
1339 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
1340 → (zc : ZChain A f mf ay x ) 1338 → (zc : ZChain A f mf ay x )
1341 → SUP A (UnionCF A f mf ay (ZChain.supf zc) x) 1339 → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x)
1342 sp0 f mf {x} ay zc = supP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where 1340 msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where
1343 ztotal : IsTotalOrderSet (ZChain.chain zc) 1341 ztotal : IsTotalOrderSet (ZChain.chain zc)
1344 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 1342 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
1345 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 1343 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1346 uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 1344 uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb))
1345
1346 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
1347 → (zc : ZChain A f mf ay x )
1348 → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
1349 sp0 f mf ay zc = M→S (ZChain.supf zc) (msp0 f mf ay zc )
1347 1350
1348 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) 1351 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) )
1349 → ZChain.supf zc (& (SUP.sup (sp0 f mf as0 zc))) o< ZChain.supf zc (& A) 1352 → ZChain.supf zc (& (SUP.sup (sp0 f mf as0 zc))) o< ZChain.supf zc (& A)
1350 → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) 1353 → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc ))
1351 fixpoint f mf zc ss<sa = z14 where 1354 fixpoint f mf zc ss<sa = z14 where
1409 z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 )))) 1412 z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 ))))
1410 (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) ) 1413 (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
1411 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ss<sa ))) -- x ≡ f x ̄ 1414 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ss<sa ))) -- x ≡ f x ̄
1412 (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x 1415 (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x
1413 supf = ZChain.supf zc 1416 supf = ZChain.supf zc
1417 msp1 : MinSUP A (ZChain.chain zc)
1418 msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
1414 sp1 : SUP A (ZChain.chain zc) 1419 sp1 : SUP A (ZChain.chain zc)
1415 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 1420 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
1416 c = & (SUP.sup sp1) 1421 c : Ordinal
1417 z20 : c << cf nmx c 1422 c = & ( SUP.sup sp1 )
1418 z20 = proj1 (cf-is-<-monotonic nmx c (SUP.as sp1) ) 1423 mc = MinSUP.sup msp1
1419 asc : odef A (supf c) 1424 c=mc : c ≡ mc
1425 c=mc = &iso
1426 z20 : mc << cf nmx mc
1427 z20 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1) )
1428 asc : odef A (supf mc)
1420 asc = ZChain.asupf zc 1429 asc = ZChain.asupf zc
1421 spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) 1430 spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )
1422 spd = ysup (cf nmx) (cf-is-≤-monotonic nmx) asc 1431 spd = ysup (cf nmx) (cf-is-≤-monotonic nmx) asc
1423 d = MinSUP.sup spd 1432 d = MinSUP.sup spd
1424 d<A : d o< & A 1433 d<A : d o< & A
1451 -- ... | case1 eq = ? 1460 -- ... | case1 eq = ?
1452 -- ... | case2 lt = ? 1461 -- ... | case2 lt = ?
1453 -- z25 : {x : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) x → (x ≡ y ) ∨ (x << y ) 1462 -- z25 : {x : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) x → (x ≡ y ) ∨ (x << y )
1454 -- z25 {x} (init au eq ) = ? -- sup c = x, cf y ≡ d, sup c =< d 1463 -- z25 {x} (init au eq ) = ? -- sup c = x, cf y ≡ d, sup c =< d
1455 -- z25 (fsuc x lt) = ? -- cf (sup c) 1464 -- z25 (fsuc x lt) = ? -- cf (sup c)
1465
1456 sd=d : supf d ≡ d 1466 sd=d : supf d ≡ d
1457 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ 1467 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
1458 sc<sd : supf c << supf d 1468
1459 sc<sd = ? 1469 sc<<d : {mc : Ordinal } → {asc : odef A (supf mc)} → (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ))
1460 -- z21 = proj1 ( cf-is-<-monotonic nmx ? ? ) 1470 → supf mc << MinSUP.sup spd
1461 -- sco<d : supf c o< supf d 1471 sc<<d {mc} {asc} spd = z25 where
1462 -- sco<d with osuc-≡< ( ZChain.supf-<= zc (case2 sc<sd ) ) 1472 d1 : Ordinal
1463 -- ... | case1 eq = ⊥-elim ( <-irr eq sc<sd ) 1473 d1 = MinSUP.sup spd
1464 -- ... | case2 lt = lt 1474 z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
1475 z24 = MinSUP.x<sup spd (init asc refl)
1476 z25 : supf mc << d1
1477 z25 with z24
1478 ... | case2 lt = lt
1479 ... | case1 eq = ?
1480
1481 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d
1482 sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )
1483 ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd )
1484 ... | case2 lt = lt
1485
1486 sms<sa : supf mc o< supf (& A)
1487 sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) ))
1488 ... | case2 lt = lt
1489 ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} {asc} spd)) )
1490 ( ZChain.supf-mono zc (o<→≤ d<A ))))
1465 1491
1466 ss<sa : supf c o< supf (& A) 1492 ss<sa : supf c o< supf (& A)
1467 ss<sa = ? -- with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ SUP.as sp0 , lift true ⟫) )) 1493 ss<sa = subst (λ k → supf k o< supf (& A)) (sym c=mc) sms<sa
1468 -- ... | case2 lt = lt 1494
1469 -- ... | case1 eq = ? -- where
1470 zorn00 : Maximal A 1495 zorn00 : Maximal A
1471 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM 1496 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM
1472 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where 1497 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where
1473 -- yes we have the maximal 1498 -- yes we have the maximal
1474 zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) ) 1499 zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) )