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

comparison src/zorn.agda @ 1025:e4919cc0cfe8

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 Fri, 25 Nov 2022 23:39:04 +0900
parents ab72526316bd
children 8b3d7c461a84
comparison
equal deleted inserted replaced
1024:ab72526316bd 1025:e4919cc0cfe8
985 -- supf0 px o≤ sp1 985 -- supf0 px o≤ sp1
986 -- 986 --
987 987
988 zc41 : ZChain A f mf ay x 988 zc41 : ZChain A f mf ay x
989 zc41 with zc43 x sp1 989 zc41 with zc43 x sp1
990 zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? 990 zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono
991 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = ? } where 991 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = ? } where
992 992
993 supf1 : Ordinal → Ordinal 993 supf1 : Ordinal → Ordinal
994 supf1 z with trio< z px 994 supf1 z with trio< z px
995 ... | tri< a ¬b ¬c = supf0 z 995 ... | tri< a ¬b ¬c = supf0 z
1065 a≤px = subst (λ k → a o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x) 1065 a≤px = subst (λ k → a o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
1066 -- supf0 a ≡ px we cannot use previous cfcs, it is in the chain because 1066 -- supf0 a ≡ px we cannot use previous cfcs, it is in the chain because
1067 -- supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x 1067 -- supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
1068 z50 : odef (UnionCF A f mf ay supf1 b) w 1068 z50 : odef (UnionCF A f mf ay supf1 b) w
1069 z50 with osuc-≡< px≤sa 1069 z50 with osuc-≡< px≤sa
1070 ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 ? (subst (λ k → FClosure A f k w) z52 fc) ⟫ where 1070 ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 cp (subst (λ k → FClosure A f k w) z52 fc) ⟫ where
1071 sa≤px : supf0 a o≤ px 1071 sa≤px : supf0 a o≤ px
1072 sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x 1072 sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x
1073 z51 : supf0 px o< b 1073 z51 : supf0 px o< b
1074 z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ cong supf0 px=sa ⟩ 1074 z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ cong supf0 px=sa ⟩
1075 supf0 (supf0 a ) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ 1075 supf0 (supf0 a ) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩
1076 supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ 1076 supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩
1077 supf1 a ∎ )) sa<b where open ≡-Reasoning 1077 supf1 a ∎ )) sa<b where open ≡-Reasoning
1078 z52 : supf1 a ≡ supf1 (supf0 px) 1078 z52 : supf1 a ≡ supf1 (supf0 px)
1079 z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩ 1079 z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩
1080 supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ 1080 supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩
1081 supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩ 1081 supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩
1082 supf1 (supf0 a) ≡⟨ cong supf1 (sym (ZChain.supf-idem zc mf< a≤px sa≤px )) ⟩ 1082 supf1 (supf0 a) ≡⟨ cong supf1 (sym (ZChain.supf-idem zc mf< a≤px sa≤px )) ⟩
1083 supf1 (supf0 (supf0 a)) ≡⟨ cong (λ k → supf1 (supf0 k)) (sym px=sa) ⟩ 1083 supf1 (supf0 (supf0 a)) ≡⟨ cong (λ k → supf1 (supf0 k)) (sym px=sa) ⟩
1084 supf1 (supf0 px) ∎ where open ≡-Reasoning 1084 supf1 (supf0 px) ∎ where open ≡-Reasoning
1085 m : MinSUP A (UnionCF A f mf ay supf0 px)
1086 m = ZChain.minsup zc o≤-refl
1087 m=spx : MinSUP.sup m ≡ supf1 (supf0 px)
1088 m=spx = begin
1089 MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc o≤-refl) ⟩
1090 supf0 px ≡⟨ cong supf0 px=sa ⟩
1091 supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩
1092 supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩
1093 supf1 a ≡⟨ z52 ⟩
1094 supf1 (supf0 px) ∎ where open ≡-Reasoning
1095 z53 : supf1 (supf0 px) ≡ supf0 px
1096 z53 = begin
1097 supf1 (supf0 px) ≡⟨ sym z52 ⟩
1098 supf1 a ≡⟨ sf1=sf0 a≤px ⟩
1099 supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩
1100 supf0 (supf0 a) ≡⟨ sym ( cong supf0 px=sa ) ⟩
1101 supf0 px ∎ where open ≡-Reasoning
1102 cp : ChainP A f mf ay supf1 (supf0 px)
1103 cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ )
1104 ; order = order
1105 ; supu=u = z53 } where
1106 uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
1107 uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<px o≤-refl ss<px (subst (λ k → FClosure A f k z1)
1108 (sf1=sf0 (o<→≤ s<px)) fc ) where
1109 s<px : s o< px
1110 s<px = ZChain.supf-inject zc (osucprev ( begin
1111 osuc (supf0 s) ≡⟨ sym (cong osuc (sf1=sf0 ?) ) ⟩
1112 osuc (supf1 s) ≤⟨ osucc ss<sp ⟩
1113 supf1 (supf0 px) ≡⟨ z53 ⟩
1114 supf0 px ∎ )) where open o≤-Reasoning O
1115 ss<px : supf0 s o< px
1116 ss<px = osucprev ( begin
1117 osuc (supf0 s) ≡⟨ sym (cong osuc (sf1=sf0 ?) ) ⟩
1118 osuc (supf1 s) ≤⟨ osucc ss<sp ⟩
1119 supf1 (supf0 px) ≡⟨ sym z52 ⟩
1120 supf1 a ≡⟨ sf1=sf0 a≤px ⟩
1121 supf0 a ≡⟨ sym px=sa ⟩
1122 px ∎ ) where open o≤-Reasoning O
1123 order : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 (supf0 px) →
1124 FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf0 px)) ∨ (z1 << supf1 (supf0 px))
1125 order {s} {z} s<u fc = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m (uz s<u fc) )
1085 ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) z53 ⟫ ) where 1126 ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) z53 ⟫ ) where
1086 z53 : supf1 a o< x 1127 z53 : supf1 a o< x
1087 z53 = ordtrans<-≤ sa<b b≤x 1128 z53 = ordtrans<-≤ sa<b b≤x
1088 ... | case1 sa<px with trio< a px 1129 ... | case1 sa<px with trio< a px
1089 ... | tri< a<px ¬b ¬c = z50 where 1130 ... | tri< a<px ¬b ¬c = z50 where
1090 z50 : odef (UnionCF A f mf ay supf1 b) w 1131 z50 : odef (UnionCF A f mf ay supf1 b) w
1091 z50 with osuc-≡< b≤x 1132 z50 with osuc-≡< b≤x
1092 ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) ? fc 1133 ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc
1093 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 1134 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
1094 ... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc u≤px ) ⟫ where -- u o< px → u o< b ? 1135 ... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc u≤px ) ⟫ where -- u o< px → u o< b ?
1095 u≤px : u o≤ px 1136 u≤px : u o≤ px
1096 u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ u<b b≤x ) 1137 u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ u<b b≤x )
1097 u<x : u o< x 1138 u<x : u o< x
1232 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → 1273 ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
1233 odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 1274 odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
1234 ms01 {sup2} us P = MinSUP.minsup m us ? 1275 ms01 {sup2} us P = MinSUP.minsup m us ?
1235 1276
1236 1277
1237 zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? 1278 zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ?
1238 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs } where 1279 ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs } where
1239 1280
1240 -- supf0 px not is included by the chain 1281 -- supf0 px not is included by the chain
1241 -- supf1 x ≡ supf0 px because of supfmax 1282 -- supf1 x ≡ supf0 px because of supfmax
1242 1283
1256 -- a ≡ px -- supf0 px o< x → odef U w 1297 -- a ≡ px -- supf0 px o< x → odef U w
1257 -- supf a ≡ px -- a o< px → odef U w 1298 -- supf a ≡ px -- a o< px → odef U w
1258 -- a ≡ px → supf px ≡ px → odef U w 1299 -- a ≡ px → supf px ≡ px → odef U w
1259 1300
1260 cfcs0 : a ≡ px → odef (UnionCF A f mf ay supf0 b) w 1301 cfcs0 : a ≡ px → odef (UnionCF A f mf ay supf0 b) w
1261 cfcs0 a=px = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b ? fc1 ⟫ where 1302 cfcs0 a=px = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b cp fc1 ⟫ where
1262 spx<b : supf0 px o< b 1303 spx<b : supf0 px o< b
1263 spx<b = subst (λ k → supf0 k o< b) a=px sa<b 1304 spx<b = subst (λ k → supf0 k o< b) a=px sa<b
1264 cs01 : supf0 a ≡ supf0 (supf0 px) 1305 cs01 : supf0 a ≡ supf0 (supf0 px)
1265 cs01 = trans (cong supf0 a=px) ( sym ( ZChain.supf-idem zc mf< o≤-refl 1306 cs01 = trans (cong supf0 a=px) ( sym ( ZChain.supf-idem zc mf< o≤-refl
1266 (subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ spx<b b≤x)))) 1307 (subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ spx<b b≤x))))
1267 fc1 : FClosure A f (supf0 (supf0 px)) w 1308 fc1 : FClosure A f (supf0 (supf0 px)) w
1268 fc1 = subst (λ k → FClosure A f k w) cs01 fc 1309 fc1 = subst (λ k → FClosure A f k w) cs01 fc
1310 m : MinSUP A (UnionCF A f mf ay supf0 (supf0 px))
1311 m = ZChain.minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x))
1312 m=sa : MinSUP.sup m ≡ supf0 (supf0 px)
1313 m=sa = begin
1314 MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x) )) ⟩
1315 supf0 (supf0 px) ∎ where open ≡-Reasoning
1316 cp : ChainP A f mf ay supf0 (supf0 px)
1317 cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ )
1318 ; order = order
1319 ; supu=u = sym (trans (cong supf0 (sym a=px)) cs01) } where
1320 uz : {s z1 : Ordinal } → supf0 s o< supf0 (supf0 px) → FClosure A f (supf0 s) z1
1321 → odef (UnionCF A f mf ay supf0 (supf0 px)) z1
1322 uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<spx spx≤px
1323 (subst (λ k → supf0 s o< k) (sym (trans (cong supf0 (sym a=px)) cs01) ) ss<sp) fc where
1324 s<spx : s o< supf0 px
1325 s<spx = ZChain.supf-inject zc ss<sp
1326 spx≤px : supf0 px o≤ px
1327 spx≤px = zc-b<x _ (ordtrans<-≤ spx<b b≤x)
1328 order : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 (supf0 px) →
1329 FClosure A f (supf0 s) z1 → (z1 ≡ supf0 (supf0 px)) ∨ (z1 << supf0 (supf0 px))
1330 order {s} {z} s<u fc = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m (uz s<u fc) )
1269 1331
1270 1332
1271 cfcs1 : odef (UnionCF A f mf ay supf0 b) w 1333 cfcs1 : odef (UnionCF A f mf ay supf0 b) w
1272 cfcs1 with trio< a px 1334 cfcs1 with trio< a px
1273 ... | tri< a<px ¬b ¬c = cfcs2 where 1335 ... | tri< a<px ¬b ¬c = cfcs2 where
1277 cfcs2 with trio< (supf0 a) px 1339 cfcs2 with trio< (supf0 a) px
1278 ... | tri< sa<x ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) 1340 ... | tri< sa<x ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b)
1279 ( ZChain.cfcs zc mf< a<px o≤-refl sa<x fc ) 1341 ( ZChain.cfcs zc mf< a<px o≤-refl sa<x fc )
1280 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ sa<x) ⟫ ) 1342 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ sa<x) ⟫ )
1281 ... | tri≈ ¬a sa=px ¬c with trio< a px 1343 ... | tri≈ ¬a sa=px ¬c with trio< a px
1282 ... | tri< a<px ¬b ¬c = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b ? fc1 ⟫ where 1344 ... | tri< a<px ¬b ¬c = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b cp fc1 ⟫ where
1283 cs01 : supf0 a ≡ supf0 (supf0 a) 1345 cs01 : supf0 a ≡ supf0 (supf0 a)
1284 cs01 = sym ( ZChain.supf-idem zc mf< (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x))) 1346 cs01 = sym ( ZChain.supf-idem zc mf< (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x)))
1285 fc1 : FClosure A f (supf0 (supf0 a)) w 1347 fc1 : FClosure A f (supf0 (supf0 a)) w
1286 fc1 = subst (λ k → FClosure A f k w) cs01 fc 1348 fc1 = subst (λ k → FClosure A f k w) cs01 fc
1349 m : MinSUP A (UnionCF A f mf ay supf0 (supf0 a))
1350 m = ZChain.minsup zc (o≤-refl0 sa=px)
1351 m=sa : MinSUP.sup m ≡ supf0 (supf0 a)
1352 m=sa = begin
1353 MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (o≤-refl0 sa=px) ) ⟩
1354 supf0 (supf0 a) ∎ where open ≡-Reasoning
1355 cp : ChainP A f mf ay supf0 (supf0 a)
1356 cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ )
1357 ; order = order
1358 ; supu=u = sym cs01 } where
1359 uz : {s z1 : Ordinal } → supf0 s o< supf0 (supf0 a) → FClosure A f (supf0 s) z1
1360 → odef (UnionCF A f mf ay supf0 (supf0 a)) z1
1361 uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< (ZChain.supf-inject zc ss<sp)
1362 (zc-b<x _ (ordtrans<-≤ sa<b b≤x)) ss<sa fc where
1363 ss<sa : supf0 s o< supf0 a
1364 ss<sa = subst (λ k → supf0 s o< k ) (sym cs01) ss<sp
1365 order : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 (supf0 a) →
1366 FClosure A f (supf0 s) z1 → (z1 ≡ supf0 (supf0 a)) ∨ (z1 << supf0 (supf0 a))
1367 order {s} {z} s<u fc = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m (uz s<u fc) )
1287 ... | tri≈ ¬a a=px ¬c = cfcs0 a=px 1368 ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
1288 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ (ordtrans<-≤ a<b b≤x) ) ⟫ ) 1369 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ (ordtrans<-≤ a<b b≤x) ) ⟫ )
1289 ... | tri≈ ¬a a=px ¬c = cfcs0 a=px 1370 ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
1290 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (zc-b<x _ (ordtrans<-≤ a<b b≤x)) c ) 1371 ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (zc-b<x _ (ordtrans<-≤ a<b b≤x)) c )
1291 1372