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

comparison src/zorn.agda @ 704:01a88eeb9d00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 12 Jul 2022 23:05:31 +0900
parents 0278f0d151f2
children 799963f352d6
comparison
equal deleted inserted replaced
703:0278f0d151f2 704:01a88eeb9d00
475 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 475 ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
476 → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x 476 → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x
477 ind f mf {y} ay x prev with trio< y x 477 ind f mf {y} ay x prev with trio< y x
478 ... | tri> ¬a ¬b c = ? 478 ... | tri> ¬a ¬b c = ?
479 ... | tri≈ ¬a refl ¬c = ? 479 ... | tri≈ ¬a refl ¬c = ?
480 ... | tri< 0<x ¬b ¬c with Oprev-p x 480 ... | tri< y<x ¬b ¬c with Oprev-p x
481 ... | yes op = zc4 where 481 ... | yes op = zc4 where
482 -- 482 --
483 -- we have previous ordinal to use induction 483 -- we have previous ordinal to use induction
484 -- 484 --
485 px = Oprev.oprev op 485 px = Oprev.oprev op
494 pchain = UnionCF A f mf ay (ZChain.supf zc) x 494 pchain = UnionCF A f mf ay (ZChain.supf zc) x
495 ptotal : IsTotalOrderSet pchain 495 ptotal : IsTotalOrderSet pchain
496 ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 496 ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
497 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 497 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
498 uz01 = chain-total A f mf ay (ZChain.supf zc) (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 498 uz01 = chain-total A f mf ay (ZChain.supf zc) (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb))
499 psupf : Ordinal → Ordinal
500 psupf z with trio< z x
501 ... | tri< a ¬b ¬c = ZChain.supf zc z
502 ... | tri≈ ¬a b ¬c = x
503 ... | tri> ¬a ¬b c = x
504 pchain⊆A : {y : Ordinal} → odef pchain y → odef A y
505 pchain⊆A {y} ny = proj1 ny
506 pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
507 pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = ? } ⟫ where
508 afa : odef A ( f a )
509 afa = proj2 ( mf a aa )
510 fua : Chain A f mf ay psupf (UChain.u ua) (f a)
511 fua with UChain.chain∋z ua
512 ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
513 ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ ? ) (fsuc _ ? )
514 pinit : {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
515 pinit {a} ⟪ aa , ua ⟫ with UChain.chain∋z ua
516 ... | ch-init a fc = s≤fc y f mf fc
517 ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) ? where -- (s≤fc _ f mf fc) where
518 zc7 : y << psupf (UChain.u ua)
519 zc7 = ? -- ChainP.fcy<sup is-sup (init ay)
520 pcy : odef pchain y
521 pcy = ⟪ ay , record { u = y ; u<x = y<x ; chain∋z = ch-init _ (init ay) } ⟫
499 522
500 -- if previous chain satisfies maximality, we caan reuse it 523 -- if previous chain satisfies maximality, we caan reuse it
501 -- 524 --
502 no-extenion : ( {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → 525 no-extenion : ( {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
503 HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc ) ab → 526 HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc ) ab →
525 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr)) 548 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
526 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax ) 549 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
527 ... | case1 is-sup = -- x is a sup of zc 550 ... | case1 is-sup = -- x is a sup of zc
528 record { chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal 551 record { chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
529 ; initial = pinit ; chain∋init = pcy ; is-max = p-ismax } where 552 ; initial = pinit ; chain∋init = pcy ; is-max = p-ismax } where
530 psupf : Ordinal → Ordinal
531 psupf z with trio< z x
532 ... | tri< a ¬b ¬c = ZChain.supf zc z
533 ... | tri≈ ¬a b ¬c = x
534 ... | tri> ¬a ¬b c = x
535 pchain⊆A : {y : Ordinal} → odef pchain y → odef A y
536 pchain⊆A {y} ny = proj1 ny
537 pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
538 pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = ? } ⟫ where
539 afa : odef A ( f a )
540 afa = proj2 ( mf a aa )
541 fua : Chain A f mf ay psupf (UChain.u ua) (f a)
542 fua with UChain.chain∋z ua
543 ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
544 ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ ? ) (fsuc _ ? )
545 pinit : {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
546 pinit {a} ⟪ aa , ua ⟫ with UChain.chain∋z ua
547 ... | ch-init a fc = s≤fc y f mf fc
548 ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) ? where -- (s≤fc _ f mf fc) where
549 zc7 : y << psupf (UChain.u ua)
550 zc7 = ? -- ChainP.fcy<sup is-sup (init ay)
551 pcy : odef pchain y
552 pcy = ? -- ⟪ ay , record { u = y ; u<x = ∈∧P→o< ⟪ ay , lift true ⟫ ; chain∋z = ch-init _ (init ay) } ⟫
553 p-ismax : {a b : Ordinal} → odef pchain a → 553 p-ismax : {a b : Ordinal} → odef pchain a →
554 b o< osuc x → (ab : odef A b) → 554 b o< osuc x → (ab : odef A b) →
555 ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) → 555 ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) →
556 * a < * b → odef pchain b 556 * a < * b → odef pchain b
557 p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ? 557 p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ?
571 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z 571 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
572 pzc z z<x = prev z z<x 572 pzc z z<x = prev z z<x
573 psupf0 : (z : Ordinal) → Ordinal 573 psupf0 : (z : Ordinal) → Ordinal
574 psupf0 z with trio< z x 574 psupf0 z with trio< z x
575 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z 575 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
576 ... | tri≈ ¬a b ¬c = o∅ 576 ... | tri≈ ¬a b ¬c = y
577 ... | tri> ¬a ¬b c = o∅ 577 ... | tri> ¬a ¬b c = y
578 UZ : HOD 578 pchain : HOD
579 UZ = UnionCF A f mf ay psupf0 x 579 pchain = UnionCF A f mf ay psupf0 x
580 total-UZ : IsTotalOrderSet UZ 580 ptotal : IsTotalOrderSet pchain
581 total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 581 ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
582 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 582 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
583 uz01 = chain-total A f mf ay psupf0 (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 583 uz01 = chain-total A f mf ay psupf0 (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb))
584 usup : SUP A UZ 584
585 usup = supP UZ (λ lt → proj1 lt) total-UZ 585 pchain⊆A : {y : Ordinal} → odef pchain y → odef A y
586 pchain⊆A {y} ny = proj1 ny
587 pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
588 pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = ? } ⟫ where
589 afa : odef A ( f a )
590 afa = proj2 ( mf a aa )
591 fua : Chain A f mf ay psupf0 (UChain.u ua) (f a)
592 fua with UChain.chain∋z ua
593 ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
594 ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ ? ) (fsuc _ ? )
595 pinit : {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
596 pinit {a} ⟪ aa , ua ⟫ with UChain.chain∋z ua
597 ... | ch-init a fc = s≤fc y f mf fc
598 ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) ? where -- (s≤fc _ f mf fc) where
599 zc7 : y << psupf0 (UChain.u ua)
600 zc7 = ? -- ChainP.fcy<sup is-sup (init ay)
601 pcy : odef pchain y
602 pcy = ⟪ ay , record { u = y ; u<x = y<x ; chain∋z = ch-init _ (init ay) } ⟫
603
604 usup : SUP A pchain
605 usup = supP pchain (λ lt → proj1 lt) ptotal
586 spu = & (SUP.sup usup) 606 spu = & (SUP.sup usup)
587 psupf : Ordinal → Ordinal 607 psupf : Ordinal → Ordinal
588 psupf z with trio< z x 608 psupf z with trio< z x
589 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z 609 ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
590 ... | tri≈ ¬a b ¬c = spu 610 ... | tri≈ ¬a b ¬c = spu
591 ... | tri> ¬a ¬b c = spu 611 ... | tri> ¬a ¬b c = spu
612
592 zc5 : ZChain A f mf ay x 613 zc5 : ZChain A f mf ay x
593 zc5 with ODC.∋-p O A (* x) 614 zc5 with ODC.∋-p O A (* x)
594 ... | no noax = {!!} where -- ¬ A ∋ p, just skip 615 ... | no noax = {!!} where -- ¬ A ∋ p, just skip
595 ... | yes ax with ODC.p∨¬p O ( HasPrev A UZ ax f ) 616 ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )
596 -- we have to check adding x preserve is-max ZChain A y f mf x 617 -- we have to check adding x preserve is-max ZChain A y f mf x
597 ... | case1 pr = {!!} where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next 618 ... | case1 pr = {!!} where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
598 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A UZ ax ) 619 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
599 ... | case1 is-sup = {!!} -- x is a sup of (zc ?) 620 ... | case1 is-sup = {!!} -- x is a sup of (zc ?)
600 ... | case2 ¬x=sup = {!!} -- no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention 621 ... | case2 ¬x=sup = {!!} -- no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
601 622
602 623
603 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A) 624 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A)