Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 588:cc416fc0ef84
chainf is now global on ZChain
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Jun 2022 03:16:59 +0900 |
| parents | 6e0789af0d63 |
| children | b1e76b7991b0 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 37 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Jun 09 02:45:21 2022 +0900 +++ b/src/zorn.agda Thu Jun 09 03:16:59 2022 +0900 @@ -233,9 +233,10 @@ x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) - ( z : Ordinal ) : Set (Level.suc n) where + (chainf : Ordinal → HOD) ( z : Ordinal ) : Set (Level.suc n) where + chain : HOD + chain = chainf z field - chain : HOD chain⊆A : chain ⊆' A chain∋x : odef chain x initial : {y : Ordinal } → odef chain y → * x ≤ * y @@ -250,8 +251,8 @@ record ZChain∧Chain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where field - zchain : ZChain A x f z chainf : (b : Ordinal) → HOD + zchain : ZChain A x f chainf z chain-mono : {a b : Ordinal} → a o< b → b o< osuc z → chainf a ⊆' chainf b chain=zchain : chainf z ≡ ZChain.chain zchain @@ -320,24 +321,24 @@ 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) → (chainf : Ordinal → HOD) (zc : ZChain A (& s) f chainf (& A) ) → SUP A (ZChain.chain zc) + zsup f mf chainf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc ) + A∋zsup : (nmx : ¬ Maximal A ) (chainf : Ordinal → HOD) (zc : ZChain A (& s) (cf nmx) chainf (& A) ) + → A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) chainf zc ) )) + A∋zsup nmx chainf zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal (zsup (cf nmx) (cf-is-≤-monotonic nmx) chainf zc ) ) + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (chainf : Ordinal → HOD) (zc : ZChain A (& s) f chainf (& A) ) → SUP A (ZChain.chain zc) + sp0 f mf chainf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain.f-total zc) 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 ) (chainf : Ordinal → HOD) (zc : ZChain A (& s) f chainf (& A) ) + → f (& (SUP.sup (sp0 f mf chainf zc ))) ≡ & (SUP.sup (sp0 f mf chainf zc )) + fixpoint f mf chainf zc = z14 where chain = ZChain.chain zc - sp1 = sp0 f mf zc + sp1 = sp0 f mf chainf zc 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 @@ -360,7 +361,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 chainf zc))) ≡ & (SUP.sup (sp0 f mf chainf zc)) 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 : ⊥ @@ -381,12 +382,12 @@ -- 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 ) → (chainf : Ordinal → HOD) → (zc : ZChain A (& s) (cf nmx) chainf (& A)) → ⊥ + z04 nmx chainf zc = <-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 ) chainf zc ))) -- 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 + sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) chainf zc c = & (SUP.sup sp1) -- @@ -400,18 +401,20 @@ -- -- we have previous ordinal to use induction -- - prev : (z : Ordinal) → z o< x → {y : Ordinal} → odef A y → ZChain A y f z + prev : (z : Ordinal) → (z<x : z o< x ) → {y : Ordinal} → (ay : odef A y) → ZChain A y f (ZChain∧Chain.chainf (prevzc z z<x ay) ) z prev z z<x ay = ZChain∧Chain.zchain (prevzc z z<x ay) px = Oprev.oprev op - zc0 : ZChain A y f (Oprev.oprev op) + pchainf : Ordinal → HOD + pchainf = ZChain∧Chain.chainf (prevzc px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay) + zc0 : ZChain A y f pchainf (Oprev.oprev op) zc0 = 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 - zc4 : ZChain A y f x + zc4 : ZChain 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 + 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 ; fc∨sup = {!!} } where -- no extention zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) → @@ -429,13 +432,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 chain 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 : 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 ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!} } ... | 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 - ; initial = scinit ; f-immediate = simm ; chain∋x = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax ; fc∨sup = {!!} } where + record { chain⊆A = s⊆A ; f-total = scmp ; f-next = scnext + ; initial = scinit ; f-immediate = simm ; chain∋x = case1 (ZChain.chain∋x zc0) ; 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) @@ -549,15 +552,15 @@ x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy) } ) ... | no ¬ox with trio< x y ... | tri< a ¬b ¬c = record { zchain = - record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} + record { chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } ; chainf = {!!} ; chain-mono = {!!} ; chain=zchain = {!!} } ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b y<x = record { zchain = UnionZ ; chainf = {!!} ; chain-mono = {!!} ; chain=zchain = {!!} } where - prev : (z : Ordinal) → z o< x → {y : Ordinal} → odef A y → ZChain A y f z + prev : (z : Ordinal) → (z<x : z o< x )→ {y : Ordinal} → (ay : odef A y) → ZChain A y f (ZChain∧Chain.chainf (prevzc z z<x ay)) z prev z z<x ay = ZChain∧Chain.zchain (prevzc z z<x ay) - UnionZ : ZChain A y f x + UnionZ : ZChain A y f {!!} x UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A ; f-total = u-total ; f-next = u-next ; initial = u-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 @@ -567,7 +570,7 @@ chain∋z : odef (ZChain.chain (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 : 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 : HOD Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A @@ -613,7 +616,7 @@ zorn01 = proj1 zorn03 zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x) zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x ) - ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04) where + ... | yes ¬Maximal = ⊥-elim ( z04 nmx chainf zorn04) where -- if we have no maximal, make ZChain, which contradict SUP condition nmx : ¬ Maximal A nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where @@ -621,8 +624,9 @@ 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∧Chain A (& s) f (& A) zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain∧Chain A y f z } (ind f mf) (& A) - - zorn04 : ZChain A (& s) (cf nmx) (& A) + chainf : Ordinal → HOD + chainf = ZChain∧Chain.chainf (zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )) + zorn04 : ZChain A (& s) (cf nmx) chainf (& A) zorn04 = ZChain∧Chain.zchain (zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )) -- usage (see filter.agda )