Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/zorn.agda @ 582:48e9d2e61bbe
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Jun 2022 02:18:25 +0900 |
| parents | 95ec4d121e12 |
| children | f545b97ce7a8 |
line wrap: on
line diff
--- a/src/zorn.agda Mon Jun 06 17:18:05 2022 +0900 +++ b/src/zorn.agda Tue Jun 07 02:18:25 2022 +0900 @@ -235,8 +235,8 @@ field x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -record ZChain ( A : HOD ) {x : Ordinal} (ax : odef A x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) - (sup : (C : HOD ) → ( C ⊆' A) → IsTotalOrderSet C → Ordinal) ( z : Ordinal ) : Set (Level.suc n) where +record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) + ( z : Ordinal ) : Set (Level.suc n) where field chain : HOD chain⊆A : chain ⊆' A @@ -250,6 +250,15 @@ → * a < * b → odef chain b fc∨sup : {a : Ordinal } → a o< osuc z → ( 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 a<b za zb {i} zai = TransFinite0 (ind i) a where + open ZChain + ind : (i a : Ordinal) → ((y : Ordinal) → y o< a → odef (ZChain.chain zb) i) → odef (ZChain.chain zb) i + ind = ? + + record Maximal ( A : HOD ) : Set (Level.suc n) where field maximal : HOD @@ -319,12 +328,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 ) ⟫ - zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A as f mf supO (& 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 as (cf nmx) (cf-is-≤-monotonic nmx) supO (& 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 (subst (λ k → odef A k ) &iso as ) f mf supO (& 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) @@ -332,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 (subst (λ k → odef A k ) &iso as ) f mf supO (& 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 @@ -380,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 (subst (λ k → odef A k ) &iso as ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& 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 ̄ @@ -392,19 +401,19 @@ -- 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 ya f mf supO z ) → { y : Ordinal } → (ya : odef A y) → ZChain A ya f mf supO 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 ay f mf supO (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 ay f mf supO 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 @@ -416,7 +425,7 @@ zc11 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox ... | 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 ay f mf supO x + ... | 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 chain = ZChain.chain zc0 zc17 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) → @@ -425,7 +434,7 @@ 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 ay f mf supO 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 ) @@ -548,7 +557,7 @@ ; initial = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} ; fc∨sup = {!!} } ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b y<x = {!!} where - UnionZ : ZChain A ay f mf supO 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 @@ -558,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 ay f mf supO (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 @@ -569,11 +578,6 @@ 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 = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) } - Uz-mono : { a b : Ordinal } → (ua : odef Uz a) (ub : odef Uz b ) → a o< b → b o< x → ZChain.chain (uzc ua) ⊆' ZChain.chain (uzc ub) - Uz-mono {a} {b} ua ub a<b b<x {i} = z40 where - z40 : odef (ZChain.chain (uzc ua)) i → odef (ZChain.chain (uzc ub)) i - z40 uai = ZChain.is-max (uzc ub) (ZChain.chain∋x (uzc ub)) {!!} {!!} - (ZChain.fc∨sup (uzc ub) {!!} {!!} ) ? u-total : IsTotalOrderSet Uz u-total {x} {y} ux uy = {!!} --- ux ⊆ uy ∨ uy ⊆ ux @@ -594,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 ya f mf supO (& A) - zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A ya f mf supO z } (ind f mf) (& A) - zorn04 : ZChain A (subst (λ k → odef A k ) &iso as ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& 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 ) -- usage (see filter.agda )