Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1043:fd26e0c4e648
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 04 Dec 2022 10:30:24 +0900 |
| parents | 912ca4abe806 |
| children | d7ffe919d463 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 23 insertions(+), 38 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Dec 04 09:15:12 2022 +0900 +++ b/src/zorn.agda Sun Dec 04 10:30:24 2022 +0900 @@ -810,13 +810,13 @@ pchainpx : HOD pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain ay px z ) - ∨ FClosure A f (supf0 px) z } ; odmax = & A ; <odmax = zc00 } where - zc00 : {z : Ordinal } → (odef A z ∧ UChain ay px z ) ∨ FClosure A f (supf0 px) z → z o< & A + ∨ (FClosure A f (supf0 px) z ∧ (supf0 px o< x)) } ; odmax = & A ; <odmax = zc00 } where + zc00 : {z : Ordinal } → (odef A z ∧ UChain ay px z ) ∨ (FClosure A f (supf0 px) z ∧ (supf0 px o< x) )→ z o< & A zc00 {z} (case1 lt) = z07 lt - zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc ) + zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf (proj1 fc) ) - zc02 : { a b : Ordinal } → odef A a ∧ UChain ay px a → FClosure A f (supf0 px) b → a ≤ b - zc02 {a} {b} ca fb = zc05 fb where + zc02 : { a b : Ordinal } → odef A a ∧ UChain ay px a → FClosure A f (supf0 px) b ∧ ( supf0 px o< x) → a ≤ b + zc02 {a} {b} ca fb = zc05 (proj1 fb) where zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a ≤ b zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb )) ... | case1 eq = subst (λ k → a ≤ k ) eq (zc05 fb) @@ -839,11 +839,11 @@ ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1 where lt1 : a0 < b0 lt1 = subst₂ (λ j k → j < k ) *iso *iso lt - ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp (supf0 px) f mf a b) + ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp (supf0 px) f mf (proj1 a) (proj1 b)) pcha : pchainpx ⊆' A pcha (case1 lt) = proj1 lt - pcha (case2 fc) = A∋fc _ f mf fc + pcha (case2 fc) = A∋fc _ f mf (proj1 fc) sup1 : MinSUP A pchainpx sup1 = minsupP pchainpx pcha ptotal @@ -853,14 +853,14 @@ -- supf0 px o≤ sp1 -- - sfpx≤sp1 : supf0 px ≤ sp1 - sfpx≤sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl )) + sfpx≤sp1 : supf0 px o< x → supf0 px ≤ sp1 + sfpx≤sp1 spx<x = MinSUP.x≤sup sup1 (case2 ⟪ init (ZChain.asupf zc {px}) refl , spx<x ⟫ ) - m13 : supf0 px o≤ sp1 - m13 = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where + m13 : supf0 px o< x → supf0 px o≤ sp1 + m13 spx<x = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1) - m14 {z} ⟪ as , ch-init fc ⟫ = ≤-ftrans (ZChain.fcy<sup zc o≤-refl fc) sfpx≤sp1 - m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ≤-ftrans (ZChain.order zc o≤-refl u<x fc) sfpx≤sp1 + m14 {z} ⟪ as , ch-init fc ⟫ = ≤-ftrans (ZChain.fcy<sup zc o≤-refl fc) (sfpx≤sp1 ?) + m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ≤-ftrans (ZChain.order zc o≤-refl u<x fc) (sfpx≤sp1 spx<x ) zc41 : ZChain A f mf< ay x zc41 = record { supf = supf1 ; sup=u = sup=u ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order @@ -929,21 +929,6 @@ 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 : sp1 o≤ x → supf0 px o< x - sfpx<x sp1≤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≤> sp1≤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 sp1≤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 } @@ -1040,15 +1025,15 @@ zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | case1 ⟪ ua1 , ch-is-sup u u<x su=u fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x su=u (fsuc _ fc₁) ⟫ - ... | case2 fc = case2 (fsuc _ fc) + ... | case2 fc = case2 ⟪ fsuc _ (proj1 fc) , proj2 fc ⟫ zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) ... | tri< a ¬b ¬c = case1 ⟪ asp , ch-is-sup u u<px (trans (sym (sf1=sf0 (o<→≤ u<px))) su=u )(init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where u<px : u o< px u<px = ZChain.supf-inject zc a asp0 : odef A (supf0 u) asp0 = ZChain.asupf zc - ... | tri≈ ¬a b ¬c = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) - (sym (trans (sf1=sf0 (zc-b<x _ u<x)) b ))) + ... | tri≈ ¬a b ¬c = case2 ⟪ (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) + (sym (trans (sf1=sf0 (zc-b<x _ u<x)) b ))) , ? ⟫ ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z) @@ -1059,7 +1044,7 @@ zc22 : odef A (supf1 z) zc22 = subst (λ k → odef A k ) (sym (sf1=sp1 px<z )) ( MinSUP.as sup1 ) z26 : supf1 px ≤ supf1 x - z26 = subst₂ (λ j k → j ≤ k ) (sym (sf1=sf0 o≤-refl )) (sym (sf1=sp1 px<x )) sfpx≤sp1 + z26 = subst₂ (λ j k → j ≤ k ) (sym (sf1=sf0 o≤-refl )) (sym (sf1=sp1 px<x )) (sfpx≤sp1 ?) z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z z23 {w} uz with zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz ) ... | case1 uz = ≤-ftrans z25 (subst₂ (λ j k → j ≤ supf1 k) (sf1=sf0 o≤-refl) (sym z=x) z26 ) where @@ -1070,16 +1055,16 @@ → 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) z28 z27 fc1 ⟫ where + z25 {w} (case2 fc) = sup ⟪ A∋fc _ f mf (proj1 fc) , ch-is-sup (supf0 px) z28 z27 fc1 ⟫ where -- z=x , supf0 px o< x z28 : supf0 px o< z -- supf0 px ≡ supf1 px o≤ supf1 x ≡ sp1 o≤ x ≡ z - z28 = subst (λ k → supf0 px o< k) (sym z=x) (sfpx<x ?) + z28 = subst (λ k → supf0 px o< k) (sym z=x) ? z29 : supf0 px o≤ px - z29 = zc-b<x _ (sfpx<x ?) + z29 = zc-b<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 + fc1 = subst (λ k → FClosure A f k w) (sym z27) (proj1 fc) -- x o≤ supf0 px o≤ supf0 z ≡ supf0 x ≡ sp1 -- x o≤ supf0 px o≤ supf0 x ≡ sp1 -- fc : FClosure A f (supf0 px) w -- ¬ ( supf0 px o< x ) → ¬ odef ( UnionCF A f ay supf1 z ) w @@ -1117,8 +1102,8 @@ ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b (fcup fc (o<→≤ (ordtrans a<b b<px) )) ... | tri≈ ¬a b=px ¬c = ZChain.order zc (o≤-refl0 b=px) a<b (fcup fc (o<→≤ (subst (λ k → a o< k) b=px a<b ))) ... | tri> ¬a ¬b px<b with trio< a px - ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px fc) sfpx≤sp1 -- supf1 a ≡ supf0 a - ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (case2 (subst (λ k → FClosure A f (supf0 k) w) a=px fc )) + ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px fc) (sfpx≤sp1 ? ) -- supf1 a ≡ supf0 a + ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (case2 ⟪ (subst (λ k → FClosure A f (supf0 k) w) a=px fc ) , ? ⟫ ) ... | tri> ¬a ¬b px<a = ⊥-elim (¬p<x<op ⟪ px<a , zc22 ⟫ ) where -- supf1 a ≡ sp1 zc22 : a o< osuc px zc22 = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)