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

comparison src/zorn.agda @ 912:870a6b57dd39

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 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 = ?