Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 828:802d70b7ea01
csupf fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 19 Aug 2022 09:52:27 +0900 |
| parents | 685f7ae1b821 |
| children | 4822758b8bf8 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 39 insertions(+), 48 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Aug 19 09:30:32 2022 +0900 +++ b/src/zorn.agda Fri Aug 19 09:52:27 2022 +0900 @@ -251,7 +251,8 @@ record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u : Ordinal) : Set n where field fcy<sup : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) - order : {s z1 : Ordinal} → (lt : s o< u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u ) + order : {s z1 : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u ) + supu=u : supf u ≡ u data UChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where @@ -286,10 +287,7 @@ sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z → IsSup A (UnionCF A f mf ay supf b) ab → supf b ≡ b supf-is-sup : {x : Ordinal } → (x≤z : x o< z) → supf x ≡ & (SUP.sup (sup x≤z) ) supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y - csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) - -- supf b ≡ b → csupf0 → csupf - csupf0 : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b) ) (supf b) - csupf0 {b} b≤z = ? + csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) supf-inject : {x y : Ordinal } → supf x o< supf y → x o< y supf-inject {x} {y} sx<sy with trio< x y ... | tri< a ¬b ¬c = a @@ -306,41 +304,32 @@ ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup u<z ) ) )) ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u<z ))) ) lt ) - -- supf s o< b - order : {b s z1 : Ordinal} → b o< z → s o< b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) - order {b} {s} {z1} b<z s<b fc = zc04 where + order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) + order {b} {s} {z1} b<z ss<sb fc = zc04 where zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 - zc01 (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc03 where + zc01 (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where + s<b : s o< b + s<b = supf-inject ss<sb s<z : s o< z s<z = ordtrans s<b b<z zc04 : odef (UnionCF A f mf ay supf (supf s)) (supf s) - zc04 = ? + zc04 = csupf (o<→≤ s<z ) zc05 : odef (UnionCF A f mf ay supf b) (supf s) zc05 with zc04 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ - ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u ? is-sup fc ⟫ where + ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 u≤x ) is-sup fc ⟫ where zc06 : supf u ≡ u - zc06 = sup=u ? ? ? - zc09 : u o≤ supf s → ( u o≤ b ) ∨ ( supf u ≡ supf b ) + zc06 = ChainP.supu=u is-sup + zc09 : u o≤ supf s → u o≤ b zc09 u<s with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u<s) ... | case1 su=ss = zc08 where zc07 : supf u o≤ supf b zc07 = subst (λ k → k o≤ supf b) (sym su=ss) (supf-mono (o<→≤ s<b) ) - zc08 : ( u o≤ b ) ∨ ( supf u ≡ supf b ) + zc08 : u o≤ b zc08 with osuc-≡< zc07 - ... | case1 su=sb = case2 su=sb - ... | case2 lt = case1 ( o<→≤ (supf-inject lt )) - ... | case2 lt = case1 ( o<→≤ (ordtrans (supf-inject lt) s<b) ) - zc10 : odef (UnionCF A f mf ay supf b) (supf s) - zc10 with zc09 u≤x - ... | case1 lt = ⟪ as , ch-is-sup u lt is-sup fc ⟫ - ... | case2 eq = ⟪ as , ch-is-sup b ? record { fcy<sup = ? ; order = ? } (init ? ? ) ⟫ where - zc11 : supf (supf s) ≡ supf s - zc11 = ? - zc03 : odef (UnionCF A f mf ay supf b) (supf s) - zc03 with csupf (o<→≤ s<z) - ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ - ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u≤x (osucc s<b)) is-sup fc ⟫ + ... | case1 su=sb = ⊥-elim ( o<¬≡ (trans ? su=sb ) ss<sb ) + ... | case2 lt = o<→≤ (supf-inject lt ) + ... | case2 lt = o<→≤ (ordtrans (supf-inject lt) s<b) zc01 (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where zc04 : odef (UnionCF A f mf ay supf b) (f x) zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc ) @@ -404,7 +393,7 @@ ... | case1 eq = subst (λ k → * b < k ) eq ct00 ... | case2 lt = IsStrictPartialOrder.trans POO ct00 lt ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub - ... | tri< a₁ ¬b ¬c with ChainP.order supb a₁ fca + ... | tri< a₁ ¬b ¬c with ChainP.order supb ? fca ... | case1 eq with s≤fc (supf ub) f mf fcb ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * a ≡ * b @@ -421,7 +410,7 @@ ... | case2 lt = IsStrictPartialOrder.trans POO ct03 lt ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri≈ ¬a eq ¬c = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (cong supf (sym eq)) fcb ) - ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa c fcb + ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa ? fcb ... | case1 eq with s≤fc (supf ua) f mf fca ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * a ≡ * b @@ -550,11 +539,12 @@ record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz ) } ) m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b m08 {z} fcz = ZChain.fcy<sup zc b<A fcz - m09 : {s z1 : Ordinal} → s o< b + m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b m09 {s} {z} s<b fcz = ZChain.order zc b<A s<b fcz m06 : ChainP A f mf ay (ZChain.supf zc) b - m06 = record { fcy<sup = m08 ; order = m09 } + m06 = record { fcy<sup = m08 ; order = m09 ; supu=u = ZChain.sup=u zc ab (o<→≤ b<A ) + record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz ) } } ... | no lim = record { is-max = is-max } where is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → b o< x → (ab : odef A b) → @@ -569,14 +559,15 @@ m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b m07 {z} fc = ZChain.fcy<sup zc m09 fc - m08 : {s z1 : Ordinal} → s o< b + m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b m08 {s} {z1} s<b fc = ZChain.order zc m09 s<b fc m05 : b ≡ ZChain.supf zc b m05 = sym (ZChain.sup=u zc ab (o<→≤ m09) record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} ) -- ZChain on x m06 : ChainP A f mf ay (ZChain.supf zc) b - m06 = record { fcy<sup = m07 ; order = m08 } + m06 = record { fcy<sup = m07 ; order = m08 ; supu=u = ZChain.sup=u zc ab (o<→≤ m09) + record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} } --- --- the maximum chain has fix point of any ≤-monotonic function @@ -741,17 +732,17 @@ zc60 : {w : Ordinal } → FClosure A f (supf0 u1) w → odef (UnionCF A f mf ay supf1 z1 ) w zc60 (init asp refl) with trio< u1 px | inspect supf1 u1 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) - record { fcy<sup = fcy<sup ; order = order } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ where + record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup) } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 ) ⟫ where fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 ) fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc ) order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 → (z2 ≡ supf1 u1) ∨ (z2 << supf1 u1) order {s} {z2} s<u1 fc with trio< s px - ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc ) - ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 ? ) + ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? fc ) + ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup ? ? ) ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) )) -- px o< s < u1 < px ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) - record { fcy<sup = fcy<sup ; order = order } (init (subst (λ k → odef A k ) (sym eq1) ? ) ? ) ⟫ where + record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans eq1 ? } (init (subst (λ k → odef A k ) (sym eq1) ? ) ? ) ⟫ where fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 ) fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ? -- ( ChainP.fcy<sup u1-is-sup fc ) order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 → @@ -768,7 +759,7 @@ ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ no-extension : ¬ xSUP → ZChain A f mf ay x no-extension ¬sp=x = record { supf = supf1 ; sup = sup - ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf + ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = ? ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where UnionCFR⊆ : {z0 z1 : Ordinal} → z0 o≤ z1 → z0 o< x → UnionCF A f mf ay supf1 z0 ⊆' UnionCF A f mf ay supf0 z1 UnionCFR⊆ {z0} {z1} z0≤1 z0<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ @@ -776,24 +767,24 @@ zc60 : {w : Ordinal } → FClosure A f (supf1 u1) w → odef (UnionCF A f mf ay supf0 z1 ) w zc60 {w} (init asp refl) with trio< u1 px | inspect supf1 u1 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) - record { fcy<sup = fcy<sup ; order = order } (init asp refl ) ⟫ where + record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup) } (init asp refl ) ⟫ where fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 ) fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc ) order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 → (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s - ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) - ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) ? )) + ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) + ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) ? )) ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) )) -- px o< s < u1 < px ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) - record { fcy<sup = fcy<sup ; order = order } (init ? ? ) ⟫ where + record { fcy<sup = fcy<sup ; order = ? ; supu=u = trans (sym ? ) (ChainP.supu=u u1-is-sup) } (init ? ? ) ⟫ where fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 ) fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc ) order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 → (z2 ≡ supf0 u1) ∨ (z2 << supf0 u1) order {s} {z2} s<u1 fc with trio< s px | inspect supf1 s - ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ?( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) fc )) - ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) ? )) + ... | tri< a ¬b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ?( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) fc )) + ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) ? ( ChainP.order u1-is-sup ? (subst (λ k → FClosure A f k z2) (sym eq2) ? )) ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) )) -- px o< s < u1 = px ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with trio< z0 px ... | tri< a ¬b ¬c with osuc-≡< (OrdTrans u1≤x (o<→≤ a) ) @@ -828,7 +819,7 @@ ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) ? lt) } } csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b) csupf {b} b<x with trio< b px | inspect supf1 b - ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl a ( ZChain.csupf zc (o<→≤ a) ) + ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl a ? ... | tri≈ ¬a refl ¬c | _ = ? -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl ) ... | tri> ¬a ¬b px<b | record { eq = eq1 } = ? -- UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x)) @@ -844,7 +835,7 @@ ... | case1 pr = no-extension {!!} -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax ) ... | case1 is-sup = -- x is a sup of zc - record { supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = csupf ; sup=u = {!!} + record { supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = ? ; sup=u = {!!} ; initial = {!!} ; chain∋init = {!!} ; sup = {!!} ; supf-is-sup = {!!} } where supx : SUP A (UnionCF A f mf ay supf0 x) supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} } @@ -943,7 +934,7 @@ no-extension : ¬ xSUP → ZChain A f mf ay x no-extension ¬sp=x = record { initial = pinit ; chain∋init = pcy ; supf = supf1 ; sup=u = sup=u ; sup = sup ; supf-is-sup = sis - ; csupf = csupf ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } where + ; csupf = ? ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } where supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay (supfu a) x @@ -982,7 +973,7 @@ zc9 : odef (UnionCF A f mf ay supf1 z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z) zc9 = {!!} zc8 : odef (UnionCF A f mf ay (supfu a) z) (ZChain.supf (pzc (osuc z) (ob<x lim a)) z) - zc8 = ZChain.csupf (pzc (osuc z) (ob<x lim a)) ? -- (o<→≤ <-osuc ) + zc8 = ? -- ZChain.csupf (pzc (osuc z) (ob<x lim a)) ? -- (o<→≤ <-osuc ) ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z ? ))