Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 657:5e056537807d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 02 Jul 2022 10:51:48 +0900 |
| parents | db9477c80dce |
| children | a7a0df28086d |
| files | src/OrdUtil.agda src/zorn.agda |
| diffstat | 2 files changed, 49 insertions(+), 127 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OrdUtil.agda Sat Jul 02 07:52:05 2022 +0900 +++ b/src/OrdUtil.agda Sat Jul 02 10:51:48 2022 +0900 @@ -82,6 +82,11 @@ ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a (ordtrans lt <-osuc ) ) ... | tri> ¬a ¬b c = ⊥-elim (¬a (ordtrans lt <-osuc ) ) +ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y +ord≤< {x} {y} {z} x<z z≤y with osuc-≡< z≤y +... | case1 z=y = subst (λ k → x o< k ) z=y x<z +... | case2 z<y = ordtrans x<z z<y + -- o<-irr : { x y : Ordinal } → { lt lt1 : x o< y } → lt ≡ lt1 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob
--- a/src/zorn.agda Sat Jul 02 07:52:05 2022 +0900 +++ b/src/zorn.agda Sat Jul 02 10:51:48 2022 +0900 @@ -262,34 +262,13 @@ → ( chainf : Ordinal → HOD ) → ( lt : ( z : Ordinal ) → z o< x → Chain A f ay z ( chainf z )) → Chain A f ay x record { od = record { def = λ z → odef A z ∧ (UChain chainf x z ∨ FClosure A f y z ) } - ; odmax = & A ; <odmax = λ {y} sy → {!!} } + ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } -Chain-uniq : (A : HOD ) ( f : Ordinal → Ordinal ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) - → ( Ordinal → HOD ) → Set (Level.suc n) -Chain-uniq A f {y} ay x chain with Oprev-p x -... | yes op = st1 where - px = Oprev.oprev op - st1 : Set (Level.suc n) - st1 with ODC.∋-p O A (* x) - ... | no noax = chain x ≡ chain px - ... | yes ax with ODC.p∨¬p O ( HasPrev A (chain px) ax f ) - ... | case1 pr = chain x ≡ chain px - ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (chain px) ax ) - ... | case1 is-sup = chain x ≡ schain where - schain : HOD - schain = record { od = record { def = λ x → odef (chain px) x ∨ (FClosure A f y x) } ; odmax = & A ; <odmax = λ {y} sy → {!!} } - ... | case2 ¬x=sup = chain x ≡ chain px -... | no ¬ox = chain x ≡ record { od = record { def = λ z → odef A z ∧ ( UChain chain x z ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = λ {y} sy → {!!} } - -record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where +record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init) ( z : Ordinal ) : Set (Level.suc n) where field - chain : Ordinal → HOD - chain-mono : {x : Ordinal} → x o≤ z → chain x ⊆' chain z - chain-uniq : Chain-uniq A f ay z chain - -record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init) (zc0 : ZChain1 A f ay (& A) ) ( z : Ordinal ) : Set (Level.suc n) where - chain : HOD - chain = ZChain1.chain zc0 z + chainf : Ordinal → HOD + chain-uniq : {x : Ordinal} → x o≤ z → Chain A f ay x (chainf x) + chain = chainf z field chain⊆A : chain ⊆' A chain∋init : odef chain init @@ -363,21 +342,21 @@ 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 ) ⟫ - sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f as0 (& A) ) (zc : ZChain A f as0 zc0 (& A) ) + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f as0 (& A) ) (total : IsTotalOrderSet (ZChain.chain zc) ) → SUP A (ZChain.chain zc) - sp0 f mf zc0 zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total + sp0 f mf zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total 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) --- --- the maximum chain has fix point of any ≤-monotonic function --- - fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f as0 (& A)) (zc : ZChain A f as0 zc0 (& A) ) + fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f as0 (& A) ) → (total : IsTotalOrderSet (ZChain.chain zc) ) - → f (& (SUP.sup (sp0 f mf zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc total)) - fixpoint f mf zc0 zc total = z14 where + → f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf zc total)) + fixpoint f mf zc total = z14 where chain = ZChain.chain zc - sp1 = sp0 f mf zc0 zc total + sp1 = sp0 f mf zc total z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) → HasPrev A chain ab f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) → * a < * b → odef chain b @@ -400,7 +379,7 @@ ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p )) ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ? (SUP.x<sup sp1 ? ) } - z14 : f (& (SUP.sup (sp0 f mf zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc total )) + z14 : f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf zc total )) z14 with total (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 ... | tri< a ¬b ¬c = ⊥-elim z16 where z16 : ⊥ @@ -421,76 +400,31 @@ -- 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 ) → (zc0 : ZChain1 A (cf nmx) as0 (& A)) (zc : ZChain A (cf nmx) as0 zc0 (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥ - z04 nmx zc0 zc total = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal sp1 )))) + z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) as0 (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥ + z04 nmx zc total = <-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 ) zc0 zc total ))) -- x ≡ f x ̄ + (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc total ))) -- x ≡ f x ̄ (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1 ))) where -- x < f x sp1 : SUP A (ZChain.chain zc) - sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc0 zc total + sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total c = & (SUP.sup sp1) -- -- create all ZChains under o< x -- - sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) - → ((z : Ordinal) → z o< x → ZChain1 A f ay z ) → ZChain1 A f ay x - sind f mf {y} ay x prev with Oprev-p x - ... | yes op = sc4 where - open ZChain1 - px = Oprev.oprev op - px<x : px o< x - px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc - sc : ZChain1 A f ay px - sc = prev px px<x - no-ext : ZChain1 A f ay x - no-ext = record { chain = s01 ; chain-mono = ? ; chain-uniq = s02 } where - s01 : Ordinal → HOD - s01 z with trio< z x - ... | tri< a ¬b ¬c = chain (prev z a ) z - ... | tri≈ ¬a b ¬c = chain (prev px px<x ) px - ... | tri> ¬a ¬b c = chain (prev px px<x ) px - s02 : Chain-uniq A f ay x s01 - s02 with trio< x x - ... | tri< a ¬b ¬c = ? - ... | tri≈ ¬a refl ¬c = ? - ... | tri> ¬a ¬b c = ? - sc4 : ZChain1 A f ay x - sc4 with ODC.∋-p O A (* x) - ... | no noax = {!!} - ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.chain sc x) ax f ) - ... | case1 pr = {!!} - ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.chain sc x) ax ) - ... | case1 is-sup = {!!} where - -- A∋sc -- x is a sup of zc - sup0 : SUP A (ZChain1.chain sc x ) - sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where - x21 : {y : HOD} → (ZChain1.chain sc x) ∋ y → (y ≡ * x) ∨ (y < * x) - x21 {y} zy with IsSup.x<sup is-sup zy - ... | case1 y=x = case1 (subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x) ) - ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x ) - sp : HOD - sp = SUP.sup sup0 - schain : HOD - schain = record { od = record { def = λ x → odef (ZChain1.chain sc x) x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!} } - ... | case2 ¬x=sup = {!!} - ... | no ¬ox = ? where - sc5 : HOD - sc5 = record { od = record { def = λ z → odef A z ∧ (UChain ? x z ∨ FClosure A f y z)} ; odmax = & A ; <odmax = λ {y} sy → {!!} } - - ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 : ZChain1 A f ay (& A)) - → ((z : Ordinal) → z o< x → ZChain A f ay zc0 z) → ZChain A f ay zc0 x - ind f mf {y} ay x zc0 prev with Oprev-p x + ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) + → ((z : Ordinal) → z o< x → ZChain A f ay z) → ZChain A f ay x + ind f mf {y} ay x prev with Oprev-p x ... | yes op = zc4 where -- -- we have previous ordinal to use induction -- px = Oprev.oprev op + zc : ZChain A f ay (Oprev.oprev op) + zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) supf : Ordinal → HOD - supf = ZChain1.chain zc0 - zc : ZChain A f ay zc0 (Oprev.oprev op) - zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) + supf = ZChain.chainf zc zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt px<x : px o< x @@ -500,12 +434,15 @@ -- no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → HasPrev A (ZChain.chain zc) ab f ∨ IsSup A (ZChain.chain zc) ab → - * a < * b → odef (ZChain.chain zc) b ) → ZChain A f ay ? x - no-extenion is-max = record { chain⊆A = ? -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc) + * a < * b → odef (ZChain.chain zc) b ) → ZChain A f ay x + no-extenion is-max = record { + chainf = {!!} + ; chain-uniq = {!!} + ; chain⊆A = {!!} -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc) + ; chain∋init = subst (λ k → odef k y ) {!!} (ZChain.chain∋init zc) ; initial = subst (λ k → {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) {!!} (ZChain.initial zc) ; f-next = subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) {!!} (ZChain.f-next zc) - ; f-total = ? - ; chain∋init = subst (λ k → odef k y ) {!!} (ZChain.chain∋init zc) + ; f-total = {!!} ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) → HasPrev A k ab f ∨ IsSup A k ab → * a < * b → odef k b ) {!!} is-max } where supf0 : Ordinal → HOD @@ -524,7 +461,7 @@ ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) - zc4 : ZChain A f ay zc0 x + zc4 : ZChain A f ay x zc4 with ODC.∋-p O A (* x) ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip zc1 : {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → @@ -533,7 +470,7 @@ zc1 {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 zc za (zc-b<x b lt) ab P a<b - ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc) ax f ) -- we have to check adding x preserve is-max ZChain A y f mf zc0 x + ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc) ax f ) -- we have to check adding x preserve is-max ZChain A y f mf x ... | case1 pr = no-extenion zc7 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next chain0 = ZChain.chain zc zc7 : {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → @@ -653,53 +590,35 @@ ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } ) ... | 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 = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = ? + ... | no ¬ox = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; initial = {!!} ; chain∋init = {!!} ; is-max = {!!} } where --- limit ordinal case supf : Ordinal → HOD - supf = ZChain1.chain zc0 - uzc : {z : Ordinal} → (u : UChain supf x z) → ZChain A f ay zc0 (UChain.u u) + supf = {!!} + uzc : {z : Ordinal} → (u : UChain supf x z) → ZChain A f ay (UChain.u u) uzc {z} u = prev (UChain.u u) (UChain.u<x u) Uz : HOD - Uz = record { od = record { def = λ z → odef A z ∧ ( UChain supf z x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = ? } + Uz = record { od = record { def = λ z → odef A z ∧ ( UChain supf z x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!} } u-next : {z : Ordinal} → odef Uz z → odef Uz (f z) - u-next {z} = ? + u-next {z} = {!!} -- (case1 u) = case1 record { u = UChain.u u ; u<x = UChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UChain.chain∋z u) } -- u-next {z} (case2 u) = case2 ( fsuc _ u ) u-initial : {z : Ordinal} → odef Uz z → * y ≤ * z - u-initial {z} = ? + u-initial {z} = {!!} -- (case1 u) = ZChain.initial ( uzc u ) (UChain.chain∋z u) -- u-initial {z} (case2 u) = s≤fc _ f mf u u-chain∋init : odef Uz y - u-chain∋init = ? -- case2 ( init ay ) + u-chain∋init = {!!} -- case2 ( init ay ) supf0 : Ordinal → HOD supf0 z with trio< z x - ... | tri< a ¬b ¬c = ZChain1.chain zc0 z + ... | tri< a ¬b ¬c = {!!} ... | tri≈ ¬a b ¬c = Uz ... | tri> ¬a ¬b c = Uz u-mono : {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x - ... | s | t = ? - - seq : Uz ≡ supf0 x - seq with trio< x x - ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) - ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b c = refl - seq<x : {b : Ordinal } → (b<x : b o< x ) → ZChain1.chain zc0 b ≡ supf0 b - seq<x {b} b<x with trio< b x - ... | tri< a ¬b ¬c = cong (λ k → ZChain1.chain zc0 b) o<-irr -- b<x ≡ a - ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) - ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) - ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y - ord≤< {x} {y} {z} x<z z≤y with osuc-≡< z≤y - ... | case1 z=y = subst (λ k → x o< k ) z=y x<z - ... | case2 z<y = ordtrans x<z z<y + ... | s | t = {!!} - SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain1 A f ay (& A) - SZ0 f mf ay = TransFinite {λ z → ZChain1 A f ay z} (sind f mf ay ) (& A) - - SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f ay (SZ0 f mf ay) (& A) - SZ f mf {y} ay = TransFinite {λ z → ZChain A f ay (SZ0 f mf ay) z } (λ x → ind f mf ay x (SZ0 f mf ay) ) (& A) + SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f ay (& A) + SZ f mf {y} ay = TransFinite {λ z → ZChain A f ay z } (λ x → ind f mf ay x ) (& A) zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM @@ -711,15 +630,13 @@ zorn01 = proj1 zorn03 zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x) zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x ) - ... | yes ¬Maximal = ⊥-elim ( z04 nmx zc0 zorn04 total ) where + ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04 total ) where -- if we have no maximal, make ZChain, which contradict SUP condition nmx : ¬ Maximal A 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) ) ⟫ - zc0 : ZChain1 A (cf nmx) as0 (& A) - zc0 = TransFinite {λ z → ZChain1 A (cf nmx) as0 z} (sind (cf nmx) (cf-is-≤-monotonic nmx) as0) (& A) - zorn04 : ZChain A (cf nmx) as0 zc0 (& A) + zorn04 : ZChain A (cf nmx) as0 (& A) zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) total : IsTotalOrderSet (ZChain.chain zorn04) total {a} {b} = zorn06 where