Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 920:a2f8d14012aa
fixpoint?
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 16 Oct 2022 17:26:49 +0900 |
parents | 213f12f27003 |
children | c0cf2b383064 |
comparison
equal
deleted
inserted
replaced
919:213f12f27003 | 920:a2f8d14012aa |
---|---|
570 cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) → odef A x → ( * x < * (cf nmx x) ) ∧ odef A (cf nmx x ) | 570 cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) → odef A x → ( * x < * (cf nmx x) ) ∧ odef A (cf nmx x ) |
571 cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫ | 571 cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫ |
572 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) | 572 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) |
573 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ | 573 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ |
574 | 574 |
575 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) | |
576 (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc) | |
577 sp0 f mf ay zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ztotal where | |
578 ztotal : IsTotalOrderSet (ZChain.chain zc) | |
579 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where | |
580 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) | |
581 uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) | |
582 | |
583 -- | 575 -- |
584 -- Second TransFinite Pass for maximality | 576 -- Second TransFinite Pass for maximality |
585 -- | 577 -- |
586 | 578 |
587 SZ1 : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) | 579 SZ1 : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) |
588 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x | 580 {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x |
589 SZ1 f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where | 581 SZ1 f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where |
590 chain-mono1 : {a b c : Ordinal} → a o≤ b | 582 chain-mono1 : {a b c : Ordinal} → a o≤ b |
591 → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c | 583 → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c |
592 chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b | 584 chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b |
593 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → | 585 is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (ab : odef A b) |
594 ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → | 586 → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f |
595 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f → | 587 → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b |
596 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b | 588 is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev |
597 is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev | |
598 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ | 589 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ |
599 ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) | 590 ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) |
600 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ | 591 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ |
601 | 592 |
602 supf = ZChain.supf zc | 593 supf = ZChain.supf zc |
603 | 594 |
604 csupf-fc : {b s z1 : Ordinal} → b o≤ & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 | 595 csupf-fc : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 |
605 csupf-fc {b} {s} {z1} b≤z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where | 596 csupf-fc {b} {s} {z1} b<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where |
606 s<b : s o< b | 597 s<b : s o< b |
607 s<b = ZChain.supf-inject zc ss<sb | 598 s<b = ZChain.supf-inject zc ss<sb |
608 s≤<z : s o≤ & A | 599 s<z : s o< & A |
609 s≤<z = ordtrans s<b b≤z | 600 s<z = ordtrans s<b b<z |
610 zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s) | 601 zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s) |
611 zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) | 602 zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) |
612 zc05 : odef (UnionCF A f mf ay supf b) (supf s) | 603 zc05 : odef (UnionCF A f mf ay supf b) (supf s) |
613 zc05 with zc04 | 604 zc05 with zc04 |
614 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ | 605 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ |
625 ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ | 616 ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ |
626 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ | 617 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ |
627 order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) | 618 order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) |
628 order {b} {s} {z1} b<z ss<sb fc = zc04 where | 619 order {b} {s} {z1} b<z ss<sb fc = zc04 where |
629 zc00 : ( z1 ≡ MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1 << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) ) | 620 zc00 : ( z1 ≡ MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1 << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) ) |
630 zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤ b<z) ) (subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc (o<→≤ b<z) ss<sb fc )) | 621 zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤ b<z) ) (subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc b<z ss<sb fc )) |
631 -- supf (supf b) ≡ supf b | 622 -- supf (supf b) ≡ supf b |
632 zc04 : (z1 ≡ supf b) ∨ (z1 << supf b) | 623 zc04 : (z1 ≡ supf b) ∨ (z1 << supf b) |
633 zc04 with zc00 | 624 zc04 with zc00 |
634 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z)) ) eq ) | 625 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z)) ) eq ) |
635 ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt ) | 626 ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt ) |
643 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → | 634 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → |
644 ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → | 635 ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → |
645 HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab → | 636 HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab → |
646 * a < * b → odef (UnionCF A f mf ay supf x) b | 637 * a < * b → odef (UnionCF A f mf ay supf x) b |
647 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P | 638 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P |
648 is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b | 639 is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b |
649 is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup | 640 is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup |
650 = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where | 641 = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where |
651 b<A : b o< & A | 642 b<A : b o< & A |
652 b<A = z09 ab | 643 b<A = z09 ab |
653 b<x : b o< x | 644 b<x : b o< x |
669 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → | 660 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → |
670 ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → | 661 ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → |
671 HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab → | 662 HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab → |
672 * a < * b → odef (UnionCF A f mf ay supf x) b | 663 * a < * b → odef (UnionCF A f mf ay supf x) b |
673 is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P | 664 is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P |
674 is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua sb<sx ab has-prev a<b | 665 is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b |
675 is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay ) | 666 is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay ) |
676 ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ | 667 ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ |
677 ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where | 668 ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where |
678 m09 : b o< & A | 669 m09 : b o< & A |
679 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) | 670 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) |
695 m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = m05 } | 686 m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = m05 } |
696 | 687 |
697 --- | 688 --- |
698 --- the maximum chain has fix point of any ≤-monotonic function | 689 --- the maximum chain has fix point of any ≤-monotonic function |
699 --- | 690 --- |
691 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) | |
692 (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc) | |
693 sp0 f mf {x} ay zc = ZChain.sup zc o≤-refl | |
694 | |
700 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) | 695 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) |
701 → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) | 696 → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) |
702 fixpoint f mf zc = z14 where | 697 fixpoint f mf zc = z14 where |
703 chain = ZChain.chain zc | 698 chain = ZChain.chain zc |
704 supf = ZChain.supf zc | 699 supf = ZChain.supf zc |
706 sp1 = sp0 f mf as0 zc | 701 sp1 = sp0 f mf as0 zc |
707 z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) | 702 z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) |
708 → HasPrev A chain b f ∨ IsSup A chain {b} ab | 703 → HasPrev A chain b f ∨ IsSup A chain {b} ab |
709 → * a < * b → odef chain b | 704 → * a < * b → odef chain b |
710 z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) | 705 z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) |
706 z22 : & (SUP.sup sp1) o< & A | |
707 z22 = c<→o< ( SUP.as sp1 ) | |
711 z21 : supf (& (SUP.sup sp1)) o< supf (& A) | 708 z21 : supf (& (SUP.sup sp1)) o< supf (& A) |
712 z21 = ? | 709 z21 = ? |
713 -- z21 : supf (& (SUP.sup sp1)) o< & A | 710 -- z21 : supf (& (SUP.sup sp1)) o< & A |
714 -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) )) | 711 -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) )) |
715 z12 : odef chain (& (SUP.sup sp1)) | 712 z12 : odef chain (& (SUP.sup sp1)) |
716 z12 with o≡? (& s) (& (SUP.sup sp1)) | 713 z12 with o≡? (& s) (& (SUP.sup sp1)) |
717 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) | 714 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) |
718 ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1) | 715 ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1) |
719 (case2 z19 ) z13 where | 716 (case2 z19 ) z13 where |
720 z13 : * (& s) < * (& (SUP.sup sp1)) | 717 z13 : * (& s) < * (& (SUP.sup sp1)) |
721 z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc ) | 718 z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc ) |
722 ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) | 719 ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) |
723 ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt | 720 ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt |
729 ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) | 726 ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) |
730 ztotal : IsTotalOrderSet (ZChain.chain zc) | 727 ztotal : IsTotalOrderSet (ZChain.chain zc) |
731 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where | 728 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where |
732 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) | 729 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) |
733 uz01 = chain-total A f mf as0 supf ( (proj2 ca)) ( (proj2 cb)) | 730 uz01 = chain-total A f mf as0 supf ( (proj2 ca)) ( (proj2 cb)) |
734 | |
735 z14 : f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) | 731 z14 : f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) |
736 z14 with ztotal (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 | 732 z14 with ztotal (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 |
737 ... | tri< a ¬b ¬c = ⊥-elim z16 where | 733 ... | tri< a ¬b ¬c = ⊥-elim z16 where |
738 z16 : ⊥ | 734 z16 : ⊥ |
739 z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 )) | 735 z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 )) |