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

comparison src/zorn.agda @ 651:18357e4bddba

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ZChain1 is not strictly positive
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Jun 2022 18:17:09 +0900
parents 3f0963e1c79f
children 8a4c3d68c6c2
comparison
equal deleted inserted replaced
650:3f0963e1c79f 651:18357e4bddba
416 no-extenion is-max = record { chain⊆A = ZChain.chain⊆A zc 416 no-extenion is-max = record { chain⊆A = ZChain.chain⊆A zc
417 ; initial = ZChain.initial zc 417 ; initial = ZChain.initial zc
418 ; f-next = ZChain.f-next zc ; chain = ZChain.chain zc 418 ; f-next = ZChain.f-next zc ; chain = ZChain.chain zc
419 ; chain∋x = ZChain.chain∋x zc 419 ; chain∋x = ZChain.chain∋x zc
420 ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) → 420 ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
421 HasPrev A k ab f ∨ IsSup A k ab → * a < * b → odef k b ) ? is-max } 421 HasPrev A k ab f ∨ IsSup A k ab → * a < * b → odef k b ) {!!} is-max }
422 422
423 zc4 : ZChain A y f x 423 zc4 : ZChain A y f x
424 zc4 with ODC.∋-p O A (* x) 424 zc4 with ODC.∋-p O A (* x)
425 ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip 425 ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip
426 zc1 : {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → 426 zc1 : {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
576 px<x : px o< x 576 px<x : px o< x
577 px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 577 px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
578 no-extrention1 : ( {a b : Ordinal} → odef (chain zc0) a → b o< osuc x → (ab : odef A b) → 578 no-extrention1 : ( {a b : Ordinal} → odef (chain zc0) a → b o< osuc x → (ab : odef A b) →
579 HasPrev A (chain zc0) ab f ∨ IsSup A (chain zc0) ab → 579 HasPrev A (chain zc0) ab f ∨ IsSup A (chain zc0) ab →
580 * a < * b → odef (ZChain.chain zc0) b ) → ZChain1 y f x 580 * a < * b → odef (ZChain.chain zc0) b ) → ZChain1 y f x
581 no-extrention1 imx = record { zc = sz00 ; chain-mono = ? ; f-total = ? } where 581 no-extrention1 imx = record { zc = sz00 ; chain-mono = {!!} ; f-total = {!!} } where
582 sz00 : {z : Ordinal} → z o≤ x → ZChain A y f z 582 sz00 : {z : Ordinal} → z o≤ x → ZChain A y f z
583 sz00 {z} z≤x = ? 583 sz00 {z} z≤x = {!!}
584 sz02 : ZChain1 y f x 584 sz02 : ZChain1 y f x
585 sz02 with ODC.∋-p O A (* x) 585 sz02 with ODC.∋-p O A (* x)
586 ... | no noax = no-extrention1 ? 586 ... | no noax = no-extrention1 {!!}
587 ... | yes ax with ODC.p∨¬p O ( HasPrev A (chain zc0) ax f ) 587 ... | yes ax with ODC.p∨¬p O ( HasPrev A (chain zc0) ax f )
588 ... | case1 pr = record { zc = ? ; chain-mono = ? ; f-total = ? } where 588 ... | case1 pr = record { zc = {!!} ; chain-mono = {!!} ; f-total = {!!} } where
589 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (chain zc0) ax ) 589 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (chain zc0) ax )
590 ... | case1 is-sup = ? where -- x is a sup of zc 1 590 ... | case1 is-sup = {!!} where -- x is a sup of zc 1
591 sup0 : SUP A (chain zc0) 591 sup0 : SUP A (chain zc0)
592 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where 592 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
593 x21 : {y : HOD} → (chain zc0) ∋ y → (y ≡ * x) ∨ (y < * x) 593 x21 : {y : HOD} → (chain zc0) ∋ y → (y ≡ * x) ∨ (y < * x)
594 x21 {y} zy with IsSup.x<sup is-sup zy 594 x21 {y} zy with IsSup.x<sup is-sup zy
595 ... | case1 y=x = case1 ( subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x) ) 595 ... | case1 y=x = case1 ( subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x) )
598 sp = SUP.sup sup0 598 sp = SUP.sup sup0
599 x=sup : x ≡ & sp 599 x=sup : x ≡ & sp
600 x=sup = sym &iso 600 x=sup = sym &iso
601 chain0 = chain zc0 601 chain0 = chain zc0
602 sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A 602 sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A
603 sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< ? ) 603 sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< {!!} )
604 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) ) 604 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
605 schain : HOD 605 schain : HOD
606 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy } 606 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy }
607 ... | case2 ¬x=sup = ? 607 ... | case2 ¬x=sup = {!!}
608 ... | no ¬ox = record { zc = zcu ; chain-mono = sz03 ; f-total = ? } where 608 ... | no ¬ox = record { zc = zcu ; chain-mono = sz03 ; f-total = {!!} } where
609 pzc : (z : Ordinal) → z o< x → ZChain A y f z 609 pzc : (z : Ordinal) → z o< x → ZChain A y f z
610 pzc z z<x = ind f mf ay z (λ w w<px → zc (prev z z<x) (o<→≤ w<px) ) 610 pzc z z<x = ind f mf ay z (λ w w<px → zc (prev z z<x) (o<→≤ w<px) )
611 Uz⊆A : {z : Ordinal} → UZFChain A f x y pzc z ∨ FClosure A f y z → odef A z 611 Uz⊆A : {z : Ordinal} → UZFChain A f x y pzc z ∨ FClosure A f y z → odef A z
612 Uz⊆A {z} (case1 u) = ZChain.chain⊆A ( pzc (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u) 612 Uz⊆A {z} (case1 u) = ZChain.chain⊆A ( pzc (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u)
613 Uz⊆A (case2 lt) = A∋fc _ f mf lt 613 Uz⊆A (case2 lt) = A∋fc _ f mf lt
616 Uz : HOD 616 Uz : HOD
617 Uz = record { od = record { def = λ z → UZFChain A f x y pzc z ∨ FClosure A f y z } ; odmax = & A 617 Uz = record { od = record { def = λ z → UZFChain A f x y pzc z ∨ FClosure A f y z } ; odmax = & A
618 ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) } 618 ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
619 zcu1 : { z : Ordinal } → z o≤ x → ZChain1 y f z 619 zcu1 : { z : Ordinal } → z o≤ x → ZChain1 y f z
620 zcu1 {z} z≤x with osuc-≡< z≤x 620 zcu1 {z} z≤x with osuc-≡< z≤x
621 ... | case1 z=x = record { zc = ? ; chain-mono = ? ; f-total = ? } 621 ... | case1 z=x = record { zc = {!!} ; chain-mono = {!!} ; f-total = {!!} }
622 ... | case2 z<x = prev z z<x 622 ... | case2 z<x = prev z z<x
623 zcu : { z : Ordinal } → z o≤ x → ZChain A y f z 623 zcu : { z : Ordinal } → z o≤ x → ZChain A y f z
624 zcu {z} z≤x = ind f mf ay z (λ w w<px → zc (zcu1 z≤x ) (o<→≤ w<px) ) 624 zcu {z} z≤x with osuc-≡< z≤x
625 ... | case1 z=x = record { chain = Uz }
626 ... | case2 z<x = ind f mf ay z (λ w w<px → zc (prev z z<x ) (o<→≤ w<px) )
625 sz03 : {a b : Ordinal} → (a≤b : a o≤ b) → (b≤x : b o≤ x ) → chain (zcu {a} (OrdTrans a≤b b≤x)) ⊆' chain (zcu b≤x ) 627 sz03 : {a b : Ordinal} → (a≤b : a o≤ b) → (b≤x : b o≤ x ) → chain (zcu {a} (OrdTrans a≤b b≤x)) ⊆' chain (zcu b≤x )
626 sz03 = ? 628 sz03 {a} {b} a≤b b≤x {i} ai with osuc-≡< (OrdTrans a≤b b≤x) | osuc-≡< b≤x
629 ... | case1 a=x | case1 b=x = {!!}
630 ... | case1 a=x | case2 b<x = ⊥-elim ( osuc-< (subst (λ k → k o< osuc b ) a=x a≤b) b<x )
631 ... | case2 a<x | case1 b=x = case1 record { u = a ; u<x = a<x ; chain∋z = subst (λ k → odef k i) {!!} ai } where
632 sz04 : {!!}
633 sz04 = {!!}
634 ... | case2 a<x | case2 b<x = {!!}
627 635
628 zorn00 : Maximal A 636 zorn00 : Maximal A
629 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM 637 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM
630 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x = zorn02 } where 638 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x = zorn02 } where
631 -- yes we have the maximal 639 -- yes we have the maximal