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

comparison src/zorn.agda @ 1063:091e7a80bfe3

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 Mon, 12 Dec 2022 07:24:45 +0900
parents 88731edfa691
children 77740070e008
comparison
equal deleted inserted replaced
1062:88731edfa691 1063:091e7a80bfe3
281 = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ; 281 = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ;
282 odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } 282 odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
283 283
284 -- Union of chain lower than x 284 -- Union of chain lower than x
285 285
286 record IChain {A : HOD} { f : Ordinal → Ordinal } {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where 286 data IChain {A : HOD} { f : Ordinal → Ordinal } {y : Ordinal } (ay : odef A y )
287 field 287 {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) : (z : Ordinal ) → Set n where
288 i : Ordinal 288 ic-init : {z : Ordinal } (fc : FClosure A f y z) → IChain ay supfz z
289 i<x : i o< x 289 ic-isup : {z : Ordinal} (i : Ordinal) (i<x : i o< x) (s<x : supfz i<x o≤ i ) (fc : FClosure A f (supfz i<x) z) → IChain ay supfz z
290 s<x : supfz i<x o≤ i 290
291 fc : FClosure A f (supfz i<x) z 291 UnionIC : ( A : HOD ) ( f : Ordinal → Ordinal ) { x : Ordinal } {y : Ordinal } (ay : odef A y ) (supfz : {z : Ordinal } → z o< x → Ordinal) → HOD
292 292 UnionIC A f ay supfz
293 UnionIC : ( A : HOD ) ( f : Ordinal → Ordinal ) { x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) → HOD 293 = record { od = record { def = λ z → odef A z ∧ IChain {A} {f} ay supfz z } ;
294 UnionIC A f supfz
295 = record { od = record { def = λ z → odef A z ∧ IChain {A} {f} supfz z } ;
296 odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } 294 odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
297 295
298 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) 296 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y )
299 → supf x o< supf y → x o< y 297 → supf x o< supf y → x o< y
300 supf-inject0 {x} {y} {supf} supf-mono sx<sy with trio< x y 298 supf-inject0 {x} {y} {supf} supf-mono sx<sy with trio< x y
1265 1263
1266 supfz : {z : Ordinal } → z o< x → Ordinal 1264 supfz : {z : Ordinal } → z o< x → Ordinal
1267 supfz {z} z<x = ZChain.supf (pzc (ob<x lim z<x)) z 1265 supfz {z} z<x = ZChain.supf (pzc (ob<x lim z<x)) z
1268 1266
1269 pchainx : HOD 1267 pchainx : HOD
1270 pchainx = UnionIC A f supfz 1268 pchainx = UnionIC A f ay supfz
1271 1269
1272 zeq : {xa xb z : Ordinal } 1270 zeq : {xa xb z : Ordinal }
1273 → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa 1271 → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa
1274 → ZChain.supf (pzc xa<x) z ≡ ZChain.supf (pzc xb<x) z 1272 → ZChain.supf (pzc xa<x) z ≡ ZChain.supf (pzc xb<x) z
1275 zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa = supf-unique A f mf< ay xa≤xb 1273 zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa = supf-unique A f mf< ay xa≤xb
1276 (pzc xa<x) (pzc xb<x) z≤xa 1274 (pzc xa<x) (pzc xb<x) z≤xa
1277 1275
1278 iceq : {ix iy : Ordinal } → ix ≡ iy → {i<x : ix o< x } {i<y : iy o< x } → supfz i<x ≡ supfz i<y 1276 iceq : {ix iy : Ordinal } → ix ≡ iy → {i<x : ix o< x } {i<y : iy o< x } → supfz i<x ≡ supfz i<y
1279 iceq refl = cong supfz o<-irr 1277 iceq refl = cong supfz o<-irr
1280 1278
1281 ifc≤ : {za zb : Ordinal } ( ia : IChain supfz za ) ( ib : IChain supfz zb ) → (ia≤ib : IChain.i ia o≤ IChain.i ib ) 1279 IChain-i : {z : Ordinal } → IChain ay supfz z → Ordinal
1282 → FClosure A f (ZChain.supf (pzc (ob<x lim (IChain.i<x ib))) (IChain.i ia)) za 1280 IChain-i (ic-init fc) = o∅
1283 ifc≤ {za} {zb} ia ib ia≤ib = subst (λ k → FClosure A f k _ ) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc) ) (IChain.fc ia) 1281 IChain-i (ic-isup ia ia<x sa<x fca) = ia
1284 1282
1285 pic<x : {z : Ordinal } → (ic : IChain supfz z ) → osuc (IChain.i ic) o< x 1283 pic<x : {z : Ordinal } → (ic : IChain ay supfz z ) → osuc (IChain-i ic) o< x
1286 pic<x {z} ic = ob<x lim (IChain.i<x ic) 1284 pic<x {z} (ic-init fc) = ob<x lim 0<x -- 0<x ∧ lim x → osuc o∅ o< x
1285 pic<x {z} (ic-isup ia ia<x sa<x fca) = ob<x lim ia<x
1286
1287 ifc≤ : {za zb : Ordinal } ( ia : IChain ay supfz za ) ( ib : IChain ay supfz zb ) → (ia≤ib : IChain-i ia o≤ IChain-i ib )
1288 → FClosure A f (ZChain.supf (pzc (ob<x lim (pic<x ib))) (IChain-i ia)) za
1289 ifc≤ {za} {zb} (ic-isup ia ia<x sa<x fca) (ic-isup ib ib<x sb<x fcb) ia≤ib
1290 = subst (λ k → FClosure A f k _ ) (zeq _ _ ? (o<→≤ <-osuc) ) fca
1291 ifc≤ {za} {zb} ia ib ia≤ib = ?
1287 1292
1288 pchainx⊆chain : {z : Ordinal } → (pz : odef pchainx z) → odef (ZChain.chain (pzc (pic<x (proj2 pz)))) z 1293 pchainx⊆chain : {z : Ordinal } → (pz : odef pchainx z) → odef (ZChain.chain (pzc (pic<x (proj2 pz)))) z
1289 pchainx⊆chain {z} ⟪ aw , ic ⟫ = ZChain.cfcs (pzc (pic<x ic) ) <-osuc o≤-refl uz03 (IChain.fc ic) where 1294 pchainx⊆chain {z} ⟪ aw , ic-init fc ⟫ = ⟪ aw , ch-init fc ⟫
1290 uz02 : FClosure A f (ZChain.supf (pzc (pic<x ic )) (IChain.i ic)) z 1295 pchainx⊆chain {z} ⟪ aw , (ic-isup ia ia<x sa<x fca) ⟫ = ZChain.cfcs (pzc (ob<x lim ia<x) ) <-osuc o≤-refl uz03 fca where
1291 uz02 = IChain.fc ic 1296 uz02 : FClosure A f (ZChain.supf (pzc (ob<x lim ia<x)) ia ) z
1292 uz03 : ZChain.supf (pzc (pic<x ic)) (IChain.i ic) o≤ IChain.i ic 1297 uz02 = fca
1293 uz03 = IChain.s<x ic 1298 uz03 : ZChain.supf (pzc (ob<x lim ia<x)) ia o≤ ia
1294 1299 uz03 = sa<x
1295 chain⊆pchainx : {z : Ordinal } → (z<x : z o< x) → odef (ZChain.chain (pzc (ob<x lim z<x))) z → odef pchainx z 1300
1296 chain⊆pchainx {z} z<x ⟪ ua , ch-init fc ⟫ = ⟪ ua , record { i = o∅ ; i<x = ? ; s<x = ? ; fc = ? } ⟫ 1301 chain⊆pchainx : {z w : Ordinal } → (oz<x : osuc z o< x) → odef (ZChain.chain (pzc oz<x)) w → odef pchainx w
1297 chain⊆pchainx {z} z<x ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , record { i = ? ; i<x = ? ; s<x = ? 1302 chain⊆pchainx {z} {w} oz<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫
1298 ; fc = subst (λ k → FClosure A f k z ) ? fc } ⟫ 1303 chain⊆pchainx {z} {w} oz<x ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = ⟪ aw , ic-isup u ? ? (subst (λ k → FClosure A f k w ) ? fc ) ⟫ where
1304 z<x : z o< x
1305 z<x = ordtrans <-osuc oz<x
1299 1306
1300 ptotalx : IsTotalOrderSet pchainx 1307 ptotalx : IsTotalOrderSet pchainx
1301 ptotalx {a} {b} ⟪ _ , ia ⟫ ⟪ _ , ib ⟫ = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 1308 ptotalx {a} {b} ⟪ _ , ia ⟫ ⟪ _ , ib ⟫ = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
1302 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 1309 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1303 uz01 with trio< (supfz (IChain.i<x ia)) (supfz (IChain.i<x ib)) 1310 uz01 with trio< (supfz (pic<x ia)) (supfz (pic<x ib))
1304 ... | tri< ia<ib ¬b ¬c with 1311 ... | tri< ia<ib ¬b ¬c with
1305 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ? (ifc≤ ia ib (o<→≤ ?))) (s≤fc _ f mf (IChain.fc ib)) 1312 ≤-ftrans (ZChain.order (pzc (ob<x lim (pic<x ib))) ? ? (ifc≤ ia ib (o<→≤ ?))) (s≤fc _ f mf ?)
1306 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where 1313 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
1307 ct00 : * (& a) ≡ * (& b) 1314 ct00 : * (& a) ≡ * (& b)
1308 ct00 = cong (*) eq1 1315 ct00 = cong (*) eq1
1309 ... | case2 lt = tri< lt (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1) 1316 ... | case2 lt = tri< lt (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)
1310 uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym ia=ib) (IChain.fc ib)) 1317 uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf ? (subst (λ k → FClosure A f k (& b)) (sym ia=ib) ?)
1311 uz01 | tri> ¬a ¬b ib<ia with 1318 uz01 | tri> ¬a ¬b ib<ia with
1312 ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ? (ifc≤ ib ia (o<→≤ ?))) (s≤fc _ f mf (IChain.fc ia)) 1319 ≤-ftrans (ZChain.order (pzc (ob<x lim (pic<x ia))) ? ? (ifc≤ ib ia (o<→≤ ?))) (s≤fc _ f mf ?)
1313 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where 1320 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
1314 ct00 : * (& a) ≡ * (& b) 1321 ct00 : * (& a) ≡ * (& b)
1315 ct00 = sym (cong (*) eq1) 1322 ct00 = sym (cong (*) eq1)
1316 ... | case2 lt = tri> (λ lt1 → <-irr (case2 lt) lt1) (λ eq → <-irr (case1 eq) lt) lt 1323 ... | case2 lt = tri> (λ lt1 → <-irr (case2 lt) lt1) (λ eq → <-irr (case1 eq) lt) lt
1317 1324
1318 usup : MinSUP A pchainx 1325 usup : MinSUP A pchainx
1319 usup = minsupP pchainx (λ ic → A∋fc _ f mf (IChain.fc (proj2 ic) ) ) ptotalx 1326 usup = minsupP pchainx (λ ic → ? ) ptotalx
1320 spu = MinSUP.sup usup 1327 spu = MinSUP.sup usup
1321 1328
1322 supf1 : Ordinal → Ordinal 1329 supf1 : Ordinal → Ordinal
1323 supf1 z with trio< z x 1330 supf1 z with trio< z x
1324 ... | tri< a ¬b ¬c = ZChain.supf (pzc (ob<x lim a)) z 1331 ... | tri< a ¬b ¬c = ZChain.supf (pzc (ob<x lim a)) z