Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1020:eee019e64bea
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 25 Nov 2022 08:57:28 +0900 |
| parents | eb2d0fb19b67 |
| children | 1407fed90475 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 40 insertions(+), 21 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Nov 24 12:30:41 2022 +0900 +++ b/src/zorn.agda Fri Nov 25 08:57:28 2022 +0900 @@ -1120,8 +1120,14 @@ -- 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)) ? ⟫ ) + ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 ? (subst (λ k → FClosure A f k w) z52 fc) ⟫ where + z51 : supf0 px o< b + z51 = ? + z52 : supf1 a ≡ supf1 (supf0 px) + z52 = ? + ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) z53 ⟫ ) where + z53 : supf1 a o< x + z53 = ordtrans<-≤ sa<b b≤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 @@ -1182,10 +1188,8 @@ (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 ss0<spx (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where - ss0<spx : supf0 s o< spx - ss0<spx = ? - ss<px : supf0 s o< px - ss<px = osucprev ( begin + ss0<spx : supf0 s o< spx + ss0<spx = osucprev ( begin osuc (supf0 s) ≡⟨ cong osuc (sym (sf1=sf0 ( begin s <⟨ supf-inject0 supf1-mono ss<spx ⟩ supf0 px ≤⟨ spx≤px ⟩ @@ -1193,8 +1197,7 @@ 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 + supf0 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 ) @@ -1283,12 +1286,24 @@ cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } → a o< b → b o≤ x → supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f mf ay supf0 b) w cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with trio< b px - ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) ? fc - ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl ? fc - ... | tri> ¬a ¬b px<b with trio< a px - ... | tri< a ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) ( ZChain.cfcs zc mf< a o≤-refl ? fc ) - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ? c ) - ... | tri≈ ¬a refl ¬c = ? -- supf0 px o< x → odef (UnionCF A f mf ay supf0 x) (supf0 px) + ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) sa<b fc + ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl sa<b fc + ... | tri> ¬a ¬b px<b = ? where + x=b : x ≡ b + x=b = ? + -- a o< x, supf a o< x + -- a o< px , supf a o< px → odef U w + -- a ≡ px -- supf0 px o< x → odef U w + -- -- x o≤ supf0 px o< x → ⊥ + -- supf a ≡ px -- a o< px → odef U w + -- a ≡ px → supf px ≡ px → odef U w + + cfcs1 : odef (UnionCF A f mf ay supf0 b) w + cfcs1 with trio< a px + ... | tri< a<px ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) + ( ZChain.cfcs zc mf< a<px o≤-refl ? fc ) + ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ? c ) + ... | tri≈ ¬a refl ¬c = ? -- supf0 px o< x → odef (UnionCF A f mf ay supf0 x) (supf0 px) -- x o≤ supf0 px o≤ sp → zc17 : {z : Ordinal } → supf0 z o≤ supf0 px @@ -1441,10 +1456,10 @@ ... | case1 b=x with trio< a x ... | tri< a<x ¬b ¬c = zc40 where sa = ZChain.supf (pzc (ob<x lim a<x)) a - m = omax a sa + m = omax a sa -- x is limit ordinal, so we have sa o< m o< x 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 ? + ... | tri< a<sa ¬b ¬c | record { eq = eq } = ob<x lim (ordtrans<-≤ sa<b b≤x ) ... | tri≈ ¬a a=sa ¬c | record { eq = eq } = subst (λ k → k o< x) eq zc41 where zc41 : omax a sa o< x zc41 = osucprev ( begin @@ -1468,7 +1483,7 @@ ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<b ? fc2 ⟫ where -- u o< px → u o< b ? zc55 : u o< osuc m zc55 = u<x - u<b : u o< b -- b o≤ u → b o≤ a -- u ≡ supf1 a + u<b : u o< b u<b = subst (λ k → u o< k ) (sym b=x) ( ordtrans u<x (ob<x lim m<x)) fc1m : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) u) w fc1m = fc1 @@ -1482,15 +1497,19 @@ ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x)) cfcs mf< {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where supfb = ZChain.supf (pzc (ob<x lim b<x)) + sb=sa : {a : Ordinal } → a o< b → supf1 a ≡ ZChain.supf (pzc (ob<x lim b<x)) a + sb=sa {a} a<b = trans (sf1=sf (ordtrans<-≤ a<b b≤x)) (zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ <-osuc) ) fcb : FClosure A f (supfb a) w - fcb = ? - -- supfb a o≤ supfb b + fcb = subst (λ k → FClosure A f k w) (sb=sa a<b) fc + -- supfb a o< b assures it is in Union b zcb : odef (UnionCF A f mf ay supfb b) w - zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) ? fcb + zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb zc40 : odef (UnionCF A f mf ay supf1 b) w zc40 with zcb ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<x ? ? ⟫ + ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<x cp (subst (λ k → FClosure A f k w) (sym (sb=sa u<x)) fc1 ) ⟫ where + cp : ChainP A f mf ay supf1 u + cp = ? --- --- the maximum chain has fix point of any ≤-monotonic function