Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1012:6f6daf464616
maxα
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 23 Nov 2022 09:55:38 +0900 |
| parents | 66154af40f89 |
| children | 2362c2d89d36 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 48 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Nov 20 17:44:21 2022 +0900 +++ b/src/zorn.agda Wed Nov 23 09:55:38 2022 +0900 @@ -1085,16 +1085,23 @@ -- this is a kind of maximality, so we cannot prove this without <-monotonicity -- - -- supf0 a ≡ px we cannot use previous cfcs, it is in the chain because - -- supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x - -- cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } → a o< b → b o≤ x → supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w - cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with trio< a px + cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with zc43 (supf0 a) px + ... | case2 px≤sa = z50 where + a≤px : a o≤ px + a≤px = subst (λ k → a o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x) + -- supf0 a ≡ px we cannot use previous cfcs, it is in the chain because + -- supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x + z50 : odef (UnionCF A f mf ay supf1 b) w + z50 with osuc-≡< px≤sa + ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) ? ? (subst (λ k → FClosure A f k w) ? fc) ⟫ + ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) sa<x ⟫ ) + ... | case1 sa<px with trio< a px ... | tri< a<px ¬b ¬c = z50 where z50 : odef (UnionCF A f mf ay supf1 b) w z50 with osuc-≡< b≤x - ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) ? fc + ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<px fc ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ ... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc u≤px ) ⟫ where -- u o< px → u o< b ? u≤px : u o≤ px @@ -1108,7 +1115,7 @@ (sym (sf=eq u<x)) s<u) (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc )) ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup) } - z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl ? fc + z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl sa<px fc ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc (o<→≤ u<px)) ⟫ where -- u o< px → u o< b ? u<b : u o< b @@ -1142,14 +1149,25 @@ spx≤px : supf0 px o≤ px spx≤px = zc-b<x _ sfpx<x z52 : supf1 (supf0 px) ≡ supf0 px - z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc mf< o≤-refl ? ) + z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc mf< o≤-refl (zc-b<x _ sfpx<x ) ) fc1 : FClosure A f (supf1 spx) w fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx) order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) ) (MinSUP.x≤sup (ZChain.minsup zc spx≤px) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) - spx≤px ? (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) + spx≤px ss<px (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where + ss<px : supf0 s o< px + ss<px = osucprev ( begin + osuc (supf0 s) ≡⟨ cong osuc (sym (sf1=sf0 ( begin + s <⟨ supf-inject0 supf1-mono ss<spx ⟩ + supf0 px ≤⟨ spx≤px ⟩ + px ∎ ) )) ⟩ + osuc (supf1 s) ≤⟨ osucc ss<spx ⟩ + supf1 spx ≡⟨ sf1=sf0 spx≤px ⟩ + supf0 spx ≤⟨ ZChain.supf-mono zc spx≤px ⟩ + supf0 px ≤⟨ spx≤px ⟩ + px ∎ ) where open o≤-Reasoning O cp1 : ChainP A f mf ay supf1 spx cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 spx≤px )) ( ZChain.fcy<sup zc spx≤px fc ) @@ -1318,6 +1336,9 @@ zc00 : {z : Ordinal } → IChain A f supfz z → z o< & A zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) ) + aic : {z : Ordinal } → IChain A f supfz z → odef A z + aic {z} ic = ? + zeq : {xa xb z : Ordinal } → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa → ZChain.supf (pzc xa<x) z ≡ ZChain.supf (pzc xb<x) z @@ -1388,15 +1409,26 @@ ... | tri> ¬a ¬b c = ? zc5 : ZChain A f mf ay x - zc5 with zc43 x spu - zc5 | (case2 sp≤x ) = ? where - cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } + zc5 = ? where + cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } → a o< b → b o≤ x → supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w - cfcs mf< {a} {b} {w} a<b b≤x sa<x fc = ? - zc5 | (case1 x<sp ) = ? where - cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } - → a o< b → b o≤ x → supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w - cfcs mf< {a} {b} {w} a<b b≤x sa<x fc = ? + cfcs mf< {a} {b} {w} a<b b≤x sa<x fc with trio< a x + ... | tri< a<x ¬b ¬c = ? where + sa = ZChain.supf (pzc (ob<x lim a<x)) a + m = omax a sa + m<x : m o< x + m<x with trio< a sa | inspect (omax a) sa + ... | tri< a<sa ¬b ¬c | record { eq = eq } = ob<x lim sa<x + ... | tri≈ ¬a b ¬c | record { eq = eq } = subst ( λ k → k o< x ) ( begin + sa ≡⟨ ? ⟩ + ? ≡⟨ sym eq ⟩ + _ ∎ ) ( ob<x lim sa<x ) where open ≡-Reasoning + ... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x + zc40 : odef (UnionCF A f mf ay supf1 b) w + zc40 with ZChain.cfcs (pzc (ob<x lim sa<x)) mf< ? o≤-refl ? ? + ... | t = ? + ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) + ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) --- --- the maximum chain has fix point of any ≤-monotonic function