Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1082:83d9000bf72f
0< is no good
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 17 Dec 2022 12:58:17 +0900 |
| parents | 7089a047e49f |
| children | 424af168622f |
| files | src/zorn.agda |
| diffstat | 1 files changed, 38 insertions(+), 30 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Dec 17 06:07:18 2022 +0900 +++ b/src/zorn.agda Sat Dec 17 12:58:17 2022 +0900 @@ -1238,7 +1238,7 @@ ... | no lim with trio< x o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) - ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = 0<supfz + ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = 0<supfz (ysup f mf ay) ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s ) ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = λ a<b b≤0 → ⊥-elim ( ¬x<0 (subst (λ k → _ o< k ) x=0 (ordtrans<-≤ a<b b≤0))) } where mf : ≤-monotonic-f A f @@ -1246,16 +1246,16 @@ mf00 : * x < * (f x) mf00 = proj1 ( mf< x ax ) ym = MinSUP.sup (ysup f mf ay) - 0<supfz : o∅ o< MinSUP.sup (ysup f mf ay) - 0<supfz with trio< o∅ (MinSUP.sup (ysup f mf ay) ) + 0<supfz : (ysup : MinSUP A (uchain f mf ay)) → o∅ o< MinSUP.sup ysup + 0<supfz ysup with trio< o∅ (MinSUP.sup ysup ) ... | tri< a ¬b ¬c = a - ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ ? (MinSUP.minsup (ysup f mf ay) (proj2 (mf _ (MinSUP.as (ysup f mf ay) ))) mf01 )) where - mf01 : {w : Ordinal} → odef (uchain f mf ay) w → w ≤ f (MinSUP.sup (ysup f mf ay)) - mf01 {w} uw = ≤-ftrans (MinSUP.x≤sup (ysup f mf ay) uw) (proj1 (mf _ (MinSUP.as (ysup f mf ay) ))) + ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ ? (MinSUP.minsup ysup (proj2 (mf _ (MinSUP.as ysup ))) mf01 )) where + mf01 : {w : Ordinal} → odef (uchain f mf ay) w → w ≤ f (MinSUP.sup ysup ) + mf01 {w} uw = ≤-ftrans (MinSUP.x≤sup ysup uw) (proj1 (mf _ (MinSUP.as ysup ))) ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) zo≤sz : {z : Ordinal} → z o≤ x → z o≤ MinSUP.sup (ysup f mf ay) zo≤sz {z} z≤x with osuc-≡< z≤x - ... | case1 refl = o<→≤ (subst (λ k → k o< MinSUP.sup (ysup f mf ay)) (sym x=0) 0<supfz ) + ... | case1 refl = o<→≤ (subst (λ k → k o< MinSUP.sup (ysup f mf ay)) (sym x=0) (0<supfz (ysup f mf ay) ) ) ... | case2 lt = ⊥-elim ( ¬x<0 (subst (λ k → z o< k ) x=0 lt ) ) is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay (λ _ → MinSUP.sup (ysup f mf ay)) z) (MinSUP.sup (ysup f mf ay)) @@ -1598,18 +1598,18 @@ zc44 : FClosure A f (supf1 u) w zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc - zo≤sz : {z : Ordinal} → z o≤ x → z o≤ supf1 z zo≤sz {z} z≤x with osuc-≡< z≤x ... | case2 z<x = subst (λ k → z o≤ k) (sym (trans (sf1=sf z<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl)))) ( ZChain.zo≤sz (pzc z<x) o≤-refl ) - ... | case1 refl = ? where -- subst (λ k → x o≤ k) (sf1=spu refl) ? where + ... | case1 refl = subst (λ k → x o≤ k) (sym (sf1=spu refl)) z47 where z47 : x o≤ spu z47 with x<y∨y≤x spu x ... | case2 lt = lt ... | case1 spu<x = ⊥-elim ( <<-irr (MinSUP.x≤sup usup z48) (proj1 ( mf< spu (MinSUP.as usup)))) where z49 : supfz spu<x ≡ spu z49 with trio< (supfz spu<x) spu - ... | tri< a ¬b ¬c = ⊥-elim ( o≤> ( IsMinSUP.minsup (is-minsup (o<→≤ spu<x)) (MinSUP.as usup) z51 ) ? ) where + ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( IsMinSUP.minsup (is-minsup (o<→≤ spu<x)) (MinSUP.as usup) z51 ) + (subst₂ (λ j k → j o< k ) refl (trans (zeq _ _ o≤-refl (o<→≤ <-osuc)) (sym (sf1=sf spu<x))) c)) where z51 : {w : Ordinal } → odef (UnionCF A f ay supf1 spu) w → w ≤ spu z51 {w} ⟪ aw , ch-init fc ⟫ = MinSUP.x≤sup usup ⟪ aw , ic-init fc ⟫ z51 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = MinSUP.x≤sup usup ⟪ aw , ic-isup u (ordtrans u<b spu<x) z55 z56 ⟫ where @@ -1622,29 +1622,37 @@ z56 : FClosure A f (supfz (ordtrans u<b spu<x)) w z56 = subst (λ k → FClosure A f k w ) (sym (trans (zeq _ _ o≤-refl (o<→≤ <-osuc) ) (sym (sf1=sf u<z)))) fc ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( MinSUP.minsup usup (ZChain.asupf (pzc (ob<x lim spu<x))) z52 ) ? ) where + ... | tri< a ¬b ¬c = ⊥-elim ( o≤> ( MinSUP.minsup usup (ZChain.asupf (pzc (ob<x lim spu<x))) z52 ) + (subst₂ (λ j k → j o< k) (zeq _ _ o≤-refl (o<→≤ <-osuc)) refl a)) where z52 : {w : Ordinal } → odef pchainU w → w ≤ supfz spu<x - z52 {w} uw = subst (λ k → w ≤ k ) (sf1=sf spu<x) ( IsMinSUP.x≤sup (is-minsup (o<→≤ spu<x)) z53 ) where + z52 {w} ⟪ aw , ic-init fc ⟫ = subst (λ k → w ≤ k ) (sf1=sf spu<x) ( IsMinSUP.x≤sup (is-minsup (o<→≤ spu<x)) ⟪ aw , ch-init fc ⟫ ) + z52 {w} ⟪ aw , ic-isup u u<b sa<b fc ⟫ = subst (λ k → w ≤ k ) (sf1=sf spu<x) ( IsMinSUP.x≤sup (is-minsup (o<→≤ spu<x)) z53 ) where + -- sa<b : supfz u<b o≤ u + -- a : supfz spu<x o< spu + z60 : odef (UnionCF A f ay (ZChain.supf (pzc (ob<x lim u<b))) (osuc u)) w + z60 = ZChain.cfcs (pzc (ob<x lim u<b)) <-osuc o≤-refl sa<b fc z53 : odef (UnionCF A f ay supf1 spu) w - z53 with pchainU⊆chain uw - ... | ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ - ... | ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<spu - (trans (trans (sf1=sf u<z) (zeq _ _ z54 (o<→≤ <-osuc))) su=u ) - (subst (λ k → FClosure A f k w) (sym (trans (sf1=sf u<z) (zeq _ _ z54 (o<→≤ <-osuc)))) fc) ⟫ where - u<spu : u o< spu - u<spu = ? -- ordtrans u<b (pic<x (proj2 uw)) - u<z : u o< z - u<z = ordtrans u<spu spu<x - z54 : osuc u o≤ osuc (IChain-i (proj2 uw)) - z54 = osucc u<b - -- u<b : u o< osuc (IChain-i (proj2 uw)) - z50 : supfz spu<x o≤ x - z50 = ? -- o<→≤ ( subst (λ k → k o< x) z49 ?) -- spu<x ) + z53 with z60 + ... | ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ + ... | ⟪ aw , ch-is-sup u u<z su=u fc ⟫ = ⟪ aw , ch-is-sup u z54 z55 z56 ⟫ where + z54 : u o< spu + z54 = osucprev ( begin + osuc u ≡⟨ cong osuc (sym su=u) ⟩ + osuc (ZChain.supf (pzc (ob<x lim u<b)) u ) ≤⟨ ? ⟩ + supfz spu<x <⟨ a ⟩ + spu ∎ ) where open o≤-Reasoning O + z57 : supf1 u ≡ ZChain.supf (pzc (ob<x lim u<b)) u + z57 = trans (sf1=sf ?) (zeq _ _ ? ? ) + z55 : supf1 u ≡ u + z55 = trans z57 su=u + z56 : FClosure A f (supf1 u) w + z56 = subst (λ k → FClosure A f k w) (sym z57) fc + z50 : supfz spu<x o≤ spu + z50 = o≤-refl0 z49 z48 : odef pchainU (f spu) - z48 = ⟪ proj2 (mf _ (MinSUP.as usup) ) , ic-isup _ (subst (λ k → k o< x) refl spu<x) ? -- z50 + z48 = ⟪ proj2 (mf _ (MinSUP.as usup) ) , ic-isup _ (subst (λ k → k o< x) refl spu<x) z50 (fsuc _ (init (ZChain.asupf (pzc (ob<x lim spu<x))) z49)) ⟫ - supfeq1 : {a b : Ordinal } → a o≤ x → b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b) ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> ( @@ -1681,8 +1689,8 @@ a<b = supf-inject0 supf-mono sa<sb a<x : a o< x a<x = ordtrans<-≤ a<b b≤x - ... | case1 refl = ? where -- zc40 (subst₂ (λ j k → j o< k) (sf1=sf a<x) (sf1=spu refl) sa<sb) - -- (subst (λ k → FClosure A f k w) (sf1=sf a<x) fc ) where + ... | case1 refl = subst (λ k → w ≤ k ) (sym (sf1=spu refl)) ( zc40 (subst₂ (λ j k → j o< k) (sf1=sf a<x) (sf1=spu refl) sa<sb) + (subst (λ k → FClosure A f k w) (sf1=sf a<x) fc )) where a<x : a o< x a<x = supf-inject0 supf-mono sa<sb zc40 : ZChain.supf (pzc (ob<x lim a<x )) a o< spu → FClosure A f (ZChain.supf (pzc (ob<x lim a<x )) a) w → w ≤ spu