Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 732:ddeb107b6f71
bchain can be reached from upwords by f. so it is worng.
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 19 Jul 2022 07:36:10 +0900 |
| parents | ac6b4d200f27 |
| children | 15f3bcc4ae3f |
| files | src/OrdUtil.agda src/zorn.agda |
| diffstat | 2 files changed, 34 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OrdUtil.agda Tue Jul 19 01:15:05 2022 +0900 +++ b/src/OrdUtil.agda Tue Jul 19 07:36:10 2022 +0900 @@ -72,6 +72,11 @@ ... | case1 x=y = subst ( λ k → k o< oz ) (sym x=y) y<z ... | case2 x<y = ordtrans x<y y<z +ordtrans<-≤ : {ox oy oz : Ordinal } → ox o< oy → oy o< osuc oz → ox o< oz +ordtrans<-≤ {ox} {oy} {oz} x<y y≤z with osuc-≡< y≤z +... | case1 x=y = subst ( λ k → ox o< k ) (x=y) x<y +... | case2 y<z = ordtrans x<y y<z + open _∧_ osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
--- a/src/zorn.agda Tue Jul 19 01:15:05 2022 +0900 +++ b/src/zorn.agda Tue Jul 19 07:36:10 2022 +0900 @@ -265,6 +265,7 @@ record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where field u>0 : o∅ o< u -- ¬ ch-init + supf=u : supf u ≡ u au : odef A u ¬u=fx : {x : Ordinal} → ¬ ( u ≡ f x ) asup : (x : Ordinal) → odef A (supf x) @@ -303,7 +304,8 @@ chain : HOD chain = UnionCF A f mf ay supf z field - chain-mono : {z1 : Ordinal} → z1 o≤ z → UnionCF A f mf ay supf z1 ⊆' UnionCF A f mf ay supf z + -- chain-mono : {z1 : Ordinal} → z1 o≤ z → UnionCF A f mf ay supf z1 ⊆' UnionCF A f mf ay supf z + chain<A : {z : Ordinal } → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf (& A) chain⊆A : chain ⊆' A chain∋init : odef chain init initial : {y : Ordinal } → odef chain y → * init ≤ * y @@ -313,7 +315,7 @@ record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where field - b<x→chain : { b : Ordinal } → b o< z → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) b → odef (UnionCF A f mf ay (ZChain.supf zc) z) b + chain≤x : { b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) b → odef (UnionCF A f mf ay (ZChain.supf zc) z) b chain-mono2 : { a b c : Ordinal } → a o≤ b → b o≤ z → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) z) a ) → b o< z → (ab : odef A b) @@ -433,20 +435,24 @@ {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x SZ1 A f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x - zc1 x prev = record { is-max = is-max ; chain-mono2 = ? ; b<x→chain = ? } where - bchain : {b : Ordinal} → b o< x → + zc1 x prev with Oprev-p x + ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 ; chain≤x = bchain } where + -- supf u ≡ u ? + px = Oprev.oprev op + bchain : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b - bchain {b} b<x ⟪ ab , record { u = u ; u<x = u=0 ; uchain = ch-init b fc } ⟫ = - ⟪ ab , record { u = u ; u<x = case2 refl ; uchain = ch-init b fc } ⟫ - bchain {b} b<x ⟪ ab , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } ⟫ = - ⟪ ab , record { u = u ; u<x = case1 (b01 fc) ; uchain = ch-is-sup is-sup fc } ⟫ where - b01 : {b : Ordinal } → FClosure A f (ZChain.supf zc u) b → u o< x - b01 (init as) = ? - b01 (fsuc z fc) = b01 fc + bchain {b} b≤x ⟪ ab , record { u = u0 ; u<x = u<x ; uchain = ch-init .b x } ⟫ = + ⟪ ab , record { u = u0 ; u<x = case2 refl ; uchain = ch-init b x } ⟫ + bchain {b} b≤x ub@record { proj1 = ab ; proj2 = record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } } with osuc-≡< b≤x + ... | case2 lt = ⟪ ab , record { u = UChain.u (proj2 sz00) ; u<x = ? ; uchain = UChain.uchain (proj2 sz00) } ⟫ where + sz00 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b + sz00 = ZChain1.chain≤x (prev px ? ) ? ub + ... | case1 refl = ? + chain-mono2 : {a b c : Ordinal} → a o≤ b → b o≤ x → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c - chain-mono2 {a} {b} {c} a≤b b≤x uac = ? + chain-mono2 {a} {b} {c} a≤b b≤x uac = {!!} is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → b o< x → (ab : odef A b) → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab → @@ -458,19 +464,17 @@ m03 = {!!} m02 : odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) (f (HasPrev.y has-prev)) m02 = ZChain.f-next zc (HasPrev.ay has-prev) - ... | case2 ¬fy<x with Oprev-p x - ... | yes op = {!!} where - px = Oprev.oprev op + ... | case2 ¬fy<x = {!!} where m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b m01 with trio< px b - ... | tri< a ¬b ¬c = ZChain1.chain-mono2 (prev px ?) ? ? m04 where + ... | tri< a ¬b ¬c = ZChain1.chain-mono2 (prev px {!!}) {!!} {!!} m04 where m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b - m04 = ZChain1.is-max (prev px ?) {!!} {!!} ab {!!} a<b + m04 = ZChain1.is-max (prev px {!!}) {!!} {!!} ab {!!} a<b ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b c = {!!} - ... | no lim = ZChain1.chain-mono2 (prev b b<x ) ? {!!} m04 where - m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b - m04 = ZChain1.is-max (prev (osuc b) ? ) {!!} <-osuc ab {!!} a<b + ... | no lim = record { is-max = {!!} ; chain-mono2 = {!!} ; chain≤x = {!!} } + --- m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b + --- m04 = ZChain1.is-max (prev (osuc b) {!!} ) {!!} <-osuc ab {!!} a<b --- --- the maximum chain has fix point of any ≤-monotonic function @@ -537,7 +541,7 @@ inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅ inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy - ; initial = isy ; f-next = inext ; f-total = itotal ; chain-mono = {!!} } where + ; initial = isy ; f-next = inext ; f-total = itotal ; chain<A = {!!} } where isupf : Ordinal → Ordinal isupf z = y cy : odef (UnionCF A f mf ay isupf o∅) y @@ -691,7 +695,7 @@ pcy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay) } ⟫ no-extension : ZChain A f mf ay x - no-extension = record { initial = pinit ; chain∋init = pcy ; supf = psupf0 ; chain-mono = ? + no-extension = record { initial = pinit ; chain∋init = pcy ; supf = psupf0 ; chain<A = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } usup : SUP A pchain @@ -718,13 +722,13 @@ zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x) - ... | no noax = no-extension where -- ¬ A ∋ p, just skip + ... | no noax = no-extension -- ¬ A ∋ p, just skip ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f ) -- 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 { initial = ? ; chain∋init = ? ; supf = psupf1 ; chain-mono = ? - ; chain⊆A = ? ; f-next = ? ; f-total = ? } where -- x is a sup of (zc ?) + ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!} ; supf = psupf1 ; chain<A = {!!} + ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} } where -- x is a sup of (zc ?) psupf1 : Ordinal → Ordinal psupf1 z with trio< z x ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z