Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 541:f3e2cbd07e7c
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 25 Apr 2022 17:51:24 +0900 |
parents | 920a5c0568c3 |
children | 3826221c61a6 |
files | src/zorn.agda |
diffstat | 1 files changed, 32 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Apr 24 18:59:31 2022 +0900 +++ b/src/zorn.agda Mon Apr 25 17:51:24 2022 +0900 @@ -177,10 +177,10 @@ x<z : * x < * z z<y : * z < * y -record Prev< (A : HOD) {x : Ordinal } (xa : odef A x) ( f : Ordinal → Ordinal ) : Set n where +record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x) ( f : Ordinal → Ordinal ) : Set n where field y : Ordinal - ay : odef A y + ay : odef B y x=fy : x ≡ f y record SUP ( A B : HOD ) : Set (Level.suc n) where @@ -200,9 +200,10 @@ chain∋x : odef chain x f-total : IsTotalOrderSet chain f-next : {a : Ordinal } → odef chain a → odef chain (f a) - is-max : {a b : Ordinal } → (ca : odef chain a ) → odef A b → a o< z - → ( Prev< A (incl chain⊆A (subst (λ k → odef chain k ) (sym &iso) ca)) f - ∨ (sup (& chain) (subst (λ k → k ⊆ A) (sym *iso) chain⊆A) (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b )) + f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) + is-max : {a b : Ordinal } → (ca : odef chain a ) → (ba : odef A b) → a o< z + → Prev< A chain ba f + ∨ (sup (& chain) (subst (λ k → k ⊆ A) (sym *iso) chain⊆A) (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b ) → * a < * b → odef chain b Zorn-lemma : { A : HOD } @@ -266,9 +267,9 @@ z03 f mf zc = z14 where chain = ZChain.chain zc sp1 = sp0 f mf zc - z10 : {a b : Ordinal } → (ca : odef chain a ) → odef A b → a o< (& A) - → ( Prev< A (incl (ZChain.chain⊆A zc) (subst (λ k → odef chain k ) (sym &iso) ca)) f - ∨ (supO (& chain) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc)) (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc)) ≡ b )) + z10 : {a b : Ordinal } → (ca : odef chain a ) → (ab : odef A b ) → a o< (& A) + → Prev< A chain ab f + ∨ (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 z12 : odef chain (& (SUP.sup sp1)) @@ -301,6 +302,12 @@ (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where 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 → 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 -- 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 @@ -317,8 +324,8 @@ 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 = ZChain.f-next zc0 - ; chain∋x = {!!} ; is-max = {!!} } + zc1 = 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 = {!!} + ; chain∋x = ZChain.chain∋x zc0 ; is-max = {!!} } ... | 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) @@ -327,34 +334,39 @@ -- x has some y which y < x ∧ f y ≡ x -- x has no y which y < x zc4 : ZChain A sa f mf supO x - zc4 with ODC.p∨¬p O ( Prev< A ax f ) + zc4 with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ax f ) ... | case1 y = zc7 where + chain = ZChain.chain zc0 zc7 : ZChain A sa f mf supO x zc7 with ODC.∋-p O (ZChain.chain zc0) (* ( f x ) ) ... | yes y = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 - ; chain∋x = {!!} ; is-max = {!!} } -- no extention + ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} } -- no extention ... | no not = record { chain = zc5 ; chain⊆A = ⊆-zc5 - ; f-total = zc6 ; f-next = {!!} ; chain∋x = ⟪ subst (λ k → odef A (& k)) *iso sa , case1 (ZChain.chain∋x zc0) ⟫ ; is-max = {!!} } where + ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where -- extend with f x zc5 : HOD - zc5 = record { od = record { def = λ z → odef A z ∧ (odef (ZChain.chain zc0) z ∨ (z ≡ f x)) } ; odmax = & A ; <odmax = z07 } + zc5 = record { od = record { def = λ z → odef (ZChain.chain zc0) z ∨ (z ≡ f x) } ; odmax = & A ; <odmax = {!!} } ⊆-zc5 : zc5 ⊆ A - ⊆-zc5 = record { incl = λ lt → proj1 lt } + ⊆-zc5 = record { incl = λ lt → {!!} } IPO = ⊆-IsPartialOrderSet ⊆-zc5 PO - fx>zc : ( z : Ordinal ) → (odef (ZChain.chain zc0) z → * z < * ( f x ) - fx>zc = ? + fx>zc : ( z : Ordinal ) → odef (ZChain.chain zc0) z → * z < * ( f x ) + fx>zc = {!!} cmp : Trichotomous _ _ - cmp record { elm = a ; is-elm = aa } record { elm = b ; is-elm = ab } = ? + 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₁) + ... | case1 c | case2 fx = {!!} + ... | case2 x | case1 x₁ = {!!} + ... | case2 x | case2 x₁ = tri≈ {!!} (subst₂ (λ j k → j ≡ k ) *iso *iso (trans (cong (*) x) (sym (cong (*) x₁ ) ))) {!!} zc6 : IsTotalOrderSet zc5 zc6 = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z} ; compare = cmp } ... | case2 not with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) {!!} {!!} ) )) ... | case1 y = {!!} ... | case2 not = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 - ; chain∋x = {!!} ; is-max = {!!} } -- no extention + ; 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 = ZChain.f-next zc0 - ; chain∋x = {!!} ; is-max = {!!} } where + ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} } where zc0 = prev (& A) a ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b c = {!!}