Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 868:35a884f2bfde
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 13 Sep 2022 02:49:49 +0900 |
| parents | 166bee3ddf4c |
| children | 1ca338c3f09c |
| files | src/zorn.agda |
| diffstat | 1 files changed, 23 insertions(+), 99 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Sep 12 19:35:32 2022 +0900 +++ b/src/zorn.agda Tue Sep 13 02:49:49 2022 +0900 @@ -365,6 +365,9 @@ {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where field supf : Ordinal → Ordinal + pchain : HOD + pchain = UnionCF A f mf ay supf z + field sup : (x : Ordinal ) → SUP A (UnionCF A f mf ay (λ _ → z) x) supf-is-sup : {x : Ordinal } → supf x ≡ & (SUP.sup (sup x) ) supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y @@ -376,28 +379,6 @@ -- sup y < sup z1 < sup z2 -- o< o< -smono→SUPU : (A : HOD) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) - → {x z : Ordinal } → { supf : Ordinal → Ordinal } - → ( supf x ≡ z ) → ( {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) - → ( {x y : Ordinal } → x o≤ y → supf x <= supf y ) - → (sz : SUP A (UnionCF A f mf ay (λ _ → z) x)) → (su : SUP A (UnionCF A f mf ay supf x)) → & (SUP.sup sz) ≡ & (SUP.sup su) -smono→SUPU A f mf {y} ay {x} {z} {supf} sx=z mono mono< s = ? where - sup = SUP.sup s - x<sup : {w : HOD} → (UnionCF A f mf ay supf x) ∋ w → (w ≡ sup ) ∨ (w < sup ) - x<sup {w} ⟪ au , ch-init fc ⟫ = SUP.x<sup s ⟪ au , ch-init fc ⟫ - x<sup {w} ⟪ au , ch-is-sup u u<x is-sup fc ⟫ with trio< u z - ... | tri< a ¬b ¬c = ? where - zc01 : {s : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) (& w) → ((& w) ≡ supf u ) ∨ ( (& w) << supf u ) - zc01 = ChainP.order is-sup - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b z<u = ⊥-elim ( o≤> u≤z z<u ) where - u≤z : u o≤ z - u≤z = begin u ≡⟨ sym (ChainP.supu=u is-sup) ⟩ - supf u ≤⟨ mono (o<→≤ u<x ) ⟩ - supf x ≡⟨ sx=z ⟩ - z ∎ where open o≤-Reasoning O - - zsupf : (A : HOD) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B ) -- SUP condition → (x : Ordinal) → ZSupf A f mf ay x @@ -407,8 +388,8 @@ zc1 x prev with Oprev-p x ... | yes op = record { supf = ? ; sup = ? ; supf-is-sup = ? ; supf-mono = ? } where px = Oprev.oprev op - pchain : HOD - pchain = UnionCF A f mf ay (ZSupf.supf ( prev px (pxo<x op) )) px + pchain0 : HOD + pchain0 = UnionCF A f mf ay (ZSupf.supf ( prev px (pxo<x op) )) px zc-b<x : {b : Ordinal } → b o< x → b o< osuc px zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt @@ -418,18 +399,14 @@ ... | tri≈ ¬a b ¬c = ZSupf.supf (prev z (subst (λ k → k o< x ) (sym b) (pxo<x op))) z ... | tri> ¬a ¬b px<x = ZSupf.supf (prev px (pxo<x op) ) px - supf1 : Ordinal → Ordinal - supf1 z with trio< z px - ... | tri< a ¬b ¬c = ZSupf.supf (prev z (ordtrans a (pxo<x op))) z - ... | tri≈ ¬a b ¬c = ZSupf.supf (prev z (subst (λ k → k o< x ) (sym b) (pxo<x op))) z - ... | tri> ¬a ¬b px<x = & (SUP.sup (zsupf0 A f mf ay supP ax)) + sp1 = & (SUP.sup (zsupf0 A f mf ay supP ? )) zc2 : ZSupf A f mf ay x zc2 with ODC.∋-p O A (* x) ... | no noax = ? - ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain z f ) + ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain0 ? f ) ... | case1 pr = ? - ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax ) + ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain0 ax ) ... | case2 ¬x=sup = ? ... | case1 is-sup = ? @@ -459,6 +436,7 @@ {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where field supf : Ordinal → Ordinal + asupf : {x : Ordinal } → odef A (supf x) chain : HOD chain = UnionCF A f mf ay supf z chain⊆A : chain ⊆' A @@ -469,8 +447,7 @@ → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → 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 - supf-max : {x : Ordinal } → z o< x → supf (osuc z) ≡ supf x - csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) + 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) chain∋init : odef chain y chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ @@ -507,35 +484,6 @@ ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) )) ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt ) - csupf-fc : {b s z1 : Ordinal} → b o≤ z → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 - csupf-fc {b} {s} {z1} b≤z ss<sb (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 = csupf 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 (zc09 u<x ) is-sup fc ⟫ where - zc06 : supf u ≡ u - zc06 = ChainP.supu=u is-sup - zc09 : u o< supf s → u o< b - zc09 u<s = ordtrans (supf-inject (subst (λ k → k o< supf s) (sym zc06) u<s)) s<b - csupf-fc {b} {s} {z1} b<z ss≤sb (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 (csupf-fc b<z ss≤sb fc ) - ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ - ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ - 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 - zc00 : ( * z1 ≡ SUP.sup (sup (o<→≤ b<z) )) ∨ ( * z1 < SUP.sup ( sup (o<→≤ b<z) ) ) - zc00 = SUP.x<sup (sup (o<→≤ b<z) ) (csupf-fc (o<→≤ b<z) ss<sb fc ) - zc04 : (z1 ≡ supf b) ∨ (z1 << supf b) - zc04 with zc00 - ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup (o<→≤ b<z)) ) (cong (&) eq) ) - ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup (o<→≤ b<z) ) ))) lt ) record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where @@ -673,6 +621,9 @@ ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k ) (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc)) ⟫ + + supf1 = ZChain.supf zc + zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x zc1 x prev with Oprev-p x ... | yes op = record { is-max = is-max } where @@ -847,12 +798,6 @@ ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op))) ... | tri> ¬a ¬b c = ? -- ZChain.supf-max zc (o<→≤ c) - supf∈A : {b : Ordinal} → b o≤ x → odef A (supf0 b) - supf∈A {b} b≤z with trio< b px - ... | tri< a ¬b ¬c = proj1 ( ZChain.csupf zc (o<→≤ a )) - ... | tri≈ ¬a b ¬c = proj1 ( ZChain.csupf zc (o≤-refl0 b )) - ... | tri> ¬a ¬b c = ? -- subst (λ k → odef A k ) (ZChain.supf-max zc (o<→≤ c)) ? -- (proj1 ( ZChain.csupf zc o≤-refl)) - supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b supf-mono = ZChain.supf-mono zc @@ -862,6 +807,7 @@ zc02 = ? -- ZChain.supf-max zc (o<→≤ (pxo<x op)) zc01 : supf0 px ≡ supf0 z zc01 = ? -- ZChain.supf-max zc (OrdTrans (o<→≤ (pxo<x op)) z≤x) + zc04 : {b : Ordinal} → b o≤ x → (b o≤ px ) ∨ (b ≡ x ) zc04 {b} b≤x with trio< b px ... | tri< a ¬b ¬c = case1 (o<→≤ a) @@ -878,8 +824,8 @@ -- supf0 px ≡ supf0 x no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f) → ZChain A f mf ay x - no-extension P = record { supf = supf0 ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = ? - ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf } where + no-extension P = record { supf = supf0 ; asupf = ? ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono + ; order = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup fc ⟫ @@ -919,7 +865,7 @@ zc12 : supf0 x ≡ u1 zc12 = subst (λ k → supf0 k ≡ u1) eq (ChainP.supu=u u1-is-sup) zcsup : xSUP (UnionCF A f mf ay supf0 px) x - zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) + zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (ZChain.asupf zc) ; is-sup = record { x<sup = x<sup } } zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 (zc20 fc ) where eq : u1 ≡ x @@ -957,7 +903,7 @@ ... | case1 lt = SUP.x<sup zc32 lt ... | case2 ⟪ spx=px , fc ⟫ = ⊥-elim ( ne spx=px ) zc33 : supf0 z ≡ & (SUP.sup zc32) - zc33 = trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl ) + zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl ) zc36 : ¬ (supf0 px ≡ px) → STMP z≤x zc36 ne = record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 ne } ; tsup=sup = zc33 } zc35 : STMP z≤x @@ -987,12 +933,6 @@ zc31 (case2 hasPrev ) with zc30 ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev ; ay = zc10 (HasPrev.ay hasPrev) ; x=fy = HasPrev.x=fy hasPrev } ) - csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 (supf0 b)) (supf0 b) - csupf {b} b≤x with zc04 b≤x - ... | case2 b=x = subst (λ k → odef (UnionCF A f mf ay supf0 k) k) ? ( ZChain.csupf zc o≤-refl ) where - zc05 : px o≤ b - zc05 = subst (λ k → px o≤ k) (sym b=x) (o<→≤ (pxo<x op) ) - ... | case1 b≤px = ZChain.csupf zc b≤px zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* x) @@ -1002,8 +942,8 @@ ... | case1 pr = no-extension (case2 pr) -- 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 = supf1 ; supf-max = ? - ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!} + record { supf = supf1 + ; sup=u = {!!} ; supf-mono = {!!} ; sup = {!!} ; supf-is-sup = {!!} } where supf1 : Ordinal → Ordinal supf1 z with trio< z px @@ -1050,13 +990,6 @@ zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ? - csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b) - csupf {b} b≤x with zc04 b≤x - ... | case2 b=x = ⟪ ? , ch-is-sup x ? ? (init ? ? ) ⟫ - ... | case1 b≤px with ZChain.csupf zc b≤px - ... | ⟪ au , ch-init fc ⟫ = ⟪ ? , ch-init ? ⟫ - ... | ⟪ au , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ? , ch-is-sup u ? ? ? ⟫ - ... | case2 ¬x=sup = no-extension (case1 nsup) where -- px is not f y' nor sup of former ZChain from y -- no extention nsup : ¬ xSUP (UnionCF A f mf ay supf0 px) x @@ -1119,8 +1052,8 @@ zc70 pr xsup = ? no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x - no-extension ¬sp=x = record { supf = supf1 ; sup=u = sup=u - ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; csupf = csupf } where + no-extension ¬sp=x = record { supf = supf1 ; sup=u = sup=u ; order = ? + ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } 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 pchain0=1 : pchain ≡ pchain1 @@ -1160,15 +1093,6 @@ ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b) (ob<x lim a)) ab {!!} record { x<sup = {!!} } ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?) ?) ab {!!} record { x<sup = {!!} } ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) - csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 (supf1 z)) (supf1 z) - csupf {z} z≤x with trio< z x - ... | tri< a ¬b ¬c = ? where - 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 ) - ... | tri≈ ¬a b ¬c = {!!} - ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x) @@ -1178,7 +1102,7 @@ ... | case1 pr = no-extension {!!} ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax ) ... | case1 is-sup = record { supf = supf1 ; sup=u = {!!} - ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!}; csupf = {!!} } -- where -- x is a sup of (zc ?) + ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!}; asupf = {!!} } -- where -- x is a sup of (zc ?) ... | case2 ¬x=sup = no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A)