Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 608:6655f03984f9
mutual tranfinite in zorn
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 17 Jun 2022 11:28:06 +0900 |
| parents | 74c0ae81e482 |
| children | 5039d228838c |
| files | src/zorn.agda |
| diffstat | 1 files changed, 68 insertions(+), 58 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Jun 16 09:58:13 2022 +0900 +++ b/src/zorn.agda Fri Jun 17 11:28:06 2022 +0900 @@ -240,14 +240,10 @@ asup : odef A sup supf-isSup : IsSup A (* chain) asup -record ChainMono (A chain : HOD) (z : Ordinal) : Set n where - supf : (x : Ordinal) → SupF A - supfz=chain : SupF.chain z ≡ & chain - supf-mono : {x y : Ordinal} → x o< y → y o< osuc z → SupF.sup (supf x ) o< SupF.sup (supf y ) - -record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where +record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) (supf : Ordinal → SupF A) ( z : Ordinal ) : Set (Level.suc n) where + chain : HOD + chain = * (SupF.chain (supf z )) field - chain : HOD chain⊆A : chain ⊆' A chain∋x : odef chain x initial : {y : Ordinal } → odef chain y → * x ≤ * y @@ -257,7 +253,12 @@ is-max : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc z → (ab : odef A b) → HasPrev A chain ab f ∨ IsSup A chain ab → * a < * b → odef chain b - fc∨sup : ChainMono A chain z + supf-mono : {x y : Ordinal} → x o< y → y o< osuc z → SupF.sup (supf x ) o< SupF.sup (supf y ) + +record ZChain1 ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where + field + supf : Ordinal → SupF A + zc : ZChain A x f supf z record Maximal ( A : HOD ) : Set (Level.suc n) where field @@ -289,6 +290,8 @@ s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) as : A ∋ * ( & s ) as = subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) ) + as0 : odef A (& s ) + as0 = subst (λ k → odef A k ) &iso as s<A : & s o< & A s<A = c<→o< (subst (λ k → odef A (& k) ) *iso as ) HasMaximal : HOD @@ -328,24 +331,27 @@ cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ - zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A (& s) f (& A) ) → SUP A (ZChain.chain zc) - zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc ) - A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A (& s) (cf nmx) (& A) ) - → A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )) - A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) ) - sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (& A) ) → SUP A (ZChain.chain zc) - sp0 f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain.f-total zc) + zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc1 : ZChain1 A (& s) f (& A) ) → SUP A (ZChain.chain (ZChain1.zc zc1)) + zsup f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc ) where + zc = ZChain1.zc zc1 + A∋zsup : (nmx : ¬ Maximal A ) (zc1 : ZChain1 A (& s) (cf nmx) (& A) ) + → A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc1 ))) + A∋zsup nmx zc1 = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc1 ) ) + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc1 : ZChain1 A (& s) f (& A) ) → SUP A (ZChain.chain (ZChain1.zc zc1)) + sp0 f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain.f-total zc) where + zc = ZChain1.zc zc1 zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y) --- --- the maximum chain has fix point of any ≤-monotonic function --- - fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (& A) ) - → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc )) - fixpoint f mf zc = z14 where + fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc1 : ZChain1 A (& s) f (& A) ) + → f (& (SUP.sup (sp0 f mf zc1 ))) ≡ & (SUP.sup (sp0 f mf zc1 )) + fixpoint f mf zc1 = z14 where + zc = ZChain1.zc zc1 chain = ZChain.chain zc - sp1 = sp0 f mf zc + sp1 = sp0 f mf zc1 z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) → HasPrev A chain ab f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) → * a < * b → odef chain b @@ -368,7 +374,7 @@ ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p )) ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ? (SUP.x<sup sp1 ? ) } - z14 : f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc)) + z14 : f (& (SUP.sup (sp0 f mf zc1))) ≡ & (SUP.sup (sp0 f mf zc1)) z14 with ZChain.f-total zc (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 ... | tri< a ¬b ¬c = ⊥-elim z16 where z16 : ⊥ @@ -389,20 +395,21 @@ -- ZChain forces fix point on any ≤-monotonic function (fixpoint) -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain -- - z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx) (& A)) → ⊥ - z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal sp1)))) + z04 : (nmx : ¬ Maximal A ) → (zc : ZChain1 A (& s) (cf nmx) (& A)) → ⊥ + z04 nmx zc1 = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal sp1)))) (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) ) - (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) -- x ≡ f x ̄ + (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc1 ))) -- x ≡ f x ̄ (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where -- x < f x - sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc + zc = ZChain1.zc zc1 + sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc1 c = & (SUP.sup sp1) ys : {y : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → HOD ys {y} ay f mf = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = {!!} } - init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x - init-chain {y} {x} ay f mf x≤y = record { chain = ys ay f mf ; chain⊆A = λ fx → A∋fc y f mf fx - ; f-total = i-total ; f-next = λ {x} sx → fsuc x sx ; chain∋sup = {!!} - ; initial = {!!} ; f-immediate = {!!} ; chain∋x = init ay ; is-max = is-max ; fc∨sup = {!!} } where + init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain1 A y f x + init-chain {y} {x} ay f mf x≤y = record { zc = record { chain⊆A = λ fx → A∋fc y f mf {!!} + ; f-total = {!!} ; f-next = λ {x} sx → {!!} + ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} } ; supf = {!!} } where i-total : IsTotalOrderSet (ys ay f mf ) i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb) is-max : {a b : Ordinal} → odef (ys ay f mf) a → @@ -416,8 +423,9 @@ -- -- create all ZChains under o< x -- - ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → - ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A y f z ) → { y : Ordinal } → (ya : odef A y) → ZChain A y f x + + ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x → { y₁ : Ordinal} (ay : odef A y₁) + → ZChain1 A y₁ f y) → {y : Ordinal} (ay : odef A y) → ZChain1 A y f x ind f mf x prev {y} ay with Oprev-p x ... | yes op = zc4 where -- @@ -426,19 +434,21 @@ open ZChain px = Oprev.oprev op - zc0 : ZChain A y f (Oprev.oprev op) - zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay + supf : Ordinal → SupF A + supf = ZChain1.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay) + zc0 : ZChain A y f (ZChain1.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay)) (Oprev.oprev op) + zc0 = ZChain1.zc (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay) zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt px<x : px o< x px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc - zc4 : ZChain A y f x + zc4 : ZChain1 A y f x zc4 with ODC.∋-p O A (* x) ... | no noax = -- ¬ A ∋ p, just skip - record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 - ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; chain∋sup = {!!} - ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = {!!} } where -- no extention + record { zc = record { chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 + ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 + ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc11 } } where -- no extention zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) → HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0) ab → * a < * b → odef (ZChain.chain zc0) b @@ -446,7 +456,7 @@ ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) ) ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f ) -- we have to check adding x preserve is-max ZChain A y f mf supO x - ... | case1 pr = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next + ... | case1 pr = {!!} where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next chain0 = ZChain.chain zc0 zc17 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) → HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0) ab → @@ -454,14 +464,13 @@ zc17 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr)) - zc9 : ZChain A y f x - zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 -- no extention - ; chain∋sup = {!!} - ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!} } + zc9 : ZChain1 A y f x + zc9 = record { zc = record { chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} -- no extention + ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} } } ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax ) ... | case1 is-sup = -- x is a sup of zc0 - record { chain = schain ; chain⊆A = s⊆A ; f-total = scmp ; f-next = scnext ; chain∋sup = {!!} - ; initial = scinit ; f-immediate = simm ; chain∋x = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax ; fc∨sup = {!!} } where + record { zc = record { chain = schain ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; chain∋sup = {!!} + ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } } where sup0 : SUP A (ZChain.chain zc0) sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where x21 : {y : HOD} → ZChain.chain zc0 ∋ y → (y ≡ * x) ∨ (y < * x) @@ -573,19 +582,19 @@ ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } ) ... | case2 b=sup = ⊥-elim ( ¬x=sup record { x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy) } ) - ... | no ¬ox = UnionZ where - UnionZ : ZChain A y f x - UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A ; f-total = u-total ; f-next = u-next ; chain∋sup = {!!} - ; initial = u-initial ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } where --- limit ordinal case + ... | no ¬ox = {!!} where + UnionZ : ZChain A y f {!!} x + UnionZ = record { chain = Uz ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; chain∋sup = {!!} + ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } where --- limit ordinal case record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x field u : Ordinal u<x : u o< x - chain∋z : odef (ZChain.chain (prev u u<x {y} ay )) z + chain∋z : odef (ZChain.chain (ZChain1.zc (prev u u<x {y} ay ))) z Uz⊆A : {z : Ordinal} → UZFChain z → odef A z - Uz⊆A {z} u = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) {y} ay ) (UZFChain.chain∋z u) - uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (UZFChain.u u) - uzc {z} u = prev (UZFChain.u u) (UZFChain.u<x u) {y} ay + Uz⊆A {z} u = ZChain.chain⊆A (ZChain1.zc ( prev (UZFChain.u u) (UZFChain.u<x u) {y} ay )) (UZFChain.chain∋z u) + uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f {!!} (UZFChain.u u) + uzc {z} u = ZChain1.zc (prev (UZFChain.u u) (UZFChain.u<x u) {y} ay) Uz : HOD Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) } @@ -594,8 +603,8 @@ u-initial : {z : Ordinal} → odef Uz z → * y ≤ * z u-initial {z} u = ZChain.initial ( uzc u ) (UZFChain.chain∋z u) u-chain∋x : odef Uz y - u-chain∋x = record { u = y ; u<x = {!!} ; chain∋z = ZChain.chain∋x (prev y {!!} ay ) } - u-mono : ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za ⊆' ZChain.chain zb + u-chain∋x = record { u = y ; u<x = {!!} ; chain∋z = ZChain.chain∋x (ZChain1.zc (prev y {!!} ay )) } + u-mono : ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain A y f {!!} a) (zb : ZChain A y f {!!} b) → ZChain.chain za ⊆' ZChain.chain zb u-mono a b b<x a≤b za zb {i} zai = TransFinite0 {λ i → odef (chain za) i → odef (chain zb) i } uind i zai where open ZChain uind : (i : Ordinal) @@ -603,7 +612,7 @@ → odef (chain za) i → odef (chain zb) i uind i previ zai = um01 where um01 : odef (chain zb) i - um01 = ? + um01 = {!!} u-total : IsTotalOrderSet Uz u-total {x} {y} ux uy with trio< (UZFChain.u ux) (UZFChain.u uy) ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy) @@ -613,6 +622,9 @@ ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux) (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) + SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain1 A y f (& A) + SZ f mf = TransFinite {λ z → {y : Ordinal } → (ay : odef A y ) → ZChain1 A y f z } (ind f mf) (& A) + zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x = zorn02 } where @@ -629,10 +641,8 @@ nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) → odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) zc5 = ⟪ Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫ - zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A (& s) f (& A) - zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A y f z } (ind f mf) (& A) - zorn04 : ZChain A (& s) (cf nmx) (& A) - zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) + zorn04 : ZChain1 A (& s) (cf nmx) (& A) + zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) -- usage (see filter.agda ) --