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

comparison src/zorn.agda @ 693:a3b7f1e0ca60

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
same problem again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 11 Jul 2022 11:49:11 +0900
parents 38103b4e6780
children 196eff771492
comparison
equal deleted inserted replaced
692:38103b4e6780 693:a3b7f1e0ca60
276 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where 276 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
277 field 277 field
278 psup : Ordinal → Ordinal 278 psup : Ordinal → Ordinal
279 p≤z : (x : Ordinal ) → odef A (psup x) 279 p≤z : (x : Ordinal ) → odef A (psup x)
280 chainf : (x : Ordinal) → HOD 280 chainf : (x : Ordinal) → HOD
281 is-chain : (x w : Ordinal) → (x<z : x o< z) → odef (chainf x) w → Chain A f mf ay chainf (psup x) w 281 is-chain : {x w : Ordinal} → odef (chainf x) w → Chain A f mf ay chainf (psup x) w
282 282
283 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) 283 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)
284 (zc0 : (x : Ordinal) → ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where 284 (zc0 : (x : Ordinal) → ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
285 chain : HOD 285 chain : HOD
286 chain = UnionCF A (& A) ( λ x _ → ZChain1.chainf (zc0 (& A)) x ) 286 chain = UnionCF A (& A) ( λ x _ → ZChain1.chainf (zc0 (& A)) x )
305 305
306 -- data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) : Ordinal → Ordinal → Set n where 306 -- data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) : Ordinal → Ordinal → Set n where
307 -- 307 --
308 -- data Chain is total 308 -- data Chain is total
309 309
310 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {x y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD) 310 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD)
311 {s s1 a b : Ordinal } ( ca : Chain A f mf ay chainf s a ) ( cb : Chain A f mf ay chainf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a ) 311 {s s1 a b : Ordinal } ( ca : Chain A f mf ay chainf s a ) ( cb : Chain A f mf ay chainf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
312 chain-total A f mf {x} {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where 312 chain-total A f mf {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
313 ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay chainf xa a → Chain A f mf ay chainf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a) 313 ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay chainf xa a → Chain A f mf ay chainf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
314 ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb 314 ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
315 ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where 315 ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where
316 ct00 : * a < * xb 316 ct00 : * a < * xb
317 ct00 = ChainP.fcy<sup supb fca 317 ct00 = ChainP.fcy<sup supb fca
481 sc = prev px px<x 481 sc = prev px px<x
482 pchain : HOD 482 pchain : HOD
483 pchain = chainf sc px 483 pchain = chainf sc px
484 484
485 no-ext : ZChain1 A f mf ay x 485 no-ext : ZChain1 A f mf ay x
486 no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 } where 486 no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = ? } where
487 psup1 : Ordinal → Ordinal 487 psup1 : Ordinal → Ordinal
488 psup1 z with o≤? z x 488 psup1 z with o≤? z x
489 ... | yes _ = ZChain1.psup sc z 489 ... | yes _ = ZChain1.psup sc z
490 ... | no _ = ZChain1.psup sc x 490 ... | no _ = ZChain1.psup sc x
491 p≤z1 : (z : Ordinal ) → odef A (psup1 z) 491 p≤z1 : (z : Ordinal ) → odef A (psup1 z)
515 pzc : (z : Ordinal) → z o< x → ZChain1 A f mf ay z 515 pzc : (z : Ordinal) → z o< x → ZChain1 A f mf ay z
516 pzc z z<x = prev z z<x 516 pzc z z<x = prev z z<x
517 UZ : HOD 517 UZ : HOD
518 UZ = UnionCF A x pchainf 518 UZ = UnionCF A x pchainf
519 chainf0 : (z : Ordinal ) → HOD 519 chainf0 : (z : Ordinal ) → HOD
520 chainf0 z with o≤? x z 520 chainf0 z with trio< z x
521 ... | yes _ = UZ 521 ... | tri< a ¬b ¬c = ZChain1.chainf (pzc z a) z
522 ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z 522 ... | tri≈ ¬a b ¬c = UZ
523 ... | tri> ¬a ¬b c = UZ
524 Chain-ext : {s a : Ordinal} → (ca : odef UZ a)
525 → Chain A f mf ay ( ZChain1.chainf (pzc _ (UChain.u<x (proj2 ca)))) s a → Chain A f mf ay chainf0 s a
526 Chain-ext {s} {a} ca (ch-init a x) = ch-init a x
527 Chain-ext {s} {a} ca (ch-is-sup is-sup fc) = ch-is-sup sc5 fc where
528 sc7 : odef ( ZChain1.chainf (pzc _ (UChain.u<x (proj2 ca))) s ) a
529 sc7 = ChainP.csupz is-sup
530 sc8 : (z<x : s o< x ) → chainf0 s ≡ ( ZChain1.chainf (pzc _ z<x )) s
531 sc8 z<x with trio< s x
532 ... | tri≈ ¬a b ¬c = ?
533 ... | tri> ¬a ¬b c = ?
534 ... | tri< a ¬b ¬c with o<-irr a z<x
535 ... | refl = refl
536 sc6 : odef (chainf0 s) a
537 sc6 with trio< s x
538 ... | tri≈ ¬a b ¬c = ?
539 ... | tri> ¬a ¬b c = ?
540 ... | tri< a' ¬b ¬c with o<-irr a' ? -- (UChain.u<x (proj2 ca))
541 ... | eq = ? -- ChainP.csupz is-sup
542 sc5 : ChainP A f mf ay chainf0 s a
543 sc5 = record {
544 asup = ChainP.asup is-sup
545 ; fcy<sup = ChainP.fcy<sup is-sup
546 ; csupz = sc6
547 ; order = ? }
523 total-UZ : IsTotalOrderSet UZ 548 total-UZ : IsTotalOrderSet UZ
524 total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 549 total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
525 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 550 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
526 uz01 = chain-total A f mf ay chainf0 {!!} {!!} 551 uz01 = chain-total A f mf ay chainf0
527 -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _ (UChain.chain∋z (proj2 ca))) 552 (Chain-ext ca (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) (UChain.chain∋z (proj2 ca))))
528 -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _ (UChain.chain∋z (proj2 cb))) 553 (Chain-ext cb (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) (UChain.chain∋z (proj2 cb))))
529 usup : SUP A UZ 554 usup : SUP A UZ
530 usup = supP UZ (λ lt → proj1 lt) total-UZ 555 usup = supP UZ (λ lt → proj1 lt) total-UZ
531 spu = & (SUP.sup usup) 556 spu = & (SUP.sup usup)
532 sc4 : ZChain1 A f mf ay x 557 sc4 : ZChain1 A f mf ay x
533 sc4 = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = {!!} } where 558 sc4 = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = {!!} } where