Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 954:e43a5cc72287
IsSUP is now min sup
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 02 Nov 2022 13:53:10 +0900 |
| parents | dfb4f7e9c454 |
| children | bc27df170a1e |
| files | src/zorn.agda |
| diffstat | 1 files changed, 89 insertions(+), 71 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Nov 02 03:42:53 2022 +0900 +++ b/src/zorn.agda Wed Nov 02 13:53:10 2022 +0900 @@ -243,6 +243,8 @@ record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x) : Set n where field x≤sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) + minsup : { sup1 : Ordinal } → odef A sup1 + → ( {z : Ordinal } → odef B z → (z ≡ sup1 ) ∨ (z << sup1 )) → x o≤ sup1 record SUP ( A B : HOD ) : Set (Level.suc n) where field @@ -659,7 +661,15 @@ 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) (chain-mono1 (o<→≤ b<x) uz) } , m04 ⟫ + ⟪ record { x≤sup = λ {z} uz → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz) + ; minsup = m07 } , m04 ⟫ where + m10 : {s : Ordinal } → (odef A s ) + → ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) ) + → {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) z → (z ≡ s) ∨ (z << s) + m10 = ? + m07 : {sup1 : Ordinal} → odef A sup1 → ({z : Ordinal} → + odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ sup1) ∨ (z << sup1)) → b o≤ sup1 + m07 {s} as min = IsSup.minsup (proj2 is-sup) as (m10 as min) m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b @@ -692,7 +702,8 @@ ; 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) (chain-mono1 (o<→≤ b<x) lt )} , m04 ⟫ -- ZChain on x + ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt ) + ; minsup = ? } , m04 ⟫ -- ZChain on x m06 : ChainP A f mf ay supf b m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = m05 } @@ -725,7 +736,7 @@ ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x ind f mf {y} ay x prev with Oprev-p x - ... | yes op = zc4 where + ... | yes op = zc41 where -- -- we have previous ordinal to use induction -- @@ -755,63 +766,69 @@ ... | case1 eq = case2 eq ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) - zc41 : supf0 px o< x → ZChain A f mf ay x - zc41 sfpx<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? + -- + -- find the next value of supf + -- + + pchainpx : HOD + pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain A f mf ay supf0 px z ) + ∨ FClosure A f (supf0 px) z } ; odmax = & A ; <odmax = zc00 } where + zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → z o< & A + zc00 {z} (case1 lt) = z07 lt + zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc ) + + zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f (supf0 px) b → a <= b + zc02 {a} {b} ca fb = zc05 fb where + zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ supf0 px + zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) refl + 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 ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb) + ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) + zc05 (init b1 refl) with MinSUP.x≤sup (ZChain.minsup zc o≤-refl) + (subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca ) + ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq ) + ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt ) + + ptotal : IsTotalOrderSet pchainpx + ptotal (case1 a) (case1 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso + (chain-total A f mf ay supf0 (proj2 a) (proj2 b)) + ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b + ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where + eq1 : a0 ≡ b0 + eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq ) + ... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where + lt1 : a0 < b0 + lt1 = subst₂ (λ j k → j < k ) *iso *iso lt + ptotal {b0} {a0} (case2 b) (case1 a) with zc02 a b + ... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where + eq1 : a0 ≡ b0 + eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq ) + ... | 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) + + pcha : pchainpx ⊆' A + pcha (case1 lt) = proj1 lt + pcha (case2 fc) = A∋fc _ f mf fc + + sup1 : MinSUP A pchainpx + sup1 = minsupP pchainpx pcha ptotal + sp1 = MinSUP.sup sup1 + + -- + -- supf0 px o≤ sp1 + -- + + zc41 : ZChain A f mf ay x + zc41 with MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl )) + zc41 | (case2 sfpx<sp1) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where - -- supf0 px is included by the chain + -- supf0 px is included by the chain of sp1 -- ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x -- supf1 x ≡ sp1, which is not included now - pchainpx : HOD - pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain A f mf ay supf0 px z ) - ∨ FClosure A f (supf0 px) z } ; odmax = & A ; <odmax = zc00 } where - zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → z o< & A - zc00 {z} (case1 lt) = z07 lt - zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc ) - zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → odef A z - zc01 {z} (case1 lt) = proj1 lt - zc01 {z} (case2 fc) = ( A∋fc (supf0 px) f mf fc ) - - zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f (supf0 px) b → a <= b - zc02 {a} {b} ca fb = zc05 fb where - zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ supf0 px - zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) refl - 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 ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb) - ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) - zc05 (init b1 refl) with MinSUP.x≤sup (ZChain.minsup zc o≤-refl) - (subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca ) - ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq ) - ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt ) - - ptotal : IsTotalOrderSet pchainpx - ptotal (case1 a) (case1 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso - (chain-total A f mf ay supf0 (proj2 a) (proj2 b)) - ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b - ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where - eq1 : a0 ≡ b0 - eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq ) - ... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where - lt1 : a0 < b0 - lt1 = subst₂ (λ j k → j < k ) *iso *iso lt - ptotal {b0} {a0} (case2 b) (case1 a) with zc02 a b - ... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where - eq1 : a0 ≡ b0 - eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq ) - ... | 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) - - pcha : pchainpx ⊆' A - pcha (case1 lt) = proj1 lt - pcha (case2 fc) = A∋fc _ f mf fc - - sup1 : MinSUP A pchainpx - sup1 = minsupP pchainpx pcha ptotal - sp1 = MinSUP.sup sup1 - supf1 : Ordinal → Ordinal supf1 z with trio< z px ... | tri< a ¬b ¬c = supf0 z @@ -943,11 +960,13 @@ s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx) ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px ⟫ ) zc12 {z} (case2 fc) = zc21 fc where + zc20 : (supf0 px ≡ px ) ∨ ( supf0 px o< px ) + zc20 = ? zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ - zc21 (init asp refl ) with osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x ) + zc21 (init asp refl ) with zc20 ... | case1 sfpx=px = ⟪ asp , ch-is-sup px zc18 record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where zc15 : supf1 px ≡ px @@ -976,7 +995,7 @@ ... | case2 sfp<px with ZChain.csupf zc sfp<px -- odef (UnionCF A f mf ay supf0 px) (supf0 px) ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ - ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u ? + ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u zc18 record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ ? ) ⟫ where z10 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) (ChainP.fcy<sup is-sup fc) @@ -992,6 +1011,8 @@ lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ? ) lt z12 : supf1 u ≡ u z12 = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup) + zc18 : supf1 u o< supf1 x + zc18 = ? @@ -1055,17 +1076,13 @@ 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 (λ k → supf0 px o< k ) (sym opx=x) sfpx<x + cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) ? csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ ) - zc4 : ZChain A f mf ay x --- x o≤ supf px - zc4 with trio< x (supf0 px) - ... | tri> ¬a ¬b c = zc41 c - ... | tri≈ ¬a b ¬c = ? - ... | tri< a ¬b ¬c = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? + zc41 | (case1 sfp=sp1 ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ? ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ? } where -- supf0 px not is included by the chain @@ -1145,7 +1162,7 @@ zc12 = subst (λ k → supf0 k ≡ u1) eq ? zcsup : xSUP (UnionCF A f mf ay supf0 px) x zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (ZChain.asupf zc) - ; is-sup = record { x≤sup = x≤sup } } + ; is-sup = record { x≤sup = x≤sup ; minsup = ? } } zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 ? where eq : u1 ≡ x eq with trio< u1 x @@ -1197,8 +1214,8 @@ sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b sup=u {b} ab b≤x is-sup with trio< b px - ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫ - ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫ + ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ + ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ ... | tri> ¬a ¬b px<b = zc31 ? where zc30 : x ≡ b zc30 with osuc-≡< b≤x @@ -1207,7 +1224,7 @@ zcsup : xSUP (UnionCF A f mf ay supf0 px) x zcsup with zc30 ... | refl = record { ax = ab ; is-sup = record { x≤sup = λ {w} lt → - IsSup.x≤sup (proj1 is-sup) ?} } + IsSup.x≤sup (proj1 is-sup) ? ; minsup = ? } } zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A (UnionCF A f mf ay supf0 px) x f) → supf0 b ≡ b zc31 (case1 ¬sp=x) with zc30 ... | refl = ⊥-elim (¬sp=x zcsup ) @@ -1366,7 +1383,7 @@ ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1) - z19 = record { x≤sup = z20 } where + z19 = record { x≤sup = z20 ; minsup = ? } where z20 : {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1)) z20 {y} zy with x≤sup (subst (λ k → odef chain k ) (sym &iso) zy) ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p )) @@ -1496,7 +1513,8 @@ sc=c : supf mc ≡ mc sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1) - is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )} + is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy ) + ; minsup = ? } not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) mc (cf nmx) not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where z30 : * mc < * (cf nmx mc) @@ -1515,7 +1533,7 @@ z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc _ fc ))) is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd) - is-sup = record { x≤sup = z22 } where + is-sup = record { x≤sup = z22 ; minsup = ? } where z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd) z23 lt = MinSUP.x≤sup spd lt z22 : {y : Ordinal} → odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) y →