Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 543:f0b45446c7ea
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 27 Apr 2022 04:04:30 +0900 |
| parents | 3826221c61a6 |
| children | 27bb51b7f012 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 50 insertions(+), 27 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Apr 26 16:10:30 2022 +0900 +++ b/src/zorn.agda Wed Apr 27 04:04:30 2022 +0900 @@ -162,7 +162,6 @@ A∋maximal : A ∋ maximal ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x -- A is Partial, use negative - -- -- inductive maxmum tree from x -- tree structure @@ -198,6 +197,7 @@ chain : HOD chain⊆A : chain ⊆ A chain∋x : odef chain x + ¬chain∋x>z : { a : Ordinal } → z o< osuc a → ¬ odef chain a f-total : IsTotalOrderSet chain f-next : {a : Ordinal } → odef chain a → a o< z → odef chain (f a) f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) @@ -237,6 +237,8 @@ x-is-maximal nmx {x} ax nogt m am = ⟪ subst (λ k → odef A k) &iso (subst (λ k → odef A k ) (sym &iso) ax) , ¬x<m ⟫ where ¬x<m : ¬ (* x < * m) ¬x<m x<m = ∅< {Gtx (subst (λ k → odef A k ) (sym &iso) ax)} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫ (≡o∅→=od∅ nogt) + + -- Uncountable acending chain by axiom of choice cf : ¬ Maximal A → Ordinal → Ordinal cf nmx x with ODC.∋-p O A (* x) ... | no _ = o∅ @@ -254,6 +256,7 @@ cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫ 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 (& 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)) @@ -262,6 +265,12 @@ sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A 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 + zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y) + + --- + --- sup is fix point in maximum chain + --- z03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf supO (& A)) → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc )) z03 f mf zc = z14 where @@ -272,6 +281,8 @@ ∨ (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 z10 = ZChain.is-max zc + z11 : & (SUP.sup sp1) o< & A + z11 = c<→o< ( SUP.A∋maximal sp1) 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 ) @@ -281,7 +292,7 @@ ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt z14 : f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc)) - z14 with IsStrictTotalOrder.compare (ZChain.f-total zc ) (me (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 {!!} ))) (me z12 ) + z14 with IsStrictTotalOrder.compare (ZChain.f-total zc ) (me (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 z11 ))) (me z12 ) ... | tri< a ¬b ¬c = ⊥-elim z16 where z16 : ⊥ z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 )) @@ -290,7 +301,7 @@ ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b ) ... | tri> ¬a ¬b c = ⊥-elim z17 where z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) - z15 = SUP.x<sup sp1 (subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso) (ZChain.f-next zc z12 {!!} ) ) + z15 = SUP.x<sup sp1 (subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso) (ZChain.f-next zc z12 z11 ) ) z17 : ⊥ z17 with z15 ... | case1 eq = ¬b eq @@ -303,11 +314,12 @@ 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 y ) - → {a b : Ordinal} (ca : odef (ZChain.chain zc0) a) - → odef A b → a o< x → Prev< A (ZChain.chain zc0) (incl (ZChain.chain⊆A zc0) (subst (odef (ZChain.chain zc0)) (sym &iso) ca)) 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 : 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<x P a<b = ZChain.is-max zc0 ca ab {!!} {!!} a<b + premax {x} {y} y<x f mf zc0 {a} {b} ca ab a<y P a<b = ZChain.is-max zc0 ca ab a<y P a<b -- Union of ZFChain UZFChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (B : Ordinal) → ( (y : Ordinal) → y o< B → ZChain A sa f mf supO y ) → HOD @@ -324,12 +336,22 @@ zc0 : ZChain A sa f mf supO (Oprev.oprev op) zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) zc1 : ZChain A sa f mf supO x - zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!} ; f-immediate = {!!} - ; chain∋x = ZChain.chain∋x zc0 ; is-max = {!!} } + zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 + ; f-next = zc20 (ZChain.f-next zc0) ; f-immediate = ZChain.f-immediate zc0 + ; ¬chain∋x>z = λ {a} x<oa → ZChain.¬chain∋x>z zc0 (ordtrans (subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc ) x<oa ) + ; chain∋x = ZChain.chain∋x zc0 ; is-max = λ za ba a<x → zc20 (λ za a<x → ZChain.is-max zc0 za ba a<x ) za a<x } where + zc20 : {P : Ordinal → Set n} → ({a : Ordinal} → odef (ZChain.chain zc0) a → a o< px → P a) + → {a : Ordinal} → (za : odef (ZChain.chain zc0) a ) → (a<x : a o< x) → P a + zc20 {P} prev {a} za a<x with trio< a px + ... | tri< a₁ ¬b ¬c = prev za a₁ + ... | tri≈ ¬a b ¬c = ⊥-elim ( ZChain.¬chain∋x>z zc0 (subst (λ k → k o< osuc a) b <-osuc ) za ) + ... | tri> ¬a ¬b c = ⊥-elim ( ZChain.¬chain∋x>z zc0 (ordtrans c <-osuc ) za ) ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x px = Oprev.oprev op zc0 : ZChain A sa f mf supO (Oprev.oprev op) zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) + 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 @@ -347,18 +369,21 @@ zc5 : HOD zc5 = record { od = record { def = λ z → odef (ZChain.chain zc0) z ∨ (z ≡ f x) } ; odmax = & A ; <odmax = {!!} } ⊆-zc5 : zc5 ⊆ A - ⊆-zc5 = record { incl = λ lt → {!!} } + ⊆-zc5 = record { incl = λ {y} lt → zc15 lt } where + zc15 : {z : Ordinal } → ( odef (ZChain.chain zc0) z ∨ (z ≡ f x) ) → 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 ax ) ) 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 ax ) - ... | ⟪ case1 x=fx , afx ⟫ = tri≈ {!!} zc13 {!!} where + ... | ⟪ case1 x=fx , afx ⟫ = tri≈ ( z01 ax (Afx ax) (case1 (sym zc13))) zc13 (z01 (Afx ax) ax (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> {!!} {!!} zc14 where + ... | ⟪ case2 x<fx , afx ⟫ = tri> (z01 ax (Afx ax) (case2 zc14)) (λ lt → z01 (Afx ax) ax (case1 lt) zc14) zc14 where zc14 : * x < * (f x) - zc14 = subst₂ (λ j k → j < k ) {!!} (subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym &iso ))) x<fx + zc14 = subst (λ k → * x < k ) (subst (λ k → * (f x) ≡ 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₁) @@ -368,19 +393,13 @@ ... | 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))) ... | tri< a₁ ¬b ¬c = {!!} - ... | tri≈ ¬a b₁ ¬c = subst₂ (λ j k → Tri ( j < k ) (j ≡ k) ( k < j ) ) {!!} {!!} ( fx=zc (subst (λ k → odef chain k) {!!} c )) where - zc11 : & a ≡ f x - zc11 = fx + ... | 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 y ) (zc8 (incl ( ZChain.chain⊆A zc0 ) c) fb) (cong (λ k → * ( f ( & k ))) b₁) - zc12 : Tri (a < b) (a ≡ b) (b < a) - zc12 with mf x (subst (λ k → odef A k) &iso ax ) - ... | ⟪ case1 x=fx , afx ⟫ = tri≈ {!!} zc13 {!!} where - zc13 : a ≡ b - zc13 = subst₂ (λ j k → j ≡ k ) (subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym zc11))) zc10 (sym ( x=fx )) - ... | ⟪ case2 x<fx , afx ⟫ = tri> {!!} {!!} zc14 where - zc14 : b < a - zc14 = subst₂ (λ j k → j < k ) zc10 (subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym zc11))) x<fx + zc11 : * (f x) ≡ a + zc11 = subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym fx)) + zc12 : odef chain x + 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} @@ -390,11 +409,15 @@ ... | 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 = ZChain.chain∋x zc0 ; is-max = {!!} } -- no extention ind f mf x prev | no ¬ox with trio< (& A) x --- limit ordinal case - ... | tri< a ¬b ¬c = 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 = {!!} } where + ... | tri< a ¬b ¬c = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 + ; f-next = {!!} + ; f-immediate = {!!} ; chain∋x = ZChain.chain∋x zc0 ; is-max = {!!} } where zc0 = prev (& A) a ... | tri≈ ¬a b ¬c = {!!} - ... | tri> ¬a ¬b c = {!!} + ... | tri> ¬a ¬b c = record { chain = uzc ; chain⊆A = record { incl = λ {x} lt → proj1 lt } ; f-total = {!!} ; f-next = {!!} + ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} } where + uzc : HOD + uzc = UZFChain f mf x prev zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x = zorn02 } where