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

comparison src/zorn.agda @ 766:e1c6c32efe01

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, 25 Jul 2022 21:21:29 +0900
parents 7fff07748fde
children 6c87cb98abf2
comparison
equal deleted inserted replaced
765:7fff07748fde 766:e1c6c32efe01
321 {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a ) 321 {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
322 chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where 322 chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
323 ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a) 323 ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
324 ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb 324 ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb
325 ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub supb fcb) with ChainP.fcy<sup supb fca 325 ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub supb fcb) with ChainP.fcy<sup supb fca
326 ... | case1 eq = ? 326 ... | case1 eq with s≤fc (supf ub) f mf fcb
327 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
328 ct00 : * a ≡ * b
329 ct00 = trans (cong (*) eq) eq1
327 ... | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where 330 ... | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where
331 ct01 : * a < * b
332 ct01 = subst (λ k → * k < * b ) (sym eq) lt
333 ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub supb fcb) | case2 lt = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where
328 ct00 : * a < * (supf ub) 334 ct00 : * a < * (supf ub)
329 ct00 = lt 335 ct00 = lt
330 ct01 : * a < * b 336 ct01 : * a < * b
331 ct01 with s≤fc (supf ub) f mf fcb 337 ct01 with s≤fc (supf ub) f mf fcb
332 ... | case1 eq = subst (λ k → * a < k ) eq ct00 338 ... | case1 eq = subst (λ k → * a < k ) eq ct00
333 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt 339 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt
334 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb 340 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
335 ... | case1 eq = ? 341 ... | case1 eq with s≤fc (supf ua) f mf fca
342 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
343 ct00 : * a ≡ * b
344 ct00 = sym (trans (cong (*) eq) eq1 )
336 ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where 345 ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where
346 ct01 : * b < * a
347 ct01 = subst (λ k → * k < * a ) (sym eq) lt
348 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where
337 ct00 : * b < * (supf ua) 349 ct00 : * b < * (supf ua)
338 ct00 = lt 350 ct00 = lt
339 ct01 : * b < * a 351 ct01 : * b < * a
340 ct01 with s≤fc (supf ua) f mf fca 352 ct01 with s≤fc (supf ua) f mf fca
341 ... | case1 eq = subst (λ k → * b < k ) eq ct00 353 ... | case1 eq = subst (λ k → * b < k ) eq ct00
342 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt 354 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt
343 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) with trio< ua ub 355 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) with trio< ua ub
344 ... | tri< a₁ ¬b ¬c with ChainP.order supb a₁ (ChainP.csupz supa) 356 ... | tri< a₁ ¬b ¬c with ChainP.order supb a₁ (ChainP.csupz supa)
345 ... | case1 eq = ? 357 ... | case1 eq with s≤fc (supf ub) f mf fcb
346 ... | case2 lt = tri< ct02 (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt) where 358 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
359 ct00 : * a ≡ * b
360 ct00 = trans (cong (*) eq) eq1
361 ... | case2 lt = tri< ct02 (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt) where
362 ct02 : * a < * b
363 ct02 = subst (λ k → * k < * b ) (sym eq) lt
364 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri< a₁ ¬b ¬c | case2 lt = tri< ct02 (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt) where
347 ct03 : * a < * (supf ub) 365 ct03 : * a < * (supf ub)
348 ct03 = lt 366 ct03 = lt
349 ct02 : * a < * b 367 ct02 : * a < * b
350 ct02 with s≤fc (supf ub) f mf fcb 368 ct02 with s≤fc (supf ub) f mf fcb
351 ... | case1 eq = subst (λ k → * a < k ) eq ct03 369 ... | case1 eq = subst (λ k → * a < k ) eq ct03
352 ... | case2 lt = IsStrictPartialOrder.trans POO ct03 lt 370 ... | case2 lt = IsStrictPartialOrder.trans POO ct03 lt
353 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri≈ ¬a refl ¬c = fcn-cmp (supf ua) f mf fca fcb 371 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri≈ ¬a refl ¬c = fcn-cmp (supf ua) f mf fca fcb
354 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri> ¬a ¬b c with ChainP.order supa c (ChainP.csupz supb) 372 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri> ¬a ¬b c with ChainP.order supa c (ChainP.csupz supb)
355 ... | case1 eq = ? 373 ... | case1 eq with s≤fc (supf ua) f mf fca
356 ... | case2 lt = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04 where 374 ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
375 ct00 : * a ≡ * b
376 ct00 = sym (trans (cong (*) eq) eq1)
377 ... | case2 lt = tri> (λ lt → <-irr (case2 ct02) lt) (λ eq → <-irr (case1 eq) ct02) ct02 where
378 ct02 : * b < * a
379 ct02 = subst (λ k → * k < * a ) (sym eq) lt
380 ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri> ¬a ¬b c | case2 lt = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04 where
357 ct05 : * b < * (supf ua) 381 ct05 : * b < * (supf ua)
358 ct05 = lt 382 ct05 = lt
359 ct04 : * b < * a 383 ct04 : * b < * a
360 ct04 with s≤fc (supf ua) f mf fca 384 ct04 with s≤fc (supf ua) f mf fca
361 ... | case1 eq = subst (λ k → * b < k ) eq ct05 385 ... | case1 eq = subst (λ k → * b < k ) eq ct05
478 m03 with proj2 ua 502 m03 with proj2 ua
479 ... | ch-init fc = ⟪ proj1 ua , ch-init fc ⟫ 503 ... | ch-init fc = ⟪ proj1 ua , ch-init fc ⟫
480 ... | ch-is-sup u is-sup-a fc with trio< u px 504 ... | ch-is-sup u is-sup-a fc with trio< u px
481 ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u is-sup-a fc ⟫ -- u o< osuc x 505 ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u is-sup-a fc ⟫ -- u o< osuc x
482 ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u is-sup-a fc ⟫ 506 ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u is-sup-a fc ⟫
483 ... | tri> ¬a ¬b c = ⊥-elim (<-irr u≤a (ptrans a<b ? ) ) where 507 ... | tri> ¬a ¬b c = m08 where
484 -- a and b is a sup of chain, order forces minimulity of sup 508 -- a and b is a sup of chain, order forces minimulity of sup
485 su=u : ZChain.supf zc u ≡ u 509 su=u : ZChain.supf zc u ≡ u
486 su=u = ChainP.supfu=u is-sup-a 510 su=u = ChainP.supfu=u is-sup-a
487 u<A : u o< & A 511 u<A : u o< & A
488 u<A = z09 (subst (λ k → odef A k ) su=u (proj1 (ZChain.csupf zc ))) 512 u<A = z09 (subst (λ k → odef A k ) su=u (proj1 (ZChain.csupf zc )))
491 m07 : osuc b o≤ x 515 m07 : osuc b o≤ x
492 m07 = osucc (ordtrans b<px px<x ) 516 m07 = osucc (ordtrans b<px px<x )
493 fcb : FClosure A f (ZChain.supf zc b) b 517 fcb : FClosure A f (ZChain.supf zc b) b
494 fcb = subst (λ k → FClosure A f k b ) (sym (ZChain.sup=u zc ab (z09 ab) 518 fcb = subst (λ k → FClosure A f k b ) (sym (ZChain.sup=u zc ab (z09 ab)
495 (record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x m07 o≤-refl lt) } ) )) ( init ab ) 519 (record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x m07 o≤-refl lt) } ) )) ( init ab )
496 b<u : b <= u 520 m08 : odef (UnionCF A f mf ay (ZChain.supf zc) px) a
497 b<u = subst (λ k → b <= k ) su=u ( ZChain.order zc u<A (ordtrans b<px c) fcb ) 521 m08 with subst (λ k → b <= k ) su=u ( ZChain.order zc u<A (ordtrans b<px c) fcb )
522 ... | case2 b<u = ⊥-elim (<-irr u≤a (ptrans a<b b<u ) )
523 ... | case1 eq = ⊥-elim ( <-irr (s≤fc u f mf (subst (λ k → FClosure A f k a ) su=u fc )) (subst (λ k → * a < * k) eq a<b ))
498 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b 524 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
499 m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 525 m04 = ZChain1.is-max (prev px px<x) m03 b<px ab
500 (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤ (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) o≤-refl lt) } ) a<b 526 (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤ (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) o≤-refl lt) } ) a<b
501 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ where 527 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ where
502 b<A : b o< & A 528 b<A : b o< & A
612 ysup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) 638 ysup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y)
613 → SUP A (uchain f mf ay) 639 → SUP A (uchain f mf ay)
614 ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay) 640 ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay)
615 641
616 inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅ 642 inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
617 inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = ? ; fcy<sup = ? 643 inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = csupf ; fcy<sup = ?
618 ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where 644 ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
619 spi = & (SUP.sup (ysup f mf ay)) 645 spi = & (SUP.sup (ysup f mf ay))
620 isupf : Ordinal → Ordinal 646 isupf : Ordinal → Ordinal
621 isupf z = spi 647 isupf z = spi
622 sp = ysup f mf ay 648 sp = ysup f mf ay
625 y<sup : * y ≤ SUP.sup (ysup f mf ay) 651 y<sup : * y ≤ SUP.sup (ysup f mf ay)
626 y<sup = SUP.x<sup (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay)) 652 y<sup = SUP.x<sup (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay))
627 isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z 653 isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
628 isy {z} ⟪ az , uz ⟫ with uz 654 isy {z} ⟪ az , uz ⟫ with uz
629 ... | ch-init fc = s≤fc y f mf fc 655 ... | ch-init fc = s≤fc y f mf fc
630 ... | ch-is-sup u is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup) (s≤fc (& (SUP.sup (ysup f mf ay))) f mf ? ) 656 ... | ch-is-sup u is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup) (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc )
631 inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a) 657 inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
632 inext {a} ua with (proj2 ua) 658 inext {a} ua with (proj2 ua)
633 ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-init (fsuc _ fc ) ⟫ 659 ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-init (fsuc _ fc ) ⟫
634 ... | ch-is-sup u is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-is-sup u (ChainP-next A f mf ay isupf is-sup) (fsuc _ fc) ⟫ 660 ... | ch-is-sup u is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-is-sup u (ChainP-next A f mf ay isupf is-sup) (fsuc _ fc) ⟫
635 itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 661 itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅)