Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 584:b684030c8a28
try mutual transfinite
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Jun 2022 18:01:28 +0900 |
| parents | f545b97ce7a8 |
| children | 9922bfe92278 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 33 insertions(+), 49 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Jun 07 12:59:08 2022 +0900 +++ b/src/zorn.agda Tue Jun 07 18:01:28 2022 +0900 @@ -235,10 +235,11 @@ field x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) +record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) (Chain : HOD) ( 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 @@ -250,31 +251,6 @@ → * 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) -Uz-mono : ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) - → ( a b : Ordinal ) → a o< b → (za : ZChain A x f a) (zb : ZChain A x f b) - → ZChain.chain za ⊆' ZChain.chain zb -Uz-mono A x f a b = TransFinite {λ a → a o< b → (za : ZChain A x f a) (zb : ZChain A x f b) - → ZChain.chain za ⊆' ZChain.chain zb } ind a where - open ZChain - ind : (a : Ordinal) - → ((y : Ordinal) → y o< a → y o< b → (za : ZChain A x f y) (zb : ZChain A x f b) → chain za ⊆' chain zb) - → a o< b → (za : ZChain A x f a) (zb : ZChain A x f b) → chain za ⊆' chain zb - ind a prev a<b za zb {i} zai with f-total za (subst (λ k → odef (chain za) k) (sym &iso) zai) - (subst (λ k → odef (chain za) k) (sym &iso) (chain∋x za) ) - ... | tri< i<x ¬b ¬c with initial za zai - ... | case1 i=x = ⊥-elim ( ¬b (sym i=x)) - ... | case2 x<i = ⊥-elim ( ¬c x<i) - ind a prev a<b za zb {i} zai | tri≈ ¬a b ¬c = subst (λ k → odef (chain zb) k ) (sym (*≡*→≡ b))(chain∋x zb) - ind a prev a<b za zb {i} zai | tri> ¬a ¬b x<i = um i zai where - um : (i : Ordinal ) → odef (chain za) i → odef (chain zb) i - um zai i with fc∨sup za zai - ... | case1 fc = {!!} - ... | case2 sup = {!!} - um01 : i o< osuc b - um01 = {!!} - um02 : {!!} - um02 = is-max zb (chain∋x zb) {!!} (chain⊆A za zai) {!!} x<i - record Maximal ( A : HOD ) : Set (Level.suc n) where field maximal : HOD @@ -344,12 +320,20 @@ 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) + 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 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∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A (& s) (cf nmx) (Chain (& A)) (& 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 : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (Chain (& A))(& 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) @@ -357,7 +341,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 (& A) ) + fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (Chain (& A))(& A) ) → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc )) fixpoint f mf zc = z14 where chain = ZChain.chain zc @@ -405,7 +389,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) (& A)) → ⊥ + z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx) (Chain (& A)) (& 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 ̄ @@ -417,22 +401,22 @@ -- 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 + ((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 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 (Oprev.oprev op) + zc0 : ZChain A y f (Chain (Oprev.oprev op)) (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 (Chain x) 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) → @@ -450,13 +434,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 = 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 + 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 ; 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 = {!!} ; f-total = {!!} ; f-next = {!!} + ; initial = {!!} ; f-immediate = {!!} ; 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) @@ -556,7 +540,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 = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 + record { 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) → @@ -569,13 +553,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 = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} + ... | tri< a ¬b ¬c = record { 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 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 + 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 record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x field u : Ordinal @@ -583,7 +567,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 (Chain (UZFChain.u u)) (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 @@ -614,9 +598,9 @@ 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) + 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) zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) -- usage (see filter.agda )