Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 585:9922bfe92278
ZChain∧Chain
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Jun 2022 18:37:57 +0900 |
| parents | b684030c8a28 |
| children | 40090ce9232c |
| files | src/zorn.agda |
| diffstat | 1 files changed, 40 insertions(+), 40 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Jun 07 18:01:28 2022 +0900 +++ b/src/zorn.agda Tue Jun 07 18:37:57 2022 +0900 @@ -89,9 +89,6 @@ ≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set (Level.suc n) ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧ odef A (f x ) --- immieate-f : (A : HOD) → ( f : Ordinal → Ordinal ) → Set n --- immieate-f A f = { x y : Ordinal } → odef A x → odef A y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) - data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where init : odef A s → FClosure A f s s fsuc : (x : Ordinal) ( p : FClosure A f s x ) → FClosure A f s (f x) @@ -235,11 +232,10 @@ field x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) (Chain : HOD) +record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where - chain : HOD - chain = Chain field + chain : HOD chain⊆A : chain ⊆' A chain∋x : odef chain x initial : {y : Ordinal } → odef chain y → * x ≤ * y @@ -251,6 +247,14 @@ → * a < * b → odef chain b fc∨sup : {a : Ordinal } → ( ca : odef chain a ) → HasPrev A chain ( chain⊆A ca) f ∨ IsSup A chain ( chain⊆A ca) +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 + chain-mono : {a b : Ordinal} → a o< b → chainf a ⊆' chainf b + chain=zchain : {b : Ordinal} → chainf z ≡ ZChain.chain zchain + record Maximal ( A : HOD ) : Set (Level.suc n) where field maximal : HOD @@ -273,10 +277,6 @@ Zorn-lemma {A} 0<A supP = zorn00 where supO : (C : HOD ) → C ⊆' A → IsTotalOrderSet C → Ordinal supO C C⊆A TC = & ( SUP.sup ( supP C C⊆A TC )) - postulate - --- irrelevance of ⊆' and compare - sup== : {C C1 : HOD } → C ≡ C1 → {c : C ⊆' A } {c1 : C1 ⊆' A } → {t : IsTotalOrderSet C } {t1 : IsTotalOrderSet C1 } - → SUP.sup ( supP C c t ) ≡ SUP.sup ( supP C1 c1 t1 ) <-irr0 : {a b : HOD} → A ∋ a → A ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥ <-irr0 {a} {b} A∋a A∋b = <-irr z07 : {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A @@ -320,20 +320,12 @@ 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 ) ⟫ - cind : ( 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 (Chain z) z ) → { y : Ordinal } → (ya : odef A y) → HOD - cind = ? - - Chain : (x : Ordinal) → HOD - Chain = {!!} - - ind f mf x prev {y} ay with Oprev-p x - zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A (& s) f (Chain (& A)) (& A) ) → SUP A (ZChain.chain zc) + 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) (Chain (& A)) (& A) ) + 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 (Chain (& A))(& A) ) → SUP A (ZChain.chain 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) 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) @@ -341,7 +333,7 @@ --- --- the maximum chain has fix point of any ≤-monotonic function --- - fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (Chain (& A))(& A) ) + 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 chain = ZChain.chain zc @@ -389,7 +381,7 @@ -- 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) (Chain (& A)) (& A)) → ⊥ + 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)))) (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) ) (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) -- x ≡ f x ̄ @@ -397,26 +389,31 @@ sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc c = & (SUP.sup sp1) + ind1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) + → ((y : Ordinal) → y o< x → {y = y₁ : Ordinal} → odef A y₁ → ZChain∧Chain A y₁ f y) → + {y : Ordinal} → odef A y → ZChain∧Chain A y f x + ind1 = {!!} + -- -- 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 (Chain z) z ) → { y : Ordinal } → (ya : odef A y) → ZChain A y f (Chain x) x + ((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 mf x prev {y} ay with Oprev-p x ... | yes op = zc4 where -- -- we have previous ordinal to use induction -- px = Oprev.oprev op - zc0 : ZChain A y f (Chain (Oprev.oprev op)) (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 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 (Chain x) x + zc4 : ZChain A y f x zc4 with ODC.∋-p O A (* x) ... | no noax = -- ¬ A ∋ p, just skip - record { chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 + 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 ; 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) → @@ -434,13 +431,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 (Chain x) x - zc9 = record { chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 -- no extention + 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⊆A = {!!} ; f-total = {!!} ; f-next = {!!} - ; initial = {!!} ; f-immediate = {!!} ; chain∋x = case1 (ZChain.chain∋x zc0) ; is-max = {!!} ; fc∨sup = {!!}} where + 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 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) @@ -540,7 +537,7 @@ ... | case1 y=b = subst (λ k → odef chain k ) y=b ( ZChain.chain∋x zc0 ) ... | case2 y<b = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b ... | case2 ¬x=sup = -- x is not f y' nor sup of former ZChain from y - record { chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 + record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = z18 ; fc∨sup = {!!} } where -- no extention z18 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) → @@ -553,13 +550,13 @@ ... | 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 with trio< x y - ... | tri< a ¬b ¬c = record { chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} + ... | tri< a ¬b ¬c = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b y<x = {!!} where - UnionZ : ZChain A y f (Chain x) x - UnionZ = record { chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} - ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } where --- limit ordinal case + 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 field u : Ordinal @@ -567,7 +564,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 (Chain (UZFChain.u u)) (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 @@ -598,11 +595,14 @@ 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 (Chain (& A)) (& A) - zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A y f (Chain z) z } (ind f mf) (& A) - zorn04 : ZChain A (& s) (cf nmx) (Chain (& A)) (& A) + 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 ) + zorn05 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain∧Chain A (& s) f (& A) + zorn05 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain∧Chain A y f z } {!!} (& A) + -- usage (see filter.agda ) -- -- _⊆'_ : ( A B : HOD ) → Set n