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

comparison src/zorn.agda @ 924:a48dc906796c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
supf usp0 instead of supf (& A) ?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 19 Oct 2022 09:10:27 +0900
parents 85f6238a38db
children babd8ac79a91
comparison
equal deleted inserted replaced
923:85f6238a38db 924:a48dc906796c
1314 → IsTotalOrderSet (UnionZF f mf ay supf ) 1314 → IsTotalOrderSet (UnionZF f mf ay supf )
1315 uztotal f mf ay sz {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 1315 uztotal f mf ay sz {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
1316 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 1316 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1317 uz01 = ? 1317 uz01 = ?
1318 1318
1319 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) 1319 usp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
1320 → ( supf : Ordinal → Ordinal ) 1320 → ( supf : Ordinal → Ordinal )
1321 → SUP A (UnionZF f mf ay supf ) 1321 → SUP A (UnionZF f mf ay supf )
1322 -- sp0 f mf {x} ay = supP (UnionZF f mf ay ) (λ lt → proj1 (ZChainP.zc lt)) (uztotal f mf ay) 1322 usp0 f mf {x} ay supf = supP (UnionZF f mf ay supf ) (λ lt → ? ) (uztotal f mf ay supf )
1323 sp0 f mf {x} ay supf = supP (UnionZF f mf ay supf ) (λ lt → ? ) (uztotal f mf ay supf ) 1323
1324 1324 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
1325 sp00 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
1326 → (zc : ZChain A f mf ay x ) 1325 → (zc : ZChain A f mf ay x )
1327 → SUP A (UnionCF A f mf ay (ZChain.supf zc) x) 1326 → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
1328 sp00 f mf {x} ay zc = supP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where 1327 sp0 f mf {x} ay zc = supP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where
1329 ztotal : IsTotalOrderSet (ZChain.chain zc) 1328 ztotal : IsTotalOrderSet (ZChain.chain zc)
1330 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 1329 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
1331 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 1330 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1332 uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 1331 uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb))
1333 1332
1334 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) 1333 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) )
1335 → f (& (SUP.sup (sp0 f mf as0 ? ))) ≡ & (SUP.sup (sp0 f mf as0 ? )) 1334 → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc ))
1336 fixpoint f mf = z14 where 1335 fixpoint f mf zc = z14 where
1337 chain = UnionZF f mf as0 ? 1336 chain = ZChain.chain zc
1338 supf : Ordinal → Ordinal 1337 supf = ZChain.supf zc
1339 supf = ? 1338 sp1 : SUP A chain
1340 sp1 : SUP A ? 1339 sp1 = sp0 f mf as0 zc
1341 sp1 = sp0 f mf as0 ?
1342 z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) 1340 z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b )
1343 → HasPrev A chain b f ∨ IsSup A chain {b} ab 1341 → HasPrev A chain b f ∨ IsSup A chain {b} ab
1344 → * a < * b → odef chain b 1342 → * a < * b → odef chain b
1345 z10 = ? -- ZChain1.is-max (SZ1 f mf as0 zc (& A) ) 1343 z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
1346 z22 : & (SUP.sup sp1) o< & A 1344 z22 : & (SUP.sup sp1) o< & A
1347 z22 = c<→o< ( SUP.as sp1 ) 1345 z22 = c<→o< ( SUP.as sp1 )
1348 z21 : supf (& (SUP.sup sp1)) o< supf (& A) 1346 z21 : supf (& (SUP.sup sp1)) o< supf (& A)
1349 z21 = ? 1347 z21 = ?
1350 -- z21 : supf (& (SUP.sup sp1)) o< & A 1348 -- z21 : supf (& (SUP.sup sp1)) o< & A
1351 -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) )) 1349 -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) ))
1352 z12 : odef chain (& (SUP.sup sp1)) 1350 z12 : odef chain (& (SUP.sup sp1))
1353 z12 with o≡? (& s) (& (SUP.sup sp1)) 1351 z12 with o≡? (& s) (& (SUP.sup sp1))
1354 ... | yes eq = subst (λ k → odef chain k) eq ? -- ( ZChain.chain∋init zc ) 1352 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
1355 ... | no ne = ? where -- ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1) 1353 ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1)
1356 -- (case2 ? ) z13 where 1354 (case2 z19 ) z13 where
1357 z13 : * (& s) < * (& (SUP.sup sp1)) 1355 z13 : * (& s) < * (& (SUP.sup sp1))
1358 z13 with SUP.x<sup sp1 ? 1356 z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc )
1359 ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) 1357 ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
1360 ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt 1358 ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
1361 z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1) 1359 z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1)
1362 z19 = record { x<sup = z20 } where 1360 z19 = record { x<sup = z20 } where
1363 z20 : {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1)) 1361 z20 : {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
1364 z20 {y} zy with SUP.x<sup sp1 ? 1362 z20 {y} zy with SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) zy)
1365 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p )) 1363 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
1366 ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) 1364 ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
1367 z14 : f (& (SUP.sup (sp0 f mf as0 ? ))) ≡ & (SUP.sup (sp0 f mf as0 ? )) 1365 ztotal : IsTotalOrderSet (ZChain.chain zc)
1368 z14 = ? -- with ? 1366 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
1369 -- ... | tri< a ¬b ¬c = ⊥-elim z16 where 1367 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1370 -- z16 : ⊥ 1368 uz01 = chain-total A f mf as0 supf ( (proj2 ca)) ( (proj2 cb))
1371 -- z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 )) 1369 z14 : f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc ))
1372 -- ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) )) 1370 z14 with ztotal (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12
1373 -- ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt )) 1371 ... | tri< a ¬b ¬c = ⊥-elim z16 where
1374 -- ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b ) 1372 z16 : ⊥
1375 -- ... | tri> ¬a ¬b c = ⊥-elim z17 where 1373 z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 ))
1376 -- z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) 1374 ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
1377 -- z15 = SUP.x<sup sp1 ? -- (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) 1375 ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
1378 -- z17 : ⊥ 1376 ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
1379 -- z17 with z15 1377 ... | tri> ¬a ¬b c = ⊥-elim z17 where
1380 -- ... | case1 eq = ¬b eq 1378 z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1)
1381 -- ... | case2 lt = ¬a lt 1379 z15 = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
1380 z17 : ⊥
1381 z17 with z15
1382 ... | case1 eq = ¬b eq
1383 ... | case2 lt = ¬a lt
1384
1382 1385
1383 -- ZChain contradicts ¬ Maximal 1386 -- ZChain contradicts ¬ Maximal
1384 -- 1387 --
1385 -- ZChain forces fix point on any ≤-monotonic function (fixpoint) 1388 -- ZChain forces fix point on any ≤-monotonic function (fixpoint)
1386 -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain 1389 -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
1387 -- 1390 --
1388 z04 : (nmx : ¬ Maximal A ) → ⊥ 1391
1389 z04 nmx = ? where -- <-irr0 ? ? 1392 z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥
1390 --(case1 ?) -- x ≡ f x ̄ 1393 z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 ))))
1391 -- ? where -- x < f x 1394 (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
1392 sp1 : SUP A ? 1395 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) -- x ≡ f x ̄
1393 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 ? 1396 (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x
1394 z041 : ? 1397 sp1 : SUP A (ZChain.chain zc)
1395 z041 = cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) ) 1398 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
1396 c = & (SUP.sup sp1) 1399 c = & (SUP.sup sp1)
1397 z042 : ?
1398 z042 = is-cf nmx (SUP.as ? )
1399 z043 = proj1 (cf-is-<-monotonic nmx ? (SUP.as ? ))
1400 zorn00 : Maximal A 1400 zorn00 : Maximal A
1401 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM 1401 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM
1402 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where 1402 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where
1403 -- yes we have the maximal 1403 -- yes we have the maximal
1404 zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) ) 1404 zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) )
1405 zorn03 = ODC.x∋minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) -- Axiom of choice 1405 zorn03 = ODC.x∋minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) -- Axiom of choice
1406 zorn01 : A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) 1406 zorn01 : A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))
1407 zorn01 = proj1 zorn03 1407 zorn01 = proj1 zorn03
1408 zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x) 1408 zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
1409 zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x ) 1409 zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
1410 ... | yes ¬Maximal = ⊥-elim ( z04 nmx ) where 1410 ... | yes ¬Maximal = ⊥-elim ( z04 nmx ? ) where
1411 -- if we have no maximal, make ZChain, which contradict SUP condition 1411 -- if we have no maximal, make ZChain, which contradict SUP condition
1412 nmx : ¬ Maximal A 1412 nmx : ¬ Maximal A
1413 nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where 1413 nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where
1414 zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) → odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 1414 zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) → odef A y → ¬ (* (& (Maximal.maximal mx)) < * y))
1415 zc5 = ⟪ Maximal.as mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫ 1415 zc5 = ⟪ Maximal.as mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫