Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 527:634c4a66cfcf
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 19 Apr 2022 11:24:55 +0900 |
parents | 7e59e0aeaa73 |
children | 8facdd7cc65a |
files | src/zorn.agda |
diffstat | 1 files changed, 31 insertions(+), 65 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Apr 18 23:52:31 2022 +0900 +++ b/src/zorn.agda Tue Apr 19 11:24:55 2022 +0900 @@ -107,7 +107,7 @@ -- El-irr : {A : HOD} → {x y : Element A } → elm x ≡ elm y → x ≡ y -- El-irr {A} {x} {y} eq = El-irr2 A eq ( is-elm-irr A eq ) -record Set≈ (A B : Ordinal ) : Set n where +record _Set≈_ (A B : Ordinal ) : Set n where field fun← : {x : Ordinal } → odef (* A) x → Ordinal fun→ : {x : Ordinal } → odef (* B) x → Ordinal @@ -116,10 +116,10 @@ fiso← : {x : Ordinal } → ( lt : odef (* B) x ) → fun← ( funA lt ) ≡ x fiso→ : {x : Ordinal } → ( lt : odef (* A) x ) → fun→ ( funB lt ) ≡ x -open Set≈ -record OS≈ {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) : Set (Level.suc n) where +open _Set≈_ +record _OS≈_ {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) : Set (Level.suc n) where field - iso : Set≈ (& A) (& B) + iso : (& A ) Set≈ (& B) fmap : {x y : Ordinal} → (ax : odef A x) → (ay : odef A y) → * x < * y → * (fun← iso (subst (λ k → odef k x) (sym *iso) ax)) < * (fun← iso (subst (λ k → odef k y) (sym *iso) ay)) @@ -127,13 +127,18 @@ Cut< A x = record { od = record { def = λ y → ( odef A y ) ∧ ( x < * y ) } ; odmax = & A ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (proj1 lt))) } -Cut<TA : {A : HOD} → (TA : IsTotalOrderSet A ) ( x : HOD )→ IsTotalOrderSet ( Cut< A x ) -Cut<TA {A} TA x = record { isEquivalence = record { refl = refl ; trans = trans ; sym = sym } +Cut<T : {A : HOD} → (TA : IsTotalOrderSet A ) ( x : HOD )→ IsTotalOrderSet ( Cut< A x ) +Cut<T {A} TA x = record { isEquivalence = record { refl = refl ; trans = trans ; sym = sym } ; trans = λ {x} {y} {z} → IsStrictTotalOrder.trans TA {me (proj1 (is-elm x))} {me (proj1 (is-elm y))} {me (proj1 (is-elm z))} ; - compare = λ x y → IsStrictTotalOrder.compare TA (me (proj1 (is-elm x))) (me (proj1 (is-elm y))) } + compare = λ x y → IsStrictTotalOrder.compare TA (me (proj1 (is-elm x))) (me (proj1 (is-elm y))) } -triTO : {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) → {!!} -triTO = {!!} +record _OS<_ {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) : Set (Level.suc n) where + field + x : HOD + iso : TA OS≈ (Cut<T TA x) + +OS<-cmp : {x : HOD} → Trichotomous {_} {IsTotalOrderSet x} _OS≈_ _OS<_ +OS<-cmp A B = {!!} record ZChain ( A : HOD ) (y : Ordinal) : Set (Level.suc n) where field @@ -223,15 +228,15 @@ -- -- extract single chain from countable infinite chains -- -ChainClosure : (A : HOD) (s : Ordinal) → (next : Ordinal → Ordinal ) → HOD -ChainClosure A s next = record { od = record { def = λ x → Chain A s next x } ; odmax = & A ; <odmax = cc01 } where +TransitiveClosure : (A : HOD) (s : Ordinal) → (next : Ordinal → Ordinal ) → HOD +TransitiveClosure A s next = record { od = record { def = λ x → Chain A s next x } ; odmax = & A ; <odmax = cc01 } where cc01 : {y : Ordinal} → Chain A s next y → y o< & A cc01 {y} cy = subst (λ k → k o< & A ) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) ( ct∈A A s next cy ) ) ) cton0 : (A : HOD ) (s : Ordinal) → (next : Ordinal → Ordinal ) {y : Ordinal } → Chain A s next y → ℕ cton0 A s next (cfirst _) = zero cton0 A s next (csuc x ax z _) = suc (cton0 A s next z) -cton : (A : HOD ) (s : Ordinal) → (next : Ordinal → Ordinal ) → Element (ChainClosure A s next) → ℕ +cton : (A : HOD ) (s : Ordinal) → (next : Ordinal → Ordinal ) → Element (TransitiveClosure A s next) → ℕ cton A s next y = cton0 A s next (is-elm y) cinext : (A : HOD) {x max : Ordinal } → (ax : A ∋ * x ) → (ifc : InfiniteChain A max ax ) → Ordinal → Ordinal @@ -241,7 +246,7 @@ InFCSet : (A : HOD) → {x max : Ordinal} (ax : A ∋ * x) → (ifc : InfiniteChain A max ax ) → HOD -InFCSet A {x} ax ifc = ChainClosure (IChainSet A ax) x (cinext A ax ifc ) +InFCSet A {x} ax ifc = TransitiveClosure (IChainSet A ax) x (cinext A ax ifc ) InFCSet⊆A : (A : HOD) → {x max : Ordinal} (ax : A ∋ * x) → (ifc : InfiniteChain A max ax ) → InFCSet A ax ifc ⊆ A InFCSet⊆A A {x} ax ifc = record { incl = λ {y} lt → incl (IChainSet⊆A ax) ( @@ -253,11 +258,11 @@ ... | no not = ⊥-elim ( not ay ) ... | yes ay1 = InfiniteChain.c-infinite ifc y (subst (λ k → odef (IChainSet A ax) k) &iso ay ) -ChainClosure-is-total : (A : HOD) → {x max : Ordinal} (ax : A ∋ * x) +TransitiveClosure-is-total : (A : HOD) → {x max : Ordinal} (ax : A ∋ * x) → IsPartialOrderSet A → (ifc : InfiniteChain A max ax ) → IsTotalOrderSet ( InFCSet A ax ifc ) -ChainClosure-is-total A {x} ax PO ifc = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO +TransitiveClosure-is-total A {x} ax PO ifc = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z} ; compare = cmp } where IPO : IsPartialOrderSet (InFCSet A ax ifc ) IPO = ⊆-IsPartialOrderSet record { incl = λ {y} lt → incl (InFCSet⊆A A {x} ax ifc) lt} PO @@ -294,11 +299,11 @@ ct011 : * oy1 < * ( IChainSup>.y (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) ) ct011 = IChainSup>.y>x (InfiniteChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet A ax) k) &iso ay1 )) ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c ) - ct12 : {y z : Element (ChainClosure B x cnext) } → elm y ≡ elm z → elm y < elm z → ⊥ + ct12 : {y z : Element (TransitiveClosure B x cnext) } → elm y ≡ elm z → elm y < elm z → ⊥ ct12 {y} {z} y=z y<z = IsStrictPartialOrder.irrefl IPO {y} {z} y=z y<z - ct13 : {y z : Element (ChainClosure B x cnext) } → elm y < elm z → elm z < elm y → ⊥ + ct13 : {y z : Element (TransitiveClosure B x cnext) } → elm y < elm z → elm z < elm y → ⊥ ct13 {y} {z} y<z y>z = IsStrictPartialOrder.irrefl IPO {y} {y} refl ( IsStrictPartialOrder.trans IPO {y} {z} {y} y<z y>z ) - ct17 : (x1 : Element (ChainClosure B x cnext)) → Chain B x cnext (& (elm x1)) + ct17 : (x1 : Element (TransitiveClosure B x cnext)) → Chain B x cnext (& (elm x1)) ct17 x1 = is-elm x1 cmp : Trichotomous _ _ cmp x1 y with NP.<-cmp (cton B x cnext x1) (cton B x cnext y) @@ -320,6 +325,12 @@ ct15 : ¬ (elm x1 < elm y) ct15 lt = ct13 {x1} {y} lt (subst₂ (λ j k → j < k ) *iso *iso (ct-monotonic (is-elm y) (is-elm x1) c ) ) +extendInfiniteChain : (A : HOD) → {x mx y my : Ordinal} (ax : A ∋ * x) (ay : A ∋ * y) + → IsPartialOrderSet A + → (ifcx : InfiniteChain A mx ax ) → (ifcy : InfiniteChain A my ay ) + → * mx < * my + → InfiniteChain A my ax +extendInfiniteChain = ? record IsFC (A : HOD) {x : Ordinal} (ax : A ∋ * x) (y : Ordinal) : Set n where field @@ -423,57 +434,12 @@ y<z = ic→< {A} PO y (subst (λ k → odef A k) &iso ay) (IChained.iy (proj2 icy)) (subst (λ k → ic-connect k (IChained.iy (proj2 icy))) &iso (IChained.ic (proj2 icy))) - -record Indirect< {x z : HOD} (x<z : x < z ) : Set (Level.suc n) where - field - y y1 : HOD - =∨< : ( y ≡ y1 ) ∨ ( y < y1 ) - dirct : ¬ ( (x < y ) ∧ ( y1 < z )) - -record NChain ( A : HOD ) (f : { x : HOD} → A ∋ x → HOD) (min : HOD) : Set (Level.suc n) where - field - N : HOD - N⊆A : N ⊆ A - nmin : N ∋ min - is-min : (x : HOD) → N ∋ x → ( min ≡ x ) ∨ ( min < x ) - total : IsTotalOrderSet N - A∋fx : { x : HOD} → (ax : A ∋ x ) → A ∋ f ax - atomic : { x y : HOD } → (nx : N ∋ x) → (x<y : x < y) → ¬ Indirect< x<y → y ≡ f (incl N⊆A nx ) - record SUP ( A B : HOD ) : Set (Level.suc n) where field sup : HOD A∋maximal : A ∋ sup x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup ) -- B is Total, use positive -record Zfixpoint (A : HOD ) (f : { x : HOD} → A ∋ x → HOD) : Set (Level.suc n) where - field - fx : HOD - afx : A ∋ fx - is-fx : fx ≡ f afx - -Zorn-fixpoint : { A : HOD } - → o∅ o< & A - → IsPartialOrderSet A - → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B ) -- SUP condition - → (f : { x : HOD} → A ∋ x → HOD ) → ( A∋fx : {x : HOD} (ax : A ∋ x ) → A ∋ f ax ) - → (f≤ : {x : HOD} → (ax : A ∋ x ) → (x ≡ f ax ) ∨ (x < f ax )) - → Zfixpoint A f -Zorn-fixpoint = {!!} - -record Zmono (A : HOD ) : Set (Level.suc n) where - field - f : { x : HOD} → A ∋ x → HOD - A∋fx : { x : HOD} → (ax : A ∋ x ) → A ∋ f ax - monotonic : { x y : HOD} → (ax : A ∋ x ) → x < f ax - -Zorn-monotonic : { A : HOD } - → o∅ o< & A - → IsPartialOrderSet A - → ¬ ( Maximal A ) - → Zmono A -Zorn-monotonic = {!!} - Zorn-lemma : { A : HOD } → o∅ o< & A → IsPartialOrderSet A @@ -503,7 +469,7 @@ nxa : A ∋ * nx nxa = {!!} -- cinext∈A A ax ifc (& (SUP.sup sup)) {!!} zc5 : InfiniteChain A max ax → ⊥ - zc5 ifc = zc6 ifc ( supP (InFCSet A ax ifc) (InFCSet⊆A A {x} ax ifc) ( ChainClosure-is-total A {x} ax PO ifc )) + zc5 ifc = zc6 ifc ( supP (InFCSet A ax ifc) (InFCSet⊆A A {x} ax ifc) ( TransitiveClosure-is-total A {x} ax PO ifc )) z03 : {x : Ordinal } → (ax : A ∋ * x ) → InfiniteChain A (& A) ax → ⊥ z03 {x} ax ifc = {!!} -- ZChain is not compatible with the SUP condition @@ -539,7 +505,7 @@ zc6 : (ifc : InfiniteChain A x ax ) → ¬ SUP A (B ifc) zc6 = {!!} FC-is-total : (ifc : InfiniteChain A x ax) → IsTotalOrderSet (B ifc) - FC-is-total ifc = ChainClosure-is-total A ax PO ifc + FC-is-total ifc = TransitiveClosure-is-total A ax PO ifc B⊆A : (ifc : InfiniteChain A x ax) → B ifc ⊆ A B⊆A = {!!} ifc : InfiniteChain A x (subst (OD.def (od A)) (sym &iso) ax) → InfiniteChain A x ax