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

comparison src/zorn.agda @ 869:1ca338c3f09c

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, 13 Sep 2022 15:26:19 +0900
parents 35a884f2bfde
children f9fc8da87b5a
comparison
equal deleted inserted replaced
868:35a884f2bfde 869:1ca338c3f09c
445 sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x) 445 sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x)
446 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z 446 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
447 → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 447 → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b
448 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) ) 448 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
449 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y 449 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y
450 order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) 450 csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b)
451
451 452
452 chain∋init : odef chain y 453 chain∋init : odef chain y
453 chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ 454 chain∋init = ⟪ ay , ch-init (init ay refl) ⟫
454 f-next : {a : Ordinal} → odef chain a → odef chain (f a) 455 f-next : {a : Ordinal} → odef chain a → odef chain (f a)
455 f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ 456 f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫
485 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt ) 486 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
486 487
487 488
488 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 489 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
489 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where 490 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
491 supf = ZChain.supf zc
490 field 492 field
491 is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) z) a ) → b o< z → (ab : odef A b) 493 order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
492 → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) z) b f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) z) ab 494 is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z → (ab : odef A b)
493 → * a < * b → odef ((UnionCF A f mf ay (ZChain.supf zc) z)) b 495 → HasPrev A (UnionCF A f mf ay supf z) b f ∨ IsSup A (UnionCF A f mf ay supf z) ab
496 → * a < * b → odef ((UnionCF A f mf ay supf z)) b
494 497
495 initial-segment : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 498 initial-segment : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
496 {a b y : Ordinal} (ay : odef A y) (za : ZChain A f mf ay a ) (zb : ZChain A f mf ay b ) 499 {a b y : Ordinal} (ay : odef A y) (za : ZChain A f mf ay a ) (zb : ZChain A f mf ay b )
497 → {z : Ordinal } → a o≤ b → z o≤ a 500 → {z : Ordinal } → a o≤ b → z o≤ a
498 → ZChain.supf za z ≡ ZChain.supf zb z 501 → ZChain.supf za z ≡ ZChain.supf zb z
620 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 623 ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫
621 ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , 624 ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab ,
622 subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) 625 subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
623 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ 626 (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫
624 627
625 supf1 = ZChain.supf zc 628 supf = ZChain.supf zc
629
630 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
631 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
632 s<b : s o< b
633 s<b = ZChain.supf-inject zc ss<sb
634 s≤<z : s o≤ & A
635 s≤<z = ordtrans s<b b≤z
636 zc04 : odef (UnionCF A f mf ay supf (supf s)) (supf s)
637 zc04 = ? ZChain.csupf zc ?
638 zc03 : odef (UnionCF A f mf ay supf (& A)) (supf s)
639 zc03 = ZChain.csupf zc ?
640 zc05 : odef (UnionCF A f mf ay supf b) (supf s)
641 zc05 with zc04
642 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫
643 ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 u<x ) is-sup fc ⟫ where
644 zc06 : supf u ≡ u
645 zc06 = ChainP.supu=u is-sup
646 zc09 : u o< supf s → u o< b
647 zc09 u<s = ordtrans (ZChain.supf-inject zc (subst (λ k → k o< supf s) (sym zc06) u<s)) s<b
648 csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where
649 zc04 : odef (UnionCF A f mf ay supf b) (f x)
650 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc )
651 ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫
652 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
653 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)
654 order {b} {s} {z1} b<z ss<sb fc = zc04 where
655 zc00 : ( * z1 ≡ SUP.sup (ZChain.sup zc (o<→≤ b<z) )) ∨ ( * z1 < SUP.sup ( ZChain.sup zc (o<→≤ b<z) ) )
656 zc00 = SUP.x<sup (ZChain.sup zc (o<→≤ b<z) ) (csupf-fc (o<→≤ b<z) ss<sb fc )
657 zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
658 zc04 with zc00
659 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-sup zc (o<→≤ b<z)) ) (cong (&) eq) )
660 ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-sup zc (o<→≤ b<z) ) ))) lt )
626 661
627 zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x 662 zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
628 zc1 x prev with Oprev-p x 663 zc1 x prev with Oprev-p x
629 ... | yes op = record { is-max = is-max } where 664 ... | yes op = record { is-max = is-max } where
630 px = Oprev.oprev op 665 px = Oprev.oprev op
631 zc-b<x : {b : Ordinal } → b o< x → b o< osuc px 666 zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
632 zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 667 zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt
633 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → 668 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
634 b o< x → (ab : odef A b) → 669 b o< x → (ab : odef A b) →
635 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab → 670 HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
636 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b 671 * a < * b → odef (UnionCF A f mf ay supf x) b
637 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P 672 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 | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b 673 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 | case2 is-sup 674 is-max {a} {b} ua b<x ab P a<b | case2 is-sup
640 = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where 675 = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫ where
641 b<A : b o< & A 676 b<A : b o< & A
642 b<A = z09 ab 677 b<A = z09 ab
643 m04 : ¬ HasPrev A (UnionCF A f mf ay (ZChain.supf zc) b) b f 678 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
644 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) 679 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp)
645 ; x=fy = HasPrev.x=fy nhp } ) 680 ; x=fy = HasPrev.x=fy nhp } )
646 m05 : ZChain.supf zc b ≡ b 681 m05 : ZChain.supf zc b ≡ b
647 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) 682 m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) )
648 ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz ) } , m04 ⟫ 683 ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz ) } , m04 ⟫
649 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b 684 m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
650 m08 {z} fcz = ZChain.fcy<sup zc b<A fcz 685 m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
651 m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 686 m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
652 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b 687 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
653 m09 {s} {z} s<b fcz = ZChain.order zc b<A s<b fcz 688 m09 {s} {z} s<b fcz = order b<A s<b fcz
654 m06 : ChainP A f mf ay (ZChain.supf zc) b 689 m06 : ChainP A f mf ay supf b
655 m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = m05 } 690 m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = m05 }
656 ... | no lim = record { is-max = is-max } where 691 ... | no lim = record { is-max = is-max } where
657 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → 692 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
658 b o< x → (ab : odef A b) → 693 b o< x → (ab : odef A b) →
659 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab → 694 HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
660 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b 695 * a < * b → odef (UnionCF A f mf ay supf x) b
661 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P 696 is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
662 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 697 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
663 is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay ) 698 is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSup.x<sup (proj2 is-sup) (init-uchain A f mf ay )
664 ... | 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 )) ⟫ 699 ... | 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 )) ⟫
665 ... | case2 y<b = chain-mono1 (osucc b<x) 700 ... | case2 y<b = chain-mono1 (osucc b<x)
668 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) 703 m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
669 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b 704 m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
670 m07 {z} fc = ZChain.fcy<sup zc m09 fc 705 m07 {z} fc = ZChain.fcy<sup zc m09 fc
671 m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 706 m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
672 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b 707 → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
673 m08 {s} {z1} s<b fc = ZChain.order zc m09 s<b fc 708 m08 {s} {z1} s<b fc = order m09 s<b fc
674 m04 : ¬ HasPrev A (UnionCF A f mf ay (ZChain.supf zc) b) b f 709 m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
675 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) 710 m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp)
676 ; x=fy = HasPrev.x=fy nhp } ) 711 ; x=fy = HasPrev.x=fy nhp } )
677 m05 : ZChain.supf zc b ≡ b 712 m05 : ZChain.supf zc b ≡ b
678 m05 = ZChain.sup=u zc ab (o<→≤ m09) 713 m05 = ZChain.sup=u zc ab (o<→≤ m09)
679 ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )} , m04 ⟫ -- ZChain on x 714 ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )} , m04 ⟫ -- ZChain on x
680 m06 : ChainP A f mf ay (ZChain.supf zc) b 715 m06 : ChainP A f mf ay supf b
681 m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = m05 } 716 m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = m05 }
682 717
683 --- 718 ---
684 --- the maximum chain has fix point of any ≤-monotonic function 719 --- the maximum chain has fix point of any ≤-monotonic function
685 --- 720 ---
782 px<x : px o< x 817 px<x : px o< x
783 px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 818 px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
784 zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px 819 zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
785 zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 820 zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt
786 821
787 pchain : HOD
788 pchain = UnionCF A f mf ay (ZChain.supf zc) px
789
790 supf0 = ZChain.supf zc 822 supf0 = ZChain.supf zc
791 823 pchain : HOD
824 pchain = UnionCF A f mf ay supf0 px
792 pchain1 : HOD 825 pchain1 : HOD
793 pchain1 = UnionCF A f mf ay supf0 x 826 pchain1 = UnionCF A f mf ay supf0 x
794 827
795 supfx : {z : Ordinal } → x o≤ z → supf0 px ≡ supf0 z 828 supfx : {z : Ordinal } → x o≤ z → supf0 px ≡ supf0 z
796 supfx {z} x≤z with trio< z px 829 supfx {z} x≤z with trio< z px
822 -- UninCF supf0 x supf0 px is included 855 -- UninCF supf0 x supf0 px is included
823 -- supf0 px ≡ px 856 -- supf0 px ≡ px
824 -- supf0 px ≡ supf0 x 857 -- supf0 px ≡ supf0 x
825 858
826 no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f) → ZChain A f mf ay x 859 no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f) → ZChain A f mf ay x
827 no-extension P = record { supf = supf0 ; asupf = ? ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 860 no-extension P = record { supf = supf0 ; asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono
828 ; order = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where 861 ; order = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where
829 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z 862 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
830 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 863 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
831 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup fc ⟫ 864 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup fc ⟫
832 zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ (HasPrev A pchain x f ) 865 zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ (HasPrev A pchain x f )