Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 554:0687736285ce
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 29 Apr 2022 14:49:25 +0900 |
| parents | 567a1a9f3e0a |
| children | 726b6dac5eaa |
| files | src/zorn.agda |
| diffstat | 1 files changed, 54 insertions(+), 58 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Apr 28 19:00:40 2022 +0900 +++ b/src/zorn.agda Fri Apr 29 14:49:25 2022 +0900 @@ -42,6 +42,12 @@ _≤_ : (x y : HOD) → Set (Level.suc n) x ≤ y = ( x ≡ y ) ∨ ( x < y ) +≤-ftrans : {x y z : HOD} → x ≤ y → y ≤ z → x ≤ z +≤-ftrans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl +≤-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z +≤-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y +≤-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z ) + open _==_ open _⊆_ @@ -67,9 +73,45 @@ ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧ odef A (f x ) data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where - init : {x : Ordinal} → odef A s → FClosure A f s s + init : odef A s → FClosure A f s s fsuc : {x : Ordinal} ( p : FClosure A f s x ) → FClosure A f s (f x) +open import Data.Nat hiding ( _<_ ; _≤_ ) +open import Data.Nat.Properties +open import nat + +fcn : {A : HOD} {s x : Ordinal} {f : Ordinal → Ordinal} → FClosure A f s x → ℕ +fcn (init as) = zero +fcn (fsuc p) = suc ( fcn p ) + +fcn-inject : {A : HOD} {s x y : Ordinal } (f : Ordinal → Ordinal) → (fcx : FClosure A f s x) → (fcy : FClosure A f s y ) → fcn fcx ≡ fcn fcy → x ≡ y +fcn-inject f (init x) (init x₁) refl = refl +fcn-inject f (fsuc fcx) (fsuc fcy) eq = cong f ( fcn-inject f fcx fcy ( cong pred eq )) + +A∋fc : {A : HOD} {s y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → odef A y +A∋fc {A} {s} {.s} f mf (init as) = as +A∋fc {A} {s} f mf (fsuc {y} fcy) = proj2 (mf y ( A∋fc {A} {s} f mf fcy ) ) + +fcn-cmp : {A : HOD} {s x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) + → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x ) +fcn-cmp {A} {s} {x} {y} f mf cx cy with <-cmp (fcn cx) (fcn cy) +... | t = {!!} + +fcn-mono : {A : HOD} {s x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) + → (imm : { x y : Ordinal } → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) ) + → (fcx : FClosure A f s x) → (fcy : FClosure A f s y ) → fcn fcx Data.Nat.≤ fcn fcy → * x ≤ * y +fcn-mono f mf imm (init _) (init _) z≤n = case1 refl +fcn-mono {A} {s} {x} f mf imm (init sa) (fsuc {y} fcy) z≤n with proj1 (mf y (A∋fc f mf fcy ) ) +... | case1 eq = subst (λ k → * s ≤ k ) eq ( fcn-mono f mf imm (init sa) fcy z≤n ) +... | case2 lt = ≤-ftrans (fcn-mono f mf imm (init sa) fcy z≤n) (case2 lt) +fcn-mono f mf imm (fsuc fcx) (fsuc fcy) (s≤s lt) with fcn-mono f mf imm fcx fcy lt +... | case1 x=y = case1 (subst₂ (λ j k → * (f j) ≡ * (f k)) &iso &iso ( cong (λ k → * (f (& k ))) x=y ) ) +... | case2 x<y with <-cmp (fcn fcx) (fcn fcy) +... | tri< a ¬b ¬c = {!!} +... | tri≈ ¬a b ¬c = {!!} +... | tri> ¬a ¬b c = {!!} +-- = case2 {!!} -- * x < * y → * (f x) < * (f y) + record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x) ( f : Ordinal → Ordinal ) : Set n where field y : Ordinal @@ -91,6 +133,7 @@ chain : HOD chain⊆A : chain ⊆ A chain∋x : odef chain x + initial : {y : Ordinal } → odef chain y → * x < * y 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 )) ) @@ -226,7 +269,8 @@ zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay zc4 : ZChain A ay f mf supO x zc4 with ODC.∋-p O A (* px) - ... | no noapx = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 + ... | no noapx = 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 } where -- no extention zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< x → (ba : odef A b) → Prev< A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (* (& (ZChain.chain zc0))) @@ -249,16 +293,16 @@ ... | case1 b=px = subst (λ k → odef chain k ) (trans (sym (Prev<.x=fy pr )) (trans &iso (sym b=px))) ( ZChain.f-next zc0 (Prev<.ay pr)) zc9 : ZChain A ay f mf supO 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 - ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc17 } -- no extention + ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = zc17 } -- no extention ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) )) ... | case1 x=sup = record { chain = schain ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} - ; f-immediate = {!!} ; chain∋x = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where -- x is sup + ; initial = {!!} ; f-immediate = {!!} ; chain∋x = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where -- x is sup sp = SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) chain = ZChain.chain zc0 schain : HOD schain = record { od = record { def = λ x → odef chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = {!!} } ... | case2 ¬x=sup = 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 + ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = ZChain.chain∋x zc0 ; is-max = {!!} } where -- no extention z18 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< x → (ba : odef A b) → Prev< A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (* (& (ZChain.chain zc0))) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0)) @@ -268,15 +312,14 @@ z18 {a} {b} za b<x ba (case1 p) a<b = {!!} z18 {a} {b} za b<x ba (case2 p) a<b = {!!} ... | no ¬ox = {!!} where --- limit ordinal case - -- Union of ZFChain - record UZFChain (y : Ordinal) : Set n where + record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x field u : Ordinal u<x : u o< x - zuy : odef (ZChain.chain (prev u u<x ay )) y - uzc : HOD - uzc = record { od = record { def = λ y → UZFChain y } ; odmax = & A ; <odmax = {!!} } - u-total : IsTotalOrderSet uzc + zuy : odef (ZChain.chain (prev u u<x {y} ay )) z + Uz : HOD + Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A ; <odmax = {!!} } + u-total : IsTotalOrderSet Uz u-total {x} {y} ux uy = {!!} zorn00 : Maximal A @@ -300,53 +343,6 @@ 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 ) - zorn99 : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) → (x y : Ordinal) (ay : odef A y) → (zc0 : ZChain A {!!} f mf supO x) → Prev< A (ZChain.chain zc0) {!!} f → {!!} - zorn99 f mf x y ay zc0 pr = {!!} where - 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)))) - chain = ZChain.chain zc0 - zc7 : ZChain A ay f mf supO x - zc7 with trio< (Prev<.y pr) x - ... | tri< a ¬b ¬c = {!!} -- already x ∈ chain because of is-max - ... | tri≈ ¬a b ¬c = {!!} -- x ≡ z ∈ chain - ... | tri> ¬a ¬b x<z = record { chain = zc5 ; chain⊆A = ⊆-zc5 --- - ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x = case1 {!!} ; is-max = {!!} } where - -- extend with x ≡ f z where cahin ∋ z - 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 = λ {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 {!!} ) ) - 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) 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 - zc6 : IsTotalOrderSet zc5 - zc6 {a} {b} ( case1 x ) ( case1 x₁ ) = ZChain.f-total zc0 x x₁ - zc6 {a} {b} ( case2 fx ) ( case2 fx₁ ) = tri≈ {!!} (subst₂ (λ j k → j ≡ k ) *iso *iso (trans (cong (*) fx) (sym (cong (*) fx₁ ) ))) {!!} - zc6 {a} {b} ( case1 c ) ( case2 fx ) = {!!} -- subst₂ (λ j k → Tri ( j < k ) (j ≡ k) ( k < j ) ) {!!} {!!} ( fx>zc (subst (λ k → odef chain k) {!!} c )) - zc6 {a} {b} ( case2 fx ) ( case1 c ) with ODC.p∨¬p O ( Prev< A chain (incl (ZChain.chain⊆A zc0) c) f ) - ... | case2 n = {!!} - ... | case1 fb with ZChain.f-total zc0 (subst (λ k → odef chain k) (sym &iso) (Prev<.ay pr)) (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 : * 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 {!!} )) - zc12 : odef chain y - zc12 = subst (λ k → odef chain k ) (subst (λ k → & b ≡ k ) &iso (sym (cong (&) zc10))) c - ... | tri> ¬a ¬b c₁ = {!!} -- usage (see filter.agda ) -- -- _⊆'_ : ( A B : HOD ) → Set n