Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 793:bcc241fbb390
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 05 Aug 2022 09:22:47 +0900 |
| parents | 150e1c7097ce |
| children | 0acbc2b102e9 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 69 insertions(+), 53 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Aug 04 06:59:40 2022 +0900 +++ b/src/zorn.agda Fri Aug 05 09:22:47 2022 +0900 @@ -276,7 +276,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 : {sup1 z1 : Ordinal} → (lt : supf sup1 o< supf u ) → FClosure A f (supf sup1 ) 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 : o∅ o< u → supf u ≡ u -- Union of supf z which o< x -- @@ -492,21 +493,26 @@ cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ + chain-mono : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) + {a b c : Ordinal} → a o≤ b + → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c + chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = + ⟪ ua , ch-init fc ⟫ + chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ua ua<x is-sup fc ⟫ = + ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x (osucc a≤b )) is-sup fc ⟫ + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) (total : IsTotalOrderSet (ZChain.chain zc) ) → SUP A (ZChain.chain zc) sp0 f mf zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y) - SZ1 :( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) + SZ1 : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → ZChain1 A f mf ay zc x - SZ1 A f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where - chain-mono1 : (x : Ordinal) {a b c : Ordinal} → a o≤ b + SZ1 f mf {y} ay zc x = TransFinite { λ x → ZChain1 A f mf ay zc x } zc1 x where + chain-mono1 : {a b c : Ordinal} → a o≤ b → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c - chain-mono1 x {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = - ⟪ ua , ch-init fc ⟫ - chain-mono1 x {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ua ua<x is-sup fc ⟫ = - ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x (osucc a≤b )) is-sup fc ⟫ + chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → b o< x → (ab : odef A b) → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f → @@ -533,14 +539,14 @@ b<A = z09 ab m05 : b ≡ ZChain.supf zc b m05 = sym ( ZChain.sup=u zc ab (z09 ab) - record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 x (osucc b<x) uz ) } ) + record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (osucc 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 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b m09 {sup1} {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 b<A ? } ... | 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) → @@ -549,7 +555,7 @@ is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay ) ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ - ... | case2 y<b = chain-mono1 x (osucc b<x) + ... | case2 y<b = chain-mono1 (osucc b<x) ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc ) m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫ where m09 : b o< & A m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab)) @@ -560,9 +566,9 @@ m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc m05 : b ≡ ZChain.supf zc b m05 = sym (ZChain.sup=u zc ab m09 - record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 x (osucc b<x) lt )} ) -- ZChain on x + record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc 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 m09 ? } --- --- the maximum chain has fix point of any ≤-monotonic function @@ -576,7 +582,7 @@ z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) → HasPrev A chain ab f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) → * a < * b → odef chain b - z10 = ZChain1.is-max (SZ1 A f mf as0 zc (& A) ) + z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) z11 : & (SUP.sup sp1) o< & A z11 = c<→o< ( SUP.A∋maximal sp1) z12 : odef chain (& (SUP.sup sp1)) @@ -641,8 +647,8 @@ → SUP A (uchain f mf ay) ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay) - inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅ - inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; sup = ? ; supf-is-sup = ? + initChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅ + initChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; sup = ? ; supf-is-sup = ? ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; supf-mono = mono ; csupf = csupf } where spi = & (SUP.sup (ysup f mf ay)) isupf : Ordinal → Ordinal @@ -681,8 +687,10 @@ uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi) uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi ) uz02 : ChainP A f mf ay isupf o∅ - uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} } + uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} ; supu=u = λ lt → ⊥-elim ( o<¬≡ refl lt ) } + SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B + SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; A∋maximal = SUP.A∋maximal sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt) } -- -- create all ZChains under o< x @@ -725,25 +733,26 @@ supf0 = ZChain.supf zc + sup1 : SUP A (UnionCF A f mf ay supf0 x) + sup1 = supP pchain pchain⊆A ptotal + sp1 = & (SUP.sup sup1 ) + supf1 : Ordinal → Ordinal + supf1 z with trio< z px + ... | tri< a ¬b ¬c = ZChain.supf zc z + ... | tri≈ ¬a b ¬c = ZChain.supf zc z + ... | tri> ¬a ¬b c = sp1 + -- if previous chain satisfies maximality, we caan reuse it -- -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x - no-extension : ZChain A f mf ay x - no-extension = record { supf = supf1 ; supf-mono = ? ; sup = sup + no-extension : ¬ sp1 ≡ x → ZChain A f mf ay x + no-extension ¬sp=x = record { supf = supf1 ; supf-mono = ? ; sup = sup ; initial = ? ; chain∋init = ? ; sup=u = {!!} ; supf-is-sup = ? ; csupf = ? ; chain⊆A = ? ; f-next = ? ; f-total = ? } where - sup1 : SUP A (UnionCF A f mf ay supf0 x) - sup1 = supP pchain pchain⊆A ptotal - sp1 = & (SUP.sup sup1 ) - supf1 : Ordinal → Ordinal - supf1 z with trio< z px - ... | tri< a ¬b ¬c = ZChain.supf zc z - ... | tri≈ ¬a b ¬c = ZChain.supf zc z - ... | tri> ¬a ¬b c = sp1 UnionCF⊆ : UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay supf0 x UnionCF⊆ ⟪ as , ch-init fc ⟫ = UnionCF⊆ ⟪ as , ch-init fc ⟫ - UnionCF⊆ ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = o1 } fc ⟫ with trio< u px - ... | tri< a ¬b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 } fc ⟫ where + UnionCF⊆ ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = o1 ; supu=u = su=u1 } fc ⟫ with trio< u px + ... | tri< a ¬b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 ; supu=u = ? } fc ⟫ where order0 : {s z1 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s @@ -752,7 +761,7 @@ ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su ) (subst (λ k → FClosure A f k z1 ) (sym eq1) fc ) ... | tri> ¬a ¬b c | record {eq = eq1} = ? - ... | tri≈ ¬a b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 } fc ⟫ where + ... | tri≈ ¬a b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 ; supu=u = ?} fc ⟫ where order0 : {s z1 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s @@ -760,41 +769,48 @@ (subst (λ k → FClosure A f k z1 ) (sym eq1) fc ) ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su ) (subst (λ k → FClosure A f k z1 ) (sym eq1) fc ) - ... | tri> ¬a ¬b c | record {eq = eq1} = ? - ... | tri> ¬a ¬b c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = fcy<sup ; order = order } fc0 ⟫ where - -- px o< u , u o< osuc x → u ≡ x - -- supf0 x ≡ sp1 ≡ x - -- u≤x → supf0 u < x - fc1 : FClosure A f sp1 z - fc1 = fc - fc0 : FClosure A f (supf0 u) z - fc0 = ? - fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u) ∨ (z << supf0 u) - fcy<sup {z} fc = ? - order : {s z1 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) - order = ? + ... | tri> ¬a ¬b px<s | record {eq = eq1} = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x ? )) where + s≤u : s o≤ u + s≤u = ? + u=x : u ≡ x + u=x with trio< u x + ... | tri< a ¬b ¬c = ? + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b c = ? + ... | tri> ¬a ¬b c = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x (su=u1 ?) )) where + u=x : u ≡ x + u=x with trio< u x + ... | tri< a ¬b ¬c = ? + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b c = ? sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) sup {z} z≤x with trio< z px - ... | tri< a ¬b ¬c = ? -- ZChain.sup zc (o<→≤ a) - ... | tri≈ ¬a b ¬c = ? -- ZChain.sup zc (o≤-refl0 b) - ... | tri> ¬a ¬b c = ? -- sp1 + ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup zc (o<→≤ a)) + ... | tri≈ ¬a b ¬c = SUP⊆ ? (ZChain.sup zc (o≤-refl0 b)) + ... | tri> ¬a ¬b c = SUP⊆ ? sup1 zc4 : ZChain A f mf ay x - zc4 with ODC.∋-p O A (* px) - ... | no noapx = no-extension -- ¬ A ∋ p, just skip - ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) apx f ) + zc4 with ODC.∋-p O A (* x) + ... | no noax = no-extension ? -- ¬ A ∋ p, just skip + ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f ) -- we have to check adding x preserve is-max ZChain A y f mf x - ... | 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 ) apx ) + ... | 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 = {!!} ; sup=u = {!!} ; supf-mono = {!!} ; initial = {!!} ; chain∋init = {!!} ; sup = ? ; supf-is-sup = ? ; supf-mono = ? } where + supx : SUP A (UnionCF A f mf ay supf0 x) + supx = record { sup = * x ; A∋maximal = subst (λ k → odef A k ) ? ax ; x<sup = ? } + spx = & (SUP.sup supx ) + x=spx : x ≡ spx + x=spx = ? psupf1 : Ordinal → Ordinal psupf1 z with trio< z x ... | tri< a ¬b ¬c = ZChain.supf zc z ... | tri≈ ¬a b ¬c = x ... | tri> ¬a ¬b c = x - ... | case2 ¬x=sup = no-extension -- px is not f y' nor sup of former ZChain from y -- no extention + + ... | case2 ¬x=sup = no-extension ? -- px is not f y' nor sup of former ZChain from y -- no extention ... | no lim = zc5 where @@ -856,7 +872,7 @@ ... | case1 eq = case1 (trans eq (sym eq1) ) ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt) cp1 : ChainP A f mf ay psupf z - cp1 = record { fcy<sup = zc20 ; order = ? } + cp1 = record { fcy<sup = zc20 ; order = ? ; supu=u = ?} --- u = supf u = supf z ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup ? {!!} {!!} {!!} ⟫ where sa = SUP.A∋maximal usup