Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1083:424af168622f
done?
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 17 Dec 2022 21:20:49 +0900 |
| parents | 83d9000bf72f |
| children | 7ec55b1bdfc2 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 65 insertions(+), 69 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Dec 17 12:58:17 2022 +0900 +++ b/src/zorn.agda Sat Dec 17 21:20:49 2022 +0900 @@ -349,7 +349,6 @@ asupf : {x : Ordinal } → odef A (supf x) supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x - 0<supfz : {x : Ordinal } → o∅ o< supf x is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x) @@ -896,7 +895,6 @@ zc41 : ZChain A f mf< ay x zc41 = record { supf = supf1 ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order - ; 0<supfz = 0<supfz ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = cfcs } where supf1 : Ordinal → Ordinal @@ -949,9 +947,6 @@ zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.as sup1) zc24 ) ... | tri> ¬a ¬b c = o≤-refl - 0<supfz : {x : Ordinal } → o∅ o< supf1 x - 0<supfz = ordtrans<-≤ (ZChain.0<supfz zc) (OrdTrans (o≤-refl0 (sym (sf1=sf0 o∅≤z))) (supf1-mono o∅≤z)) - fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z @@ -1238,7 +1233,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 (ysup f mf ay) + ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (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,17 +1241,12 @@ mf00 : * x < * (f x) mf00 = proj1 ( mf< x ax ) ym = 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 (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 (ysup f mf ay) ) ) + ... | case1 refl = subst (λ k → k o≤ _) (sym x=0) o∅≤z ... | 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)) is-minsup {z} z≤x with osuc-≡< z≤x @@ -1270,7 +1260,7 @@ is02 : {w : Ordinal } → odef (uchain f mf ay) w → (w ≡ s) ∨ (w << s) is02 fc = sup ⟪ A∋fc _ f mf fc , ch-init fc ⟫ ... | case2 lt = ⊥-elim ( ¬x<0 (subst (λ k → z o< k ) x=0 lt ) ) - ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = order ; 0<supfz = 0<sufz + ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = order ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = cfcs } where mf : ≤-monotonic-f A f @@ -1357,22 +1347,55 @@ ZChain.supf (pzc (pic<x ia)) (IChain-i ia) ∎ ) sa<sb ) where open o≤-Reasoning O IC⊆ : {a b : Ordinal } (ia : IChain ay supfz a ) (ib : IChain ay supfz b ) - → IChain-i ia o≤ IChain-i ib → odef (ZChain.chain (pzc (pic<x ib))) a - IC⊆ {a} {b} (ic-init fc ) ib ia≤ib = ⟪ A∋fc _ f mf fc , ch-init fc ⟫ - IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia≤ib = ⊥-elim ( o≤> ia≤ib ic01 ) where + → IChain-i ia o< IChain-i ib → odef (ZChain.chain (pzc (pic<x ib))) a + IC⊆ {a} {b} (ic-init fc ) ib ia<ib = ⟪ A∋fc _ f mf fc , ch-init fc ⟫ + IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia<ib = ⊥-elim ( o<> ia<ib ic01 ) where ic02 : o∅ o< supfz i<x - ic02 = ZChain.0<supfz (pzc (ob<x lim i<x)) + ic02 = ? ic01 : o∅ o< i ic01 = ordtrans<-≤ ic02 sa<x - IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia≤ib - = ZChain.cfcs (pzc (ob<x lim j<x) ) ia≤ib o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) ia≤ib) sb<x) - (subst (λ k → FClosure A f k a) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc)) fc ) + IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia<ib + = ZChain.cfcs (pzc (ob<x lim j<x) ) (o<→≤ ia<ib) o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) (o<→≤ ia<ib)) sb<x) + (subst (λ k → FClosure A f k a) (zeq _ _ (osucc (o<→≤ ia<ib)) (o<→≤ <-osuc)) fc ) ptotalU : IsTotalOrderSet pchainU ptotalU {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib)) - ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o<→≤ ia<ib)) (pchainU⊆chain ib) - ... | tri≈ ¬a ia=ib ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) (o≤-refl0 ia=ib)) (pchainU⊆chain ib) - ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainU⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) (o<→≤ ib<ia)) + ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) ia<ib) (pchainU⊆chain ib) + ... | tri≈ ¬a ia=ib ¬c = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso ( pcmp (proj2 ia) (proj2 ib) ia=ib ) where + pcmp : (ia : IChain ay supfz (& a)) → (ib : IChain ay supfz (& b)) → IChain-i ia ≡ IChain-i ib + → Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) + pcmp (ic-init fca) (ic-init fcb) eq = fcn-cmp _ f mf fca fcb + pcmp (ic-init fca) (ic-isup i i<x s<x fcb) eq with ZChain.fcy<sup (pzc i<x) o≤-refl fca + ... | case1 eq1 = ct22 where + ct22 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) + ct22 with subst (λ k → k ≤ & b) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fcb ) + ... | case1 eq2 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where + ct00 : * (& a) ≡ * (& b) + ct00 = cong (*) (trans eq1 eq2) + ... | case2 lt = tri< fc11 (λ eq → <-irr (case1 (sym eq)) fc11) (λ lt → <-irr (case2 fc11) lt) where + fc11 : * (& a) < * (& b) + fc11 = subst (λ k → k < * (& b) ) (cong (*) (sym eq1)) lt + ... | case2 lt = tri< fc11 (λ eq → <-irr (case1 (sym eq)) fc11) (λ lt → <-irr (case2 fc11) lt) where + fc11 : * (& a) < * (& b) + fc11 = ftrans<-≤ lt (subst (λ k → k ≤ & b) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fcb ) ) + pcmp (ic-isup i i<x s<x fca) (ic-init fcb) eq with ZChain.fcy<sup (pzc i<x) o≤-refl fcb + ... | case1 eq1 = ct22 where + ct22 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) + ct22 with subst (λ k → k ≤ & a) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fca ) + ... | case1 eq2 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where + ct00 : * (& a) ≡ * (& b) + ct00 = cong (*) (sym (trans eq1 eq2)) + ... | case2 lt = tri> (λ lt → <-irr (case2 fc11) lt) (λ eq → <-irr (case1 eq) fc11) fc11 where + fc11 : * (& b) < * (& a) + fc11 = subst (λ k → k < * (& a) ) (cong (*) (sym eq1)) lt + ... | case2 lt = tri> (λ lt → <-irr (case2 fc12) lt) (λ eq → <-irr (case1 eq) fc12) fc12 where + fc12 : * (& b) < * (& a) + fc12 = ftrans<-≤ lt (subst (λ k → k ≤ & a) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fca ) ) + pcmp (ic-isup i i<x s<x fca) (ic-isup i i<y s<y fcb) refl = fcn-cmp _ f mf fca (subst (λ k → FClosure A f k (& b)) pc01 fcb ) where + pc01 : supfz i<y ≡ supfz i<x + pc01 = cong supfz o<-irr + ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainU⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) ib<ia) + usup : MinSUP A pchainU usup = minsupP pchainU (λ ic → proj1 ic ) ptotalU @@ -1483,9 +1506,6 @@ ... | tri≈ ¬a z=x ¬c = MinSUP.minsup usup (MinSUP.as ssup) (λ uw → MinSUP.x≤sup ssup (case1 uw) ) ... | tri> ¬a ¬b c = o≤-refl -- (sf1=sps c) - 0<sufz : {x : Ordinal } → o∅ o< supf1 x - 0<sufz = ordtrans<-≤ (ZChain.0<supfz (pzc (ob<x lim 0<x ))) (OrdTrans (o≤-refl0 (sym (sf1=sf 0<x ))) (supf-mono o∅≤z)) - is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z) is-minsup {z} z≤x with osuc-≡< z≤x ... | case1 z=x = record { as = asupf ; x≤sup = zm00 ; minsup = zm01 } where @@ -1601,52 +1621,28 @@ 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 = subst (λ k → x o≤ k) (sym (sf1=spu refl)) z47 where + ... | case1 refl with x<y∨y≤x (supf1 spu) x + ... | case2 x≤ssp = z40 where + z40 : z o≤ supf1 z + z40 with x<y∨y≤x z spu + ... | case1 z<spu = o<→≤ ( subst (λ k → z o< k ) (sym (sf1=spu refl)) z<spu ) + ... | case2 spu≤z = begin -- x ≡ supf1 spu ≡ spu ≡ supf1 x + x ≤⟨ x≤ssp ⟩ + supf1 spu ≤⟨ supf-mono spu≤z ⟩ + supf1 x ∎ where open o≤-Reasoning O + ... | case1 ssp<x = 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 + z70 : odef (UnionCF A f ay supf1 z) (supf1 spu) + z70 = cfcs spu<x o≤-refl ssp<x (init asupf refl ) + z73 : IsSUP A (UnionCF A f ay (ZChain.supf (pzc (ob<x lim spu<x))) spu) spu + z73 = record { ax = MinSUP.as usup ; x≤sup = λ uw → MinSUP.x≤sup usup (chain⊆pchainU1 spu<x uw ) } 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 ) - (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 - u<z : u o< z - u<z = ordtrans u<b spu<x - z57 : supfz (ordtrans u<b spu<x) ≡ u - z57 = trans (trans (zeq _ _ o≤-refl (o<→≤ <-osuc) ) (sym (sf1=sf u<z))) su=u - z55 : supfz (ordtrans u<b spu<x) o≤ u - z55 = o≤-refl0 z57 - 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 ) - (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} ⟪ 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 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 + z49 = begin + supfz spu<x ≡⟨ ZChain.sup=u (pzc (ob<x lim spu<x)) (MinSUP.as usup) (o<→≤ <-osuc) z73 ⟩ + spu ∎ where open ≡-Reasoning z50 : supfz spu<x o≤ spu z50 = o≤-refl0 z49 z48 : odef pchainU (f spu)