Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 912:870a6b57dd39
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 12 Oct 2022 14:03:38 +0900 |
parents | 3105feb3c4e1 |
children | d5293a7c2ec4 |
comparison
equal
deleted
inserted
replaced
911:3105feb3c4e1 | 912:870a6b57dd39 |
---|---|
405 supf-< : {x y : Ordinal } → supf x o< supf y → supf x << supf y | 405 supf-< : {x y : Ordinal } → supf x o< supf y → supf x << supf y |
406 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z | 406 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z |
407 | 407 |
408 minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f mf ay supf x) | 408 minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f mf ay supf x) |
409 supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z ) | 409 supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z ) |
410 csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain | 410 csupf : {b x : Ordinal } → supf b o< x → x o≤ z → odef (UnionCF A f mf ay supf x) (supf b) -- supf z is not an element of this chain |
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 |
453 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ | 453 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ |
454 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans eq (sym (supf-is-minsup u≤z ) ) )) | 454 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans eq (sym (supf-is-minsup u≤z ) ) )) |
455 ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt ) | 455 ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt ) |
456 | 456 |
457 -- ordering is not proved here but in ZChain1 | 457 -- ordering is not proved here but in ZChain1 |
458 | |
459 -- csupf< : {a b : Ordinal } → a o≤ b → odef (UnionCF A f mf ay supf z) (supf a) → odef (UnionCF A f mf ay supf z) (supf b) | |
460 -- csupf< = ? | |
458 | 461 |
459 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) | 462 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) |
460 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where | 463 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where |
461 supf = ZChain.supf zc | 464 supf = ZChain.supf zc |
462 field | 465 field |
606 s<b : s o< b | 609 s<b : s o< b |
607 s<b = ZChain.supf-inject zc ss<sb | 610 s<b = ZChain.supf-inject zc ss<sb |
608 s≤<z : s o≤ & A | 611 s≤<z : s o≤ & A |
609 s≤<z = ordtrans s<b b≤z | 612 s≤<z = ordtrans s<b b≤z |
610 zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s) | 613 zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s) |
611 zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) | 614 zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) o≤-refl |
612 zc05 : odef (UnionCF A f mf ay supf b) (supf s) | 615 zc05 : odef (UnionCF A f mf ay supf b) (supf s) |
613 zc05 with zc04 | 616 zc05 with zc04 |
614 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ | 617 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ |
615 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ZChain.supf-inject zc zc08) is-sup fc ⟫ where | 618 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ZChain.supf-inject zc zc08) is-sup fc ⟫ where |
616 zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s | 619 zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s |
814 ... | case1 eq = case2 eq | 817 ... | case1 eq = case2 eq |
815 ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) | 818 ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) |
816 | 819 |
817 zc41 : supf0 px o< x → ZChain A f mf ay x | 820 zc41 : supf0 px o< x → ZChain A f mf ay x |
818 zc41 sfpx<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? | 821 zc41 sfpx<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? |
819 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where | 822 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupfp } where |
820 -- supf0 px is included by the chain | 823 -- supf0 px is included by the chain |
821 -- ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x | 824 -- ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x |
822 -- supf1 x ≡ sp1, which is not included now | 825 -- supf1 x ≡ sp1, which is not included now |
823 | 826 |
824 pchainpx : HOD | 827 pchainpx : HOD |
1012 s<px : s o< px | 1015 s<px : s o< px |
1013 s<px = supf-inject0 supf1-mono ss<spx | 1016 s<px = supf-inject0 supf1-mono ss<spx |
1014 sf<px : supf0 s o< px | 1017 sf<px : supf0 s o< px |
1015 sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx | 1018 sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx |
1016 csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 | 1019 csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 |
1017 csupf17 (init as refl ) = ZChain.csupf zc sf<px | 1020 csupf17 (init as refl ) = ZChain.csupf zc sf<px o≤-refl |
1018 csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) | 1021 csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) |
1019 | 1022 |
1020 ... | case2 sfp<px with ZChain.csupf zc sfp<px -- odef (UnionCF A f mf ay supf0 px) (supf0 px) | 1023 ... | case2 sfp<px with ZChain.csupf zc sfp<px o≤-refl -- odef (UnionCF A f mf ay supf0 px) (supf0 px) |
1021 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ | 1024 ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ |
1022 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u (ordtrans u≤x px<x) | 1025 ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u (ordtrans u≤x px<x) |
1023 record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ (o<→≤ u≤x) ) ⟫ where | 1026 record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ (o<→≤ u≤x) ) ⟫ where |
1024 z10 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) | 1027 z10 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) |
1025 z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x))) (ChainP.fcy<sup is-sup fc) | 1028 z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x))) (ChainP.fcy<sup is-sup fc) |
1076 -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1 | 1079 -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1 |
1077 -- z1 ≡ px , supf0 px ≡ px | 1080 -- z1 ≡ px , supf0 px ≡ px |
1078 psz1≤px : supf1 z1 o≤ px | 1081 psz1≤px : supf1 z1 o≤ px |
1079 psz1≤px = subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x | 1082 psz1≤px = subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x |
1080 cs01 : supf0 px o< px → odef (UnionCF A f mf ay supf0 px) (supf0 px) | 1083 cs01 : supf0 px o< px → odef (UnionCF A f mf ay supf0 px) (supf0 px) |
1081 cs01 spx<px = ZChain.csupf zc spx<px | 1084 cs01 spx<px = ZChain.csupf zc spx<px o≤-refl |
1082 csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) | 1085 csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) |
1083 csupf2 with trio< z1 px | inspect supf1 z1 | 1086 csupf2 with trio< z1 px | inspect supf1 z1 |
1084 csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px | 1087 csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px |
1085 ... | case2 lt = zc12 (case1 cs03) where | 1088 ... | case2 lt = zc12 (case1 cs03) where |
1086 cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) | 1089 cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) |
1087 cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) | 1090 cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) o≤-refl |
1088 ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) | 1091 ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) |
1089 ... | case1 sfz=sfpx = zc12 (case2 (init (ZChain.asupf zc) cs04 )) where | 1092 ... | case1 sfz=sfpx = zc12 (case2 (init (ZChain.asupf zc) cs04 )) where |
1090 supu=u : supf1 (supf1 z1) ≡ supf1 z1 | 1093 supu=u : supf1 (supf1 z1) ≡ supf1 z1 |
1091 supu=u = trans (cong supf1 sfz=px) (sym sfz=sfpx) | 1094 supu=u = trans (cong supf1 sfz=px) (sym sfz=sfpx) |
1092 cs04 : supf0 px ≡ supf0 z1 | 1095 cs04 : supf0 px ≡ supf0 z1 |
1096 supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩ | 1099 supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩ |
1097 supf0 z1 ∎ where open ≡-Reasoning | 1100 supf0 z1 ∎ where open ≡-Reasoning |
1098 ... | case2 sfz<sfpx = ? --- supf0 z1 o< supf0 px | 1101 ... | case2 sfz<sfpx = ? --- supf0 z1 o< supf0 px |
1099 csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) | 1102 csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) |
1100 csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } with trio< sp1 px | 1103 csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } with trio< sp1 px |
1101 ... | tri< sp1<px ¬b ¬c = ? -- sp1 o< px, supf0 sp1 ≡ supf0 px, sp1 o< z1 | 1104 ... | tri< sp1<px ¬b ¬c = ? -- sp1 o< px, supf0 sp1 o≤ px, supf0 sp1 o≤ supf0 px, sp1 o< z1 |
1102 ... | tri≈ ¬a sp1=px ¬c = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) | 1105 ... | tri≈ ¬a sp1=px ¬c = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) |
1103 record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where | 1106 record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where |
1104 -- supf1 z1 ≡ sp1, px o< z1, sp1 o< x -- sp1 o< z1 | 1107 -- supf1 z1 ≡ sp1, px o< z1, sp1 o< x -- sp1 o< z1 |
1105 -- supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1 | 1108 -- supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1 |
1106 asm : odef A (supf1 z1) | 1109 asm : odef A (supf1 z1) |
1111 supf1 px ≡⟨ cong supf1 (sym sp1=px) ⟩ | 1114 supf1 px ≡⟨ cong supf1 (sym sp1=px) ⟩ |
1112 supf1 sp1 ∎ ))) where open ≡-Reasoning | 1115 supf1 sp1 ∎ ))) where open ≡-Reasoning |
1113 supu=u : supf1 (supf1 z1) ≡ supf1 z1 | 1116 supu=u : supf1 (supf1 z1) ≡ supf1 z1 |
1114 supu=u = ? | 1117 supu=u = ? |
1115 ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) | 1118 ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) |
1119 | |
1120 csupfp : {w z : Ordinal } → supf1 w o< z → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 w) | |
1121 csupfp {w} {z} sw1<z z≤x with osuc-≡< z≤x | |
1122 ... | case1 eq = ? | |
1123 ... | case2 lt = ? where | |
1124 csupfpx : odef (UnionCF A f mf ay supf0 z) (supf0 w) | |
1125 csupfpx = ZChain.csupf zc ? ? | |
1116 | 1126 |
1117 zc4 : ZChain A f mf ay x --- x o≤ supf px | 1127 zc4 : ZChain A f mf ay x --- x o≤ supf px |
1118 zc4 with trio< x (supf0 px) | 1128 zc4 with trio< x (supf0 px) |
1119 ... | tri> ¬a ¬b c = zc41 c | 1129 ... | tri> ¬a ¬b c = zc41 c |
1120 ... | tri≈ ¬a b ¬c = ? | 1130 ... | tri≈ ¬a b ¬c = ? |