Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 547:379bd9b4610c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 27 Apr 2022 23:21:21 +0900 |
| parents | 3234a5f6bfcf |
| children | 5ad7a31df4f4 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 50 insertions(+), 45 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Apr 27 11:01:43 2022 +0900 +++ b/src/zorn.agda Wed Apr 27 23:21:21 2022 +0900 @@ -192,7 +192,7 @@ SupCond A B _ _ = SUP A B record ZChain ( A : HOD ) {x : Ordinal} (ax : odef A x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) - (sup : (C : Ordinal ) → (* C ⊆ A) → IsTotalOrderSet (* C) → Ordinal) : Set (Level.suc n) where + (sup : (C : Ordinal ) → (* C ⊆ A) → IsTotalOrderSet (* C) → Ordinal) ( z : Ordinal ) : Set (Level.suc n) where field chain : HOD chain⊆A : chain ⊆ A @@ -200,7 +200,7 @@ f-total : IsTotalOrderSet chain f-next : {a : Ordinal } → odef chain a → odef chain (f a) f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) - is-max : {a b : Ordinal } → (ca : odef chain a ) → (ba : odef A b) + is-max : {a b : Ordinal } → (ca : odef chain a ) → a o< z → (ba : odef A b) → Prev< A chain ba f ∨ (sup (& chain) (subst (λ k → k ⊆ A) (sym *iso) chain⊆A) (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b ) → * a < * b → odef chain b @@ -223,6 +223,8 @@ s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) sa : A ∋ * ( & s ) sa = 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 )) ) + s<A : & s o< & A + s<A = c<→o< (subst (λ k → odef A (& k) ) *iso sa ) HasMaximal : HOD HasMaximal = record { od = record { def = λ x → odef A x ∧ ( (m : Ordinal) → odef A m → ¬ (* x < * m)) } ; odmax = & A ; <odmax = z07 } no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → odef A x ∧ ((m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m) )) → ⊥ @@ -256,12 +258,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 sa f mf supO ) → SUP A (ZChain.chain zc) + zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A sa f mf supO (& 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 sa (cf nmx) (cf-is-≤-monotonic nmx) supO ) + A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& 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 sa ) f mf supO ) → SUP A (* (& (ZChain.chain zc))) + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) f mf supO (& A) ) → SUP A (* (& (ZChain.chain zc))) sp0 f mf zc = supP (* (& (ZChain.chain zc))) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc)) (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc) ) zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P @@ -270,12 +272,12 @@ --- --- sup is fix point in maximum chain --- - z03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) f mf supO ) + z03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) f mf supO (& A) ) → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc )) z03 f mf zc = z14 where chain = ZChain.chain zc sp1 = sp0 f mf zc - z10 : {a b : Ordinal } → (ca : odef chain a ) → (ab : odef A b ) + z10 : {a b : Ordinal } → (ca : odef chain a ) → a o< & A → (ab : odef A b ) → Prev< A chain ab f ∨ (supO (& chain) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc)) (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc)) ≡ b ) → * a < * b → odef chain b @@ -285,7 +287,7 @@ z12 : odef chain (& (SUP.sup sp1)) z12 with o≡? (& s) (& (SUP.sup sp1)) ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋x zc ) - ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) (SUP.A∋maximal sp1) (case2 refl ) z13 where + ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) s<A (SUP.A∋maximal sp1) (case2 refl ) z13 where z13 : * (& s) < * (& (SUP.sup sp1)) z13 with SUP.x<sup sp1 (subst (λ k → odef k (& s)) (sym *iso) ( ZChain.chain∋x zc )) ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) @@ -305,49 +307,52 @@ z17 with z15 ... | case1 eq = ¬b eq ... | case2 lt = ¬a lt - z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) (cf nmx) (cf-is-≤-monotonic nmx) supO ) → ⊥ + -- ZChain requires the Maximal + z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥ z04 nmx zc = z01 {* (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 (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc c = & (SUP.sup sp1) - premax : {x y : Ordinal} → y o< x → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain A sa f mf supO ) + premax : {x y : Ordinal} → y o< x → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain A sa f mf supO y ) → {a b : Ordinal} (ca : odef (ZChain.chain zc0) a) → (ab : odef A b) → a o< y → Prev< A (ZChain.chain zc0) ab f ∨ (supO (& (ZChain.chain zc0)) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0)) (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ b) → * a < * b → odef (ZChain.chain zc0) b - premax {x} {y} y<x f mf zc0 {a} {b} ca ab a<y P a<b = ZChain.is-max zc0 ca ab P a<b -- ca ab y P a<b + premax {x} {y} y<x f mf zc0 {a} {b} ca ab a<y P a<b = ZChain.is-max zc0 ca a<y ab P a<b -- ca ab y P a<b -- Union of ZFChain UZFChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (B : Ordinal) - → ( (y : Ordinal) → y o< B → (ya : odef A y) → ZChain A ya f mf supO ) → HOD + → ( (z : Ordinal) → z o< B → {y : Ordinal} → (ya : odef A y) → ZChain A ya f mf supO z ) → HOD UZFChain f mf B prev = record { od = record { def = λ y → odef A y ∧ (y o< B) ∧ ( (y<b : y o< B) → (ya : odef A y) → odef (ZChain.chain (prev y y<b ya )) y) } ; odmax = & A ; <odmax = z07 } - -- ZChain is not compatible with the SUP condition + -- create all ZChains under o< x ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → - ((y : Ordinal) → y o< x → (ya : odef A y) → ZChain A ya f mf supO) → (ya : odef A x) → ZChain A ya f mf supO - ind f mf x prev ax with Oprev-p x + ((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 + ind f mf x prev {y} ay with Oprev-p x ... | yes op with ODC.∋-p O A (* (Oprev.oprev op)) ... | yes apx = zc4 where -- we have previous ordinal and A ∋ op px = Oprev.oprev op apx0 = subst (λ k → odef A k ) &iso apx - zc0 : ZChain A apx0 f mf supO - zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) apx0 - ax0 : odef A (& (* x)) - ax0 = {!!} + zc0 : ZChain A ay f mf supO (Oprev.oprev op) + zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay + zc1 : {y : Ordinal } → (ay : odef A y ) → ZChain A ay f mf supO (Oprev.oprev op) + zc1 {y} ay = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay + ay0 : odef A (& (* y)) + ay0 = (subst (λ k → odef A k ) (sym &iso) ay ) Afx : { x : Ordinal } → A ∋ * x → A ∋ * (f x) Afx {x} ax = (subst (λ k → odef A k ) (sym &iso) (proj2 (mf x (subst (λ k → odef A k ) &iso ax)))) -- x is in the previous chain, use the same -- x has some y which y < x ∧ f y ≡ x -- x has no y which y < x - zc4 : ZChain A ax f mf supO - zc4 with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ax f ) - ... | case1 y = zc7 where -- we have previous < + zc4 : ZChain A ay f mf supO x + zc4 with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ay f ) + ... | case1 pr = zc7 where -- we have previous < chain = ZChain.chain zc0 - zc7 : ZChain A ax f mf supO + zc7 : ZChain A ay f mf supO x zc7 with ODC.∋-p O (ZChain.chain zc0) (* ( f x ) ) - ... | yes y = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 + ... | yes pr = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A 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 = {!!} } where -- no extention z22 : {a : Ordinal} → x o< osuc a → ¬ odef (ZChain.chain zc0) a @@ -367,23 +372,23 @@ ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x = case1 {!!} ; ¬chain∋x>z = {!!} ; is-max = {!!} } where -- extend with f x -- cahin ∋ y ∧ chain ∋ f y ∧ x ≡ f ( f y ) zc5 : HOD - zc5 = record { od = record { def = λ z → odef (ZChain.chain zc0) z ∨ (z ≡ f x) } ; odmax = & A ; <odmax = {!!} } + zc5 = record { od = record { def = λ z → odef (ZChain.chain zc0) z ∨ (z ≡ f y) } ; odmax = & A ; <odmax = {!!} } ⊆-zc5 : zc5 ⊆ A ⊆-zc5 = record { incl = λ {y} lt → zc15 lt } where - zc15 : {z : Ordinal } → ( odef (ZChain.chain zc0) z ∨ (z ≡ f x) ) → odef A z + zc15 : {z : Ordinal } → ( odef (ZChain.chain zc0) z ∨ (z ≡ f y) ) → odef A z zc15 {z} (case1 zz) = subst (λ k → odef A k ) &iso ( incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k ) (sym &iso) zz ) ) - zc15 (case2 refl) = proj2 ( mf x (subst (λ k → odef A k ) &iso {!!} ) ) + zc15 (case2 refl) = proj2 ( mf y (subst (λ k → odef A k ) &iso {!!} ) ) IPO = ⊆-IsPartialOrderSet ⊆-zc5 PO zc8 : { A B x : HOD } → (ax : A ∋ x ) → (P : Prev< A B ax f ) → * (f (& (* (Prev<.y P)))) ≡ x zc8 {A} {B} {x} ax P = subst₂ (λ j k → * ( f j ) ≡ k ) (sym &iso) *iso (sym (cong (*) ( Prev<.x=fy P))) - fx=zc : odef (ZChain.chain zc0) x → Tri (* (f x) < * x ) (* (f x) ≡ * x) (* x < * (f x) ) - fx=zc c with mf x (subst (λ k → odef A k) &iso ax0 ) - ... | ⟪ case1 x=fx , afx ⟫ = tri≈ ( z01 ax0 (Afx ax0) (case1 (sym zc13))) zc13 (z01 (Afx ax0) ax0 (case1 zc13)) where - zc13 : * (f x) ≡ * x - zc13 = subst (λ k → k ≡ * x ) (subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym &iso))) (sym ( x=fx )) - ... | ⟪ case2 x<fx , afx ⟫ = tri> (z01 ax0 (Afx ax0) (case2 zc14)) (λ lt → z01 (Afx ax0) ax0 (case1 lt) zc14) zc14 where - zc14 : * x < * (f x) - zc14 = subst (λ k → * x < k ) (subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym &iso ))) x<fx + fx=zc : odef (ZChain.chain zc0) y → Tri (* (f y) < * y ) (* (f y) ≡ * y) (* y < * (f y) ) + fx=zc c with mf y (subst (λ k → odef A k) &iso ay0 ) + ... | ⟪ case1 x=fx , afx ⟫ = tri≈ ( z01 ay0 (Afx ay0) (case1 (sym zc13))) zc13 (z01 (Afx ay0) ay0 (case1 zc13)) where + zc13 : * (f y) ≡ * y + zc13 = subst (λ k → k ≡ * y ) (subst (λ k → * (f y) ≡ k ) *iso (cong (*) (sym &iso))) (sym ( x=fx )) + ... | ⟪ case2 x<fx , afx ⟫ = tri> (z01 ay0 (Afx ay0) (case2 zc14)) (λ lt → z01 (Afx ay0) ay0 (case1 lt) zc14) zc14 where + zc14 : * y < * (f y) + zc14 = subst (λ k → * y < k ) (subst (λ k → * (f y) ≡ k ) *iso (cong (*) (sym &iso ))) x<fx cmp : Trichotomous _ _ cmp record { elm = a ; is-elm = aa } record { elm = b ; is-elm = ab } with aa | ab ... | case1 x | case1 x₁ = IsStrictTotalOrder.compare (ZChain.f-total zc0) (me x) (me x₁) @@ -391,21 +396,21 @@ ... | case1 c | case2 fx = {!!} -- subst₂ (λ j k → Tri ( j < k ) (j ≡ k) ( k < j ) ) {!!} {!!} ( fx>zc (subst (λ k → odef chain k) {!!} c )) ... | case2 fx | case1 c with ODC.p∨¬p O ( Prev< A chain (incl (ZChain.chain⊆A zc0) c) f ) ... | case2 n = {!!} - ... | case1 fb with IsStrictTotalOrder.compare (ZChain.f-total zc0) (me (subst (λ k → odef chain k) (sym &iso) (Prev<.ay y))) (me (subst (λ k → odef chain k) (sym &iso) (Prev<.ay fb))) + ... | case1 fb with IsStrictTotalOrder.compare (ZChain.f-total zc0) (me (subst (λ k → odef chain k) (sym &iso) (Prev<.ay pr))) (me (subst (λ k → odef chain k) (sym &iso) (Prev<.ay fb))) ... | tri< a₁ ¬b ¬c = {!!} ... | tri≈ ¬a b₁ ¬c = subst₂ (λ j k → Tri ( j < k ) (j ≡ k) ( k < j ) ) zc11 zc10 ( fx=zc zc12 ) where - zc10 : * x ≡ b - zc10 = subst₂ (λ j k → j ≡ k ) (zc8 ax {!!} ) (zc8 (incl ( ZChain.chain⊆A zc0 ) c) fb) (cong (λ k → * ( f ( & k ))) b₁) - zc11 : * (f x) ≡ a - zc11 = subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym fx)) - zc12 : odef chain x + zc10 : * y ≡ b + zc10 = subst₂ (λ j k → j ≡ k ) (zc8 ay {!!} ) (zc8 (incl ( ZChain.chain⊆A zc0 ) c) fb) (cong (λ k → * ( f ( & k ))) b₁) + zc11 : * (f y) ≡ a + zc11 = subst (λ k → * (f y) ≡ k ) *iso (cong (*) (sym fx)) + zc12 : odef chain y zc12 = subst (λ k → odef chain k ) (subst (λ k → & b ≡ k ) &iso (sym (cong (&) zc10))) c ... | tri> ¬a ¬b c₁ = {!!} zc6 : IsTotalOrderSet zc5 zc6 = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z} ; compare = cmp } ... | case2 not with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) {!!} {!!} ) )) - ... | case1 y = {!!} -- x is sup + ... | case1 pr = {!!} -- x is sup ... | case2 not = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} } -- no extention ... | no noapx = {!!} -- we have previous ordinal but ¬ A ∋ op @@ -432,9 +437,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 - zorn03 f mf = TransFinite {λ y → (ya : odef A y ) → ZChain A ya f mf supO } (ind f mf) (& s ) - zorn04 : ZChain A (subst (λ k → odef A k ) &iso sa ) (cf nmx) (cf-is-≤-monotonic nmx) supO + 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 sa ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& A) zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso sa ) -- usage (see filter.agda )