Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 879:6222efcf3b04
MinSUP
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 30 Sep 2022 10:55:23 +0900 |
| parents | 1ec8c0cfc892 |
| children | d4839adf694d |
| files | src/zorn.agda |
| diffstat | 1 files changed, 80 insertions(+), 44 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Sep 24 10:52:57 2022 +0900 +++ b/src/zorn.agda Fri Sep 30 10:55:23 2022 +0900 @@ -97,6 +97,10 @@ open _==_ open _⊆_ +-- <-TransFinite : {A x : HOD} → {P : HOD → Set n} → x ∈ A +-- → ({x : HOD} → A ∋ x → ({y : HOD} → A ∋ y → y < x → P y ) → P x) → P x +-- <-TransFinite = ? + -- -- Closure of ≤-monotonic function f has total order -- @@ -357,6 +361,19 @@ ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy ) ... | case2 lt = ⊥-elim ( o<> sx<sy lt ) +record MinSUP ( A B : HOD ) : Set n where + field + sup : Ordinal + asm : odef A sup + x<sup : {x : Ordinal } → odef B x → (x ≡ sup ) ∨ (x << sup ) + minsup : { sup1 : Ordinal } → odef A sup1 + → ( {x : Ordinal } → odef B x → (x ≡ sup1 ) ∨ (x << sup1 )) → sup o≤ sup1 + +z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A +z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) + +-- M→S : {A B : HOD} → MinSUP A B → SUP A B +-- M→S {A} {B} ms = record { sup = MinSUP.sup ms ; as = MinSUP.asm ms ; x<sup = MinSUP.x<sup ms } record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where @@ -368,15 +385,18 @@ chain⊆A : chain ⊆' A chain⊆A = λ lt → proj1 lt field - sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x) + supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y + supf-< : {x y : Ordinal } → supf x o< supf y → supf x << supf y + minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f mf ay supf x) + sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x) + sup {x} x≤z = ? -- M→S (minsup x≤z ) + field sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) ) - csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) + csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain - supf-max : {x : Ordinal } → z o< x → supf x ≡ supf z -- supf z may different from spuf pz - supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y - supf-< : {x y : Ordinal } → supf x o< supf y → supf x << supf y + -- supf-max : {x : Ordinal } → z o< x → supf x ≡ supf z -- supf z may different from spuf pz x≤supfx : z o≤ supf z chain∋init : odef chain y @@ -410,19 +430,18 @@ ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy ) ... | case2 lt = ⊥-elim ( o<> sx<sy lt ) - supf-idem : {x : Ordinal } → supf (supf x) ≡ supf x - supf-idem {x} = ? - supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b) supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) ) + -- supf-idem : {x : Ordinal } → supf x o≤ z → supf (supf x) ≡ supf x + -- supf-idem {x} sx≤z = sup=u (supf∈A ?) sx≤z ? + fcy<sup : {u w : Ordinal } → u o≤ z → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf fcy<sup {u} {w} u≤z fc with SUP.x<sup (sup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) )) ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt ) - -- ordering is not proved here but in ZChain1 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) @@ -452,8 +471,6 @@ <-irr0 {a} {b} A∋a A∋b = <-irr z07 : {y : Ordinal} {A : HOD } → {P : Set n} → odef A y ∧ P → y o< & A z07 {y} {A} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) - z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A - z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) s : HOD s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) as : A ∋ * ( & s ) @@ -476,6 +493,50 @@ ¬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) + minsupP : ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → MinSUP A B + minsupP B B⊆A total = m02 where + xsup : (sup : Ordinal ) → Set n + xsup sup = {w : Ordinal } → odef B w → (w ≡ sup ) ∨ (w << sup ) + ∀-imply-or : {A : Ordinal → Set n } {B : Set n } + → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B + ∀-imply-or {A} {B} ∀AB with ODC.p∨¬p O ((x : Ordinal ) → A x) -- LEM + ∀-imply-or {A} {B} ∀AB | case1 t = case1 t + ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x not )) where + lemma : ¬ ((x : Ordinal ) → A x) → B + lemma not with ODC.p∨¬p O B + lemma not | case1 b = b + lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) + m00 : (x : Ordinal ) → ( ( z : Ordinal) → z o< x → ¬ (odef A z ∧ xsup z) ) ∨ MinSUP A B + m00 x = TransFinite0 ind x where + ind : (x : Ordinal) → ((z : Ordinal) → z o< x → ( ( w : Ordinal) → w o< z → ¬ (odef A w ∧ xsup w )) ∨ MinSUP A B) + → ( ( w : Ordinal) → w o< x → ¬ (odef A w ∧ xsup w) ) ∨ MinSUP A B + ind x prev = ∀-imply-or m01 where + m01 : (z : Ordinal) → (z o< x → ¬ (odef A z ∧ xsup z)) ∨ MinSUP A B + m01 z with trio< z x + ... | tri≈ ¬a b ¬c = case1 ( λ lt → ⊥-elim ( ¬a lt ) ) + ... | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim ( ¬a lt ) ) + ... | tri< a ¬b ¬c with prev z a + ... | case2 mins = case2 mins + ... | case1 not with ODC.p∨¬p O (odef A z ∧ xsup z) + ... | case1 mins = case2 record { sup = z ; asm = proj1 mins ; x<sup = proj2 mins ; minsup = m04 } where + m04 : {sup1 : Ordinal} → odef A sup1 → ({w : Ordinal} → odef B w → (w ≡ sup1) ∨ (w << sup1)) → z o≤ sup1 + m04 {s} as lt with trio< z s + ... | tri< a ¬b ¬c = o<→≤ a + ... | tri≈ ¬a b ¬c = o≤-refl0 b + ... | tri> ¬a ¬b s<z = ⊥-elim ( not s s<z ⟪ as , lt ⟫ ) + ... | case2 notz = case1 (λ _ → notz ) + m03 : ¬ ((z : Ordinal) → z o< & A → ¬ odef A z ∧ xsup z) + m03 not = ⊥-elim ( not s1 (z09 (SUP.as S)) ⟪ SUP.as S , m05 ⟫ ) where + S : SUP A B + S = supP B B⊆A total + s1 = & (SUP.sup S) + m05 : {w : Ordinal } → odef B w → (w ≡ s1 ) ∨ (w << s1 ) + m05 {w} bw with SUP.x<sup S {* w} (subst (λ k → odef B k) (sym &iso) bw ) + ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) eq) ) + ... | case2 lt = case2 ( subst (λ k → _ < k ) (sym *iso) lt ) + m02 : MinSUP A B + m02 = dont-or (m00 (& A)) m03 + -- Uncountable ascending chain by axiom of choice cf : ¬ Maximal A → Ordinal → Ordinal cf nmx x with ODC.∋-p O A (* x) @@ -515,31 +576,6 @@ uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) - x≤sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) - (zc : ZChain A f mf ay x ) → x o≤ & (SUP.sup (sp0 f mf ay zc)) - x≤sp0 f mf {x} ay zc with trio< x (& (SUP.sup (sp0 f mf ay zc))) - ... | tri< a ¬b ¬c = o<→≤ a - ... | tri≈ ¬a b ¬c = o≤-refl0 b - ... | tri> ¬a ¬b sp<sp0 = ? where - sp1 : {z : Ordinal } → z o≤ x → SUP A (UnionCF A f mf ay (ZChain.supf zc) z) - sp1 {z} z≤x = ZChain.sup zc z≤x - - record MinSUP ( A B : HOD ) (z : Ordinal) : Set (Level.suc n) where - field - sup : HOD - asm : A ∋ sup - x<sup : {x : HOD} → B ∋ x → (& x) o< z → (x ≡ sup ) ∨ (x < sup ) - minsup : {x sup1 : HOD} → B ∋ x → (& x) o< z → (x ≡ sup1 ) ∨ (x < sup1 ) → sup ≤ sup1 - - msupP : {B : HOD} → MinSUP A B (& A) - msupP {B} = tf (& A) where - ind : (x : Ordinal) → ((y : Ordinal) → y o< x → MinSUP A B y) → MinSUP A B x - ind x prev = ? - tf : (z : Ordinal) → MinSUP A B z - tf z = TransFinite {λ x → MinSUP A B x } ind z - - M→S : {B : HOD} {z : Ordinal } → (& B) o< z → MinSUP A B z → SUP A B - M→S {B} lt ms = record { sup = MinSUP.sup ms ; as = MinSUP.asm ms ; x<sup = ? } -- -- Second TransFinite Pass for maximality @@ -842,7 +878,7 @@ supf1 : Ordinal → Ordinal supf1 z with trio< z px ... | tri< a ¬b ¬c = supf0 z - ... | tri≈ ¬a b ¬c = px + ... | tri≈ ¬a b ¬c = px --- supf px ≡ px ... | tri> ¬a ¬b c = sp1 pchainp : HOD @@ -929,9 +965,9 @@ ... | case1 eq = ? ... | case2 lt = ? - ... | case2 px<spfx = record { supf = supf0 ; asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono - ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where - + ... | case2 px<spfx = ? where + -- record { supf = supf0 ; asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono + -- ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where supf1 : Ordinal → Ordinal supf1 z with trio< z px ... | tri< a ¬b ¬c = supf0 z @@ -1136,8 +1172,8 @@ zc70 pr xsup = ? no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x - no-extension ¬sp=x = record { supf = supf1 ; sup=u = sup=u - ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } where + no-extension ¬sp=x = ? where -- record { supf = supf1 ; sup=u = sup=u + -- ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } where supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z pchain0=1 : pchain ≡ pchain1 @@ -1185,8 +1221,8 @@ -- we have to check adding x preserve is-max ZChain A y f mf x ... | case1 pr = no-extension {!!} ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax ) - ... | case1 is-sup = record { supf = supf1 ; sup=u = {!!} - ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!}; asupf = {!!} } -- where -- x is a sup of (zc ?) + ... | case1 is-sup = ? -- record { supf = supf1 ; sup=u = {!!} + -- ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!}; asupf = {!!} } -- where -- x is a sup of (zc ?) ... | case2 ¬x=sup = no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A)