Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 980:49cf50d451e1
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 09 Nov 2022 11:10:11 +0900 |
| parents | 6229017a6176 |
| children | 6b67e43733ca |
| files | src/zorn.agda |
| diffstat | 1 files changed, 33 insertions(+), 48 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Nov 09 05:00:56 2022 +0900 +++ b/src/zorn.agda Wed Nov 09 11:10:11 2022 +0900 @@ -1178,60 +1178,45 @@ UChain⊆ A f mf {x} {y} ay {supf0} {supf1} (ZChain.supf-mono zc) sf=eq sf≤ (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) (ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px)))) - -- px o< z1 , px o≤ supf1 z1 --> px o≤ sp1 o< x -- sp1 ≡ px--> odef (UnionCF A f mf ay supf1 x) sp1 - -- supf1 px ≡ sp1 o< supf1 x + -- px o< z1 , supf1 z1 o< x -> sp1 o≤ z1 -- sp1 o≤ supf1 x + -- px o≤ supf1 z1 , supf1 z1 o< x -> supf1 z1 ≡ px --> z1 o≤ px → supf0 z1 ≡ px + --> px o< x1 → sp1 ≡ px csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) csupf1 {z1} sz1<x = csupf2 where - -- z1 o< px → supf1 z1 ≡ supf0 z1 - -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1 - -- z1 ≡ px , supf0 px ≡ px psz1≤px : supf1 z1 o≤ px psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) - csupf2 with 3cases - ... | case2 (case2 p) with trio< z1 px | inspect supf1 z1 - ... | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px - ... | case2 lt = zc12 (proj1 p) (proj2 p) (case1 cs03) where - cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) - cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) - ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) - ... | case1 sfz=sfpx = zc12 (proj1 p) (proj2 p) (case2 (init (ZChain.asupf zc) cs04 )) where - cs04 : supf0 px ≡ supf0 z1 - cs04 = begin - supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ - supf1 px ≡⟨ sym sfz=sfpx ⟩ - supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩ - supf0 z1 ∎ where open ≡-Reasoning - ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫ ) where - --- supf1 z1 ≡ px , z1 o< px , px ≡ supf0 z1 o< supf0 px o< x - cs05 : px o< supf0 px - cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx - cs06 : supf0 px o< osuc px - cs06 = subst₂ (λ j k → j o< k ) (sym (proj1 p)) (sym opx=x) px<x - csupf2 | case2 (case2 p) | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (proj1 p) (proj2 p) - (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) - csupf2 | case2 (case2 p) | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ⊥-elim ( ¬p<x<op ⟪ cs08 , cs09 ⟫ ) where - cs08 : px o< sp1 - cs08 = subst (λ k → k o< sp1 ) (proj1 p) (proj2 p ) - cs09 : sp1 o< osuc px - cs09 = subst ( λ k → sp1 o< k ) (sym (Oprev.oprev=x op)) sz1<x - csupf2 | case2 (case1 p) with trio< (supf0 px) sp1 -- ¬ (supf0 px o< sp1 -- sp1 o≤ supf px) - ... | tri< a ¬b ¬c = ⊥-elim (p a) - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> sfpx≤sp1 c ) - csupf2 | case1 p with trio< (supf0 px) px -- ¬ (supf0 px ≡ px ) - ... | tri< sf0px<px ¬b ¬c = ? where - cs10 : odef (UnionCF A f mf ay supf0 px) (supf0 px) - cs10 = ZChain.csupf zc sf0px<px - ... | tri≈ ¬a b ¬c = ⊥-elim (p b) - ... | tri> ¬a ¬b px<sf0px = ? where - cs11 : px o< z1 → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - cs11 px<z1 = ⊥-elim ( ¬p<x<op ⟪ px<sf0px , subst₂ (λ j k → j o< k ) refl (sym (Oprev.oprev=x op)) - (ordtrans≤-< (subst (λ k → supf0 px o< k) (cong osuc (sym (sf1=sp1 px<z1 ))) sfpx≤sp1 ) sz1<x) ⟫ ) - cs12 : z1 o≤ px → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - cs12 = ? - + csupf2 with osuc-≡< psz1≤px + ... | case2 lt with trio< z1 px | inspect supf1 z1 + ... | tri< a ¬b ¬c | record { eq = eq } = + subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) eq ( csupf0 (subst (λ k → k o< px) (sym eq) lt) (o<→≤ a )) + ... | tri≈ ¬a b ¬c | record { eq = eq } = + subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) eq ( csupf0 (subst (λ k → k o< px) (sym eq) lt) (o≤-refl0 b )) + ... | tri> ¬a ¬b px<z1 | record { eq = eq } = ⟪ MinSUP.asm sup1 , ch-is-sup sp1 cs00 ? (init asupf1 ssp1=sp1 ) ⟫ where + ssp1=sp1 : supf1 sp1 ≡ sp1 + ssp1=sp1 = ? + cs00 : supf1 sp1 o≤ supf1 x + cs00 = ? + csupf2 | case1 psz1=px with trio< z1 px | inspect supf1 z1 + ... | tri< a ¬b ¬c | record { eq = eq } = ⟪ ZChain.asupf zc , ch-is-sup px cs00 ? (init asupf1 cs01 ) ⟫ where + -- spuf1 z1 == px o< x , z1 o< px, + cs03 : supf0 z1 o< px + cs03 = ? + cs02 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) + cs02 = ZChain.csupf zc cs03 + cs01 : supf1 px ≡ supf0 z1 + cs01 = ? + cs00 : supf1 px o≤ supf1 x + cs00 = supf1-mono (o<→≤ px<x) + ... | tri≈ ¬a b ¬c | record { eq = eq } = ⟪ ZChain.asupf zc , ch-is-sup px cs00 ? (init asupf1 cs01 ) ⟫ where + cs01 : supf1 px ≡ supf0 z1 + cs01 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b) ) + cs00 : supf1 px o≤ supf1 x + cs00 = supf1-mono (o<→≤ px<x) + ... | tri> ¬a ¬b c | record { eq = eq } = ⟪ MinSUP.asm sup1 , ch-is-sup x o≤-refl ? (init asupf1 cs01 ) ⟫ where + cs01 : supf1 x ≡ sp1 + cs01 = sf1=sp1 px<x zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where