Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1040:4b525726f2df
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 03 Dec 2022 11:48:47 +0900 |
| parents | 4b22a2ece4e8 |
| children | f12a9b4066a0 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 30 insertions(+), 23 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Dec 03 09:57:13 2022 +0900 +++ b/src/zorn.agda Sat Dec 03 11:48:47 2022 +0900 @@ -353,7 +353,9 @@ chain∋init {x} x≤z = ⟪ ay , ch-init (init ay refl) ⟫ mf : ≤-monotonic-f A f - mf x ax = ? + mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where + mf00 : * x < * (f x) + mf00 = proj1 ( mf< x ax ) f-next : {a z : Ordinal} → odef (UnionCF A f ay supf z) a → odef (UnionCF A f ay supf z) (f a) f-next {a} ⟪ ua , ch-init fc ⟫ = ⟪ proj2 ( mf _ ua) , ch-init (fsuc _ fc) ⟫ @@ -714,7 +716,7 @@ chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b - m05 = ZChain.sup=u zc ab (o<→≤ m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫ -- ZChain on x + m05 = ZChain.sup=u zc ab (o<→≤ m09) ⟪ record { ax = ab ; x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫ -- ZChain on x m10 : odef (UnionCF A f ay supf x) b m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05) ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where @@ -730,7 +732,7 @@ m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b - m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫ + m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫ m14 : ZChain.supf zc b o< x m14 = subst (λ k → k o< x ) (sym m05) b<x m13 : odef (UnionCF A f ay supf x) z @@ -928,6 +930,21 @@ fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc + sfpx<x : supf0 px o< x + sfpx<x with trio< (supf0 px) x + ... | tri< a ¬b ¬c = a + ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where + -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case + m12 : supf0 px ≡ sp1 + m12 with osuc-≡< m13 + ... | case1 eq = eq + ... | case2 lt = ⊥-elim ( o≤> sp≤x (subst (λ k → k o< sp1) spx=x lt )) + m10 : f (supf0 px) ≡ supf0 px + m10 = fc-stop A f mf (ZChain.asupf zc) m11 m12 where + m11 : {z : Ordinal} → FClosure A f (supf0 px) z → (z ≡ sp1) ∨ (z << sp1) + m11 {z} fc = MinSUP.x≤sup sup1 (case2 fc) + ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans m13 sp≤x))) -- x o< supf0 px o≤ sp1 ≤ x + -- this is a kind of maximality, so we cannot prove this without <-monotonicity -- cfcs : {a b w : Ordinal } @@ -1003,8 +1020,7 @@ z53 : odef A w z53 = A∋fc {A} _ f mf fc csupf1 : odef (UnionCF A f ay supf1 b) w - csupf1 with trio< (supf0 px) x - ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) z52 fc1 ⟫ where + csupf1 = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) z52 fc1 ⟫ where spx = supf0 px spx≤px : supf0 px o≤ px spx≤px = zc-b<x _ sfpx<x @@ -1012,17 +1028,6 @@ z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc 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 - ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where - -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case - m12 : supf0 px ≡ sp1 - m12 with osuc-≡< m13 - ... | case1 eq = eq - ... | case2 lt = ⊥-elim ( o≤> sp≤x (subst (λ k → k o< sp1) spx=x lt )) - m10 : f (supf0 px) ≡ supf0 px - m10 = fc-stop A f mf (ZChain.asupf zc) m11 m12 where - m11 : {z : Ordinal} → FClosure A f (supf0 px) z → (z ≡ sp1) ∨ (z << sp1) - m11 {z} fc = MinSUP.x≤sup sup1 (case2 fc) - ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans m13 sp≤x))) -- x o< supf0 px o≤ sp1 ≤ x ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x zc11 : {z : Ordinal} → odef (UnionCF A f ay supf1 x) z → odef pchainpx z @@ -1062,13 +1067,15 @@ → supf1 z o≤ s z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sp1 px<z)) ( MinSUP.minsup sup1 as z25 ) where z25 : {w : Ordinal } → odef pchainpx w → w ≤ s - z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf fc , ch-is-sup (supf0 px) ? ? ? ⟫ where - z27 : supf1 px ≡ px --- sp1 o≤ x - z27 = trans (sf1=sf0 o≤-refl) ( ZChain.sup=u zc ? ? ? ) - z29 : supf0 px o≤ z - z29 = ? -- supf0 px ≡ supf1 px o≤ supf1 x o≤ - z28 : supf0 px o< z - z28 = ? + z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf fc , ch-is-sup (supf0 px) z28 z27 fc1 ⟫ where + z28 : supf0 px o< z -- supf0 px ≡ supf1 px o≤ supf1 x o≤ + z28 = subst (λ k → supf0 px o< k) (sym z=x) sfpx<x + z29 : supf0 px o≤ px + z29 = zc-b<x _ sfpx<x + z27 : supf1 (supf0 px) ≡ supf0 px + z27 = trans (sf1=sf0 z29) ( ZChain.supf-idem zc o≤-refl z29 ) + fc1 : FClosure A f (supf1 (supf0 px)) w + fc1 = subst (λ k → FClosure A f k w) (sym z27) fc z25 {w} (case1 ⟪ ua , ch-init fc ⟫) = sup ⟪ ua , ch-init fc ⟫ z25 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc ⟫) = sup ⟪ ua , ch-is-sup u u<z (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where