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

comparison src/zorn.agda @ 935:ed711d7be191

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mem exhaust fix on fixpoint
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Oct 2022 16:06:18 +0900
parents ebcad8e5ae55
children f160556a7c9a
comparison
equal deleted inserted replaced
934:ebcad8e5ae55 935:ed711d7be191
1347 → (zc : ZChain A f mf ay x ) 1347 → (zc : ZChain A f mf ay x )
1348 → SUP A (UnionCF A f mf ay (ZChain.supf zc) x) 1348 → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
1349 sp0 f mf ay zc = M→S (ZChain.supf zc) (msp0 f mf ay zc ) 1349 sp0 f mf ay zc = M→S (ZChain.supf zc) (msp0 f mf ay zc )
1350 1350
1351 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) 1351 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) )
1352 → ZChain.supf zc (& (SUP.sup (sp0 f mf as0 zc))) o< ZChain.supf zc (& A) 1352 → (sp1 : SUP A (ZChain.chain zc)) -- & (SUP.sup (sp0 f mf as0 zc ))
1353 → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) 1353 → (ssp<as : ZChain.supf zc (& (SUP.sup sp1)) o< ZChain.supf zc (& A))
1354 fixpoint f mf zc ss<sa = z14 where 1354 → f (& (SUP.sup sp1)) ≡ & (SUP.sup sp1)
1355 fixpoint f mf zc sp1 ssp<as = z14 where
1355 chain = ZChain.chain zc 1356 chain = ZChain.chain zc
1356 supf = ZChain.supf zc 1357 supf = ZChain.supf zc
1357 sp1 : SUP A chain 1358 sp : Ordinal
1358 sp1 = sp0 f mf as0 zc 1359 sp = & (SUP.sup sp1)
1360 asp : odef A sp
1361 asp = SUP.as sp1
1359 z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) 1362 z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b )
1360 → HasPrev A chain b f ∨ IsSup A chain {b} ab 1363 → HasPrev A chain b f ∨ IsSup A chain {b} ab
1361 → * a < * b → odef chain b 1364 → * a < * b → odef chain b
1362 z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) 1365 z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
1363 z22 : & (SUP.sup sp1) o< & A 1366 z22 : sp o< & A
1364 z22 = c<→o< ( SUP.as sp1 ) 1367 z22 = z09 asp
1365 z21 : supf (& (SUP.sup sp1)) o< supf (& A) 1368 x<sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 )
1366 z21 = ss<sa 1369 x<sup bz with SUP.x<sup sp1 bz
1367 -- z21 : supf (& (SUP.sup sp1)) o< & A 1370 ... | case1 eq = case1 ?
1368 -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) )) 1371 ... | case2 lt = case2 ?
1369 z12 : odef chain (& (SUP.sup sp1)) 1372 z12 : odef chain sp
1370 z12 with o≡? (& s) (& (SUP.sup sp1)) 1373 z12 with o≡? (& s) sp
1371 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) 1374 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
1372 ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1) 1375 ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp
1373 (case2 z19 ) z13 where 1376 (case2 z19 ) z13 where
1374 z13 : * (& s) < * (& (SUP.sup sp1)) 1377 z13 : * (& s) < * sp
1375 z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc ) 1378 z13 with x<sup ( ZChain.chain∋init zc )
1376 ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) 1379 ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
1377 ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt 1380 ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
1378 z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1) 1381 z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1)
1379 z19 = record { x<sup = z20 } where 1382 z19 = record { x<sup = z20 } where
1380 z20 : {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1)) 1383 z20 : {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
1381 z20 {y} zy with SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) zy) 1384 z20 {y} zy with x<sup (subst (λ k → odef chain k ) (sym &iso) zy)
1382 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p )) 1385 ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
1383 ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) 1386 ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
1384 ztotal : IsTotalOrderSet (ZChain.chain zc) 1387 ztotal : IsTotalOrderSet (ZChain.chain zc)
1385 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 1388 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
1386 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 1389 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1387 uz01 = chain-total A f mf as0 supf ( (proj2 ca)) ( (proj2 cb)) 1390 uz01 = chain-total A f mf as0 supf ( (proj2 ca)) ( (proj2 cb))
1388 z14 : f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) 1391 z14 : f sp ≡ sp
1389 z14 with ztotal (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 1392 z14 with ztotal (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12
1390 ... | tri< a ¬b ¬c = ⊥-elim z16 where 1393 ... | tri< a ¬b ¬c = ⊥-elim z16 where
1391 z16 : ⊥ 1394 z16 : ⊥
1392 z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 )) 1395 z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 ))
1393 ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) )) 1396 ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
1394 ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt )) 1397 ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
1395 ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b ) 1398 ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
1396 ... | tri> ¬a ¬b c = ⊥-elim z17 where 1399 ... | tri> ¬a ¬b c = ⊥-elim z17 where
1397 z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) 1400 z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) < * sp )
1398 z15 = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) 1401 z15 = ? -- x<sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
1399 z17 : ⊥ 1402 z17 : ⊥
1400 z17 with z15 1403 z17 with z15
1401 ... | case1 eq = ¬b eq 1404 ... | case1 eq = ¬b eq
1402 ... | case2 lt = ¬a lt 1405 ... | case2 lt = ¬a ?
1403 1406
1404 1407
1405 -- ZChain contradicts ¬ Maximal 1408 -- ZChain contradicts ¬ Maximal
1406 -- 1409 --
1407 -- ZChain forces fix point on any ≤-monotonic function (fixpoint) 1410 -- ZChain forces fix point on any ≤-monotonic function (fixpoint)
1409 -- 1412 --
1410 1413
1411 z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥ 1414 z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥
1412 z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 )))) 1415 z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 ))))
1413 (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) ) 1416 (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
1414 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ss<sa ))) -- x ≡ f x ̄ 1417 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc
1418 (sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc ) ss<sa ))) -- x ≡ f x ̄
1415 (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x 1419 (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x
1416 supf = ZChain.supf zc 1420 supf = ZChain.supf zc
1417 msp1 : MinSUP A (ZChain.chain zc) 1421 msp1 : MinSUP A (ZChain.chain zc)
1418 msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 1422 msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
1419 sp1 : SUP A (ZChain.chain zc) 1423 sp1 : SUP A (ZChain.chain zc)