Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1068:f24f4de4d459
add 0<supfz
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 13 Dec 2022 02:59:01 +0900 |
| parents | 074b6a506b1b |
| children | 99df080f4fdb |
| files | src/zorn.agda |
| diffstat | 1 files changed, 20 insertions(+), 38 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Dec 13 00:14:32 2022 +0900 +++ b/src/zorn.agda Tue Dec 13 02:59:01 2022 +0900 @@ -350,6 +350,7 @@ supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x + 0<supfz : {x : Ordinal } → o∅ o< supf x is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) @@ -885,7 +886,7 @@ m14 {z} uz = MinSUP.x≤sup sup1 (case1 uz) zc41 : ZChain A f mf< ay x - zc41 = record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order + zc41 = record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order ; 0<supfz = ? ; zo≤sz = zo≤sz ; supfmax = supfmax ; is-minsup = is-minsup ; cfcs = cfcs } where supf1 : Ordinal → Ordinal @@ -1238,14 +1239,14 @@ ... | no lim with trio< x o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) - ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) + ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = ? ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s ) ; zo≤sz = ? ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ? } where mf : ≤-monotonic-f A f mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where mf00 : * x < * (f x) mf00 = proj1 ( mf< x ax ) - ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? + ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = ? ; zo≤sz = ? ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where -- mf : ≤-monotonic-f A f @@ -1320,42 +1321,23 @@ ZChain.supf (pzc (pic<x ia)) (IChain-i ib) ≤⟨ ZChain.supf-mono (pzc (pic<x ia)) (o<→≤ c) ⟩ ZChain.supf (pzc (pic<x ia)) (IChain-i ia) ∎ ) sa<sb ) where open o≤-Reasoning O + IC⊆ : {a b : Ordinal } (ia : IChain ay supfz a ) (ib : IChain ay supfz b ) + → IChain-i ia o≤ IChain-i ib → odef (ZChain.chain (pzc (pic<x ib))) a + IC⊆ {a} {b} (ic-init fc ) ib ia≤ib = ⟪ A∋fc _ f mf fc , ch-init fc ⟫ + IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia≤ib = ⊥-elim ( o≤> ia≤ib ic01 ) where + ic02 : o∅ o< supfz i<x + ic02 = ZChain.0<supfz (pzc (ob<x lim i<x)) + ic01 : o∅ o< i + ic01 = ordtrans<-≤ ic02 sa<x + IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia≤ib + = ZChain.cfcs (pzc (ob<x lim j<x) ) ia≤ib o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) ia≤ib) sb<x) + (subst (λ k → FClosure A f k a) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc)) fc ) + ptotalx : IsTotalOrderSet pchainx - ptotalx {a} {b} ia ib with trio< (ZChain.supf (pzc (pic<x (proj2 ia))) (IChain-i (proj2 ia))) - (ZChain.supf (pzc (pic<x (proj2 ib))) (IChain-i (proj2 ib))) - ... | tri< ia<ib ¬b ¬c = uz01 where - uz01 : Tri (a < b) (a ≡ b) (b < a ) - uz01 with pchainx⊆chain ia - ... | ⟪ ai , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-init fc ⟫ (pchainx⊆chain ib) - ... | ⟪ ai , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-is-sup u uz02 uz03 uz04 ⟫ (pchainx⊆chain ib) where - a<b : IChain-i (proj2 ia) o< IChain-i (proj2 ib) - a<b = ichain-inject {_} {_} {proj2 ia} {proj2 ib} ia<ib - uz02 : u o< osuc (IChain-i (proj2 ib)) - uz02 = ordtrans<-≤ u<x (o<→≤ (osucc a<b)) - uz03 : ZChain.supf (pzc (pic<x (proj2 ib))) u ≡ u - uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) )) su=u - uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a) - uz04 = subst (λ k → FClosure A f k (& a)) ( zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ u<x) ) fc - ... | tri≈ ¬a ia=ib ¬c = ? where - uz01 : Tri (* (& a ) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a )) - uz01 with proj2 ia | proj2 ib - ... | ic-init fca | ic-init fcb = fcn-cmp y f mf fca fcb - ... | ic-isup ia ia<x sa<x fca | ic-init fcb = ? - ... | ic-init fca | ic-isup ib ib<x sb<x fcb = ? - ... | ic-isup ia ia<x sa<x fca | ic-isup ib ib<x sb<x fcb = fcn-cmp ? f mf ? ? - ... | tri> ¬a ¬b ib<ia = uz01 where - uz01 : Tri (a < b) (a ≡ b) (b < a ) - uz01 with pchainx⊆chain ib - ... | ⟪ bi , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) ⟪ bi , ch-init fc ⟫ - ... | ⟪ bi , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) ⟪ bi , ch-is-sup u uz02 uz03 uz04 ⟫ where - b<a : IChain-i (proj2 ib) o< IChain-i (proj2 ia) - b<a = ichain-inject {_} {_} {proj2 ib} {proj2 ia} ib<ia - uz02 : u o< osuc (IChain-i (proj2 ia)) - uz02 = ordtrans<-≤ u<x (o<→≤ (osucc b<a)) - uz03 : ZChain.supf (pzc (pic<x (proj2 ia))) u ≡ u - uz03 = trans (sym ( zeq _ _ (o<→≤ (osucc b<a)) (o<→≤ u<x) )) su=u - uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ia))) u) (& b) - uz04 = subst (λ k → FClosure A f k (& b)) ( zeq _ _ (o<→≤ (osucc b<a)) (o<→≤ u<x) ) fc + ptotalx {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib)) + ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainx⊆chain ib) + ... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainx⊆chain ib) + ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainx⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) (o<→≤ ib<ia)) usup : MinSUP A pchainx usup = minsupP pchainx (λ ic → ? ) ptotalx