Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 958:33891adf80ea
IsMinSup contains not HasPrev
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 04 Nov 2022 06:47:23 +0900 |
| parents | ce42b1c5cf42 |
| children | 1ef03eedd148 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 32 insertions(+), 50 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Nov 03 19:01:54 2022 +0900 +++ b/src/zorn.agda Fri Nov 04 06:47:23 2022 +0900 @@ -233,7 +233,7 @@ -- tree structure -- -record HasPrev (A B : HOD) (x : Ordinal ) ( f : Ordinal → Ordinal ) : Set n where +record HasPrev (A B : HOD) ( f : Ordinal → Ordinal ) (x : Ordinal ) : Set n where field ax : odef A x y : Ordinal @@ -244,11 +244,12 @@ -- field -- x≤sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -record IsMinSup (A B : HOD) {x : Ordinal } (xa : odef A x) : Set n where +record IsMinSup (A B : HOD) ( f : Ordinal → Ordinal ) {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 + not-hp : ¬ ( HasPrev A B f x ) record SUP ( A B : HOD ) : Set (Level.suc n) where field @@ -408,7 +409,7 @@ field supf : Ordinal → Ordinal sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z - → IsMinSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b + → IsMinSup A (UnionCF A f mf ay supf b) f ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b asupf : {x : Ordinal } → odef A (supf x) supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y @@ -469,37 +470,18 @@ -- ordering is not proved here but in ZChain1 - IsSup< : {b x : Ordinal } (ab : odef A b ) - → b o< x - → IsMinSup A (UnionCF A f mf ay supf x) ab → IsMinSup A (UnionCF A f mf ay supf b) ab - IsSup< {b} {x} ab b<x is-sup = record { - x≤sup = λ {z} uz → IsMinSup.x≤sup is-sup (chain-mono f mf ay supf supf-mono (o<→≤ b<x) uz) - ; minsup = m07 } where - m10 : {s : Ordinal } → (odef A s ) - → ( {w : Ordinal} → odef (UnionCF A f mf ay supf b) w → (w ≡ s) ∨ (w << s) ) - → {w : Ordinal} → odef (UnionCF A f mf ay supf x) w → (w ≡ s) ∨ (w << s) - m10 {s} as b-is-sup ⟪ aa , ch-init fc ⟫ = ? - m10 {s} as b-is-sup ⟪ aa , ch-is-sup u {w} u<x is-sup-z fc ⟫ = m01 where - m01 : w <= s - m01 with trio< (supf u) (supf b) - ... | tri< a ¬b ¬c = b-is-sup ⟪ aa , ch-is-sup u {w} a is-sup-z fc ⟫ - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? - -- <=-trans (IsMinSup.x≤sup is-sup ⟪ aa , ch-is-sup u u<x is-sup-z fc ⟫) b<=s - m07 : {s : Ordinal} → odef A s → ({z : Ordinal} → - odef (UnionCF A f mf ay supf b) z → (z ≡ s) ∨ (z << s)) → b o≤ s - m07 {s} as b-is-sup = IsMinSup.minsup is-sup as (m10 as b-is-sup ) + -- b o< x → IsMinSup A (UnionCF A f mf ay supf x) ab → IsMinSup A (UnionCF A f mf ay supf b) ab + -- is not valid without ¬ HasPrev 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 supf = ZChain.supf zc field is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → supf b o< supf z → (ab : odef A b) - → HasPrev A (UnionCF A f mf ay supf z) b f ∨ IsMinSup A (UnionCF A f mf ay supf b) ab + → HasPrev A (UnionCF A f mf ay supf z) f b ∨ IsMinSup A (UnionCF A f mf ay supf b) f ab → * a < * b → odef ((UnionCF A f mf ay supf z)) b order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) - record Maximal ( A : HOD ) : Set (Level.suc n) where field maximal : HOD @@ -621,7 +603,7 @@ → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c chain-mono1 {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (ab : odef A b) - → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f + → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) f b → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ @@ -671,7 +653,7 @@ zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt ) is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → - HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsMinSup A (UnionCF A f mf ay supf b) ab → + HasPrev A (UnionCF A f mf ay supf x) f b ∨ IsMinSup A (UnionCF A f mf ay supf b) f ab → * a < * b → odef (UnionCF A f mf ay supf x) b is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b @@ -681,12 +663,12 @@ b<A = z09 ab b<x : b o< x b<x = ZChain.supf-inject zc sb<sx - m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f + m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = 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 → IsMinSup.x≤sup (proj2 is-sup) ? -- (chain-mono1 (o<→≤ b<x) uz) + ⟪ record { x≤sup = λ {z} uz → IsMinSup.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) ) @@ -705,7 +687,7 @@ ... | no lim = record { is-max = is-max ; order = order } where is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) → - HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsMinSup A (UnionCF A f mf ay supf b) ab → + HasPrev A (UnionCF A f mf ay supf x) f b ∨ IsMinSup A (UnionCF A f mf ay supf b) f ab → * a < * b → odef (UnionCF A f mf ay supf x) b is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b @@ -721,7 +703,7 @@ 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 = order m09 s<b fc - m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f + m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) @@ -749,10 +731,10 @@ SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x≤sup = λ lt → SUP.x≤sup sup (B⊆C lt) } - record xSUP (B : HOD) (x : Ordinal) : Set n where + record xSUP (B : HOD) (f : Ordinal → Ordinal ) (x : Ordinal) : Set n where field ax : odef A x - is-sup : IsMinSup A B ax + is-sup : IsMinSup A B f ax -- -- create all ZChains under o< x @@ -1151,7 +1133,7 @@ zc111 {z} z<px ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ zc111 {z} z<px ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ? ? ⟫ - zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ (HasPrev A pchain x f ) + zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) f x ) ∨ (HasPrev A pchain f x ) → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z ) zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px @@ -1185,7 +1167,7 @@ ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ? zc12 : supf0 x ≡ u1 zc12 = subst (λ k → supf0 k ≡ u1) eq ? - zcsup : xSUP (UnionCF A f mf ay supf0 px) x + zcsup : xSUP (UnionCF A f mf ay supf0 px) f x zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (ZChain.asupf zc) ; 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 @@ -1237,7 +1219,7 @@ zc37 : MinSUP A (UnionCF A f mf ay supf0 z) zc37 = record { sup = ? ; asm = ? ; x≤sup = ? } sup=u : {b : Ordinal} (ab : odef A b) → - b o≤ x → IsMinSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b + b o≤ x → IsMinSup A (UnionCF A f mf ay supf0 b) supf0 ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) f b ) → 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 → IsMinSup.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 → IsMinSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ @@ -1246,11 +1228,11 @@ zc30 with osuc-≡< b≤x ... | case1 eq = sym (eq) ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) - zcsup : xSUP (UnionCF A f mf ay supf0 px) x + zcsup : xSUP (UnionCF A f mf ay supf0 px) supf0 x zcsup with zc30 ... | refl = record { ax = ab ; is-sup = record { x≤sup = λ {w} lt → IsMinSup.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 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) supf0 x ) ∨ HasPrev A (UnionCF A f mf ay supf0 px) f x ) → supf0 b ≡ b zc31 (case1 ¬sp=x) with zc30 ... | refl = ⊥-elim (¬sp=x zcsup ) zc31 (case2 hasPrev ) with zc30 @@ -1293,7 +1275,7 @@ is-max-hp : (supf : Ordinal → Ordinal) (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a → b o< x → (ab : odef A b) → - HasPrev A (UnionCF A f mf ay supf x) b f → + HasPrev A (UnionCF A f mf ay supf x) f b → * a < * b → odef (UnionCF A f mf ay supf x) b is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ @@ -1301,10 +1283,10 @@ -- subst (λ k → UChain A f mf ay supf x k ) -- (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc)) ⟫ - zc70 : HasPrev A pchain x f → ¬ xSUP pchain x + zc70 : HasPrev A pchain f x → ¬ xSUP pchain f x zc70 pr xsup = ? - no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x + no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) supf0 x ) → ZChain A f mf ay x no-extension ¬sp=x = ? where -- record { supf = supf1 ; sup=u = sup=u -- ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } where supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal @@ -1341,7 +1323,7 @@ zc8 = ZChain.supf-is-minsup (pzc z a) {!!} ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) - sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsMinSup A (UnionCF A f mf ay supf1 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) b f ) → supf1 b ≡ b + sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsMinSup A (UnionCF A f mf ay supf1 b) f ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) f b ) → supf1 b ≡ b sup=u {z} ab z≤x is-sup with trio< z x ... | 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 = {!!} } @@ -1350,10 +1332,10 @@ zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x) ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip - ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain x f ) + ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain f x ) -- we have to check adding x preserve is-max ZChain A y f mf x ... | case1 pr = no-extension {!!} - ... | case2 ¬fy<x with ODC.p∨¬p O (IsMinSup A pchain ax ) + ... | case2 ¬fy<x with ODC.p∨¬p O (IsMinSup A pchain f ax ) ... | case1 is-sup = ? -- record { supf = supf1 ; sup=u = {!!} -- ; 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 @@ -1391,7 +1373,7 @@ asp : odef A sp asp = SUP.as sp1 z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) - → HasPrev A chain b f ∨ IsMinSup A (UnionCF A f mf ab (ZChain.supf zc) b) ab + → HasPrev A chain f b ∨ IsMinSup A (UnionCF A f mf ab (ZChain.supf zc) b) f ab → * a < * b → odef chain b z10 = ? -- ZChain1.is-max (SZ1 f mf as0 zc (& A) ) z22 : sp o< & A @@ -1407,7 +1389,7 @@ z13 with x≤sup ( ZChain.chain∋init zc ) ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt - z19 : IsMinSup A (UnionCF A f mf as0 (ZChain.supf zc) sp) asp + z19 : IsMinSup A (UnionCF A f mf as0 (ZChain.supf zc) sp) f asp z19 = record { x≤sup = ? ; 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) @@ -1537,10 +1519,10 @@ 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 : IsMinSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1) + is-sup : IsMinSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (cf nmx) (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 ) ; minsup = ? } - not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) mc (cf nmx) + not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (cf nmx) mc 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) z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) @@ -1557,7 +1539,7 @@ z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc _ fc ))) - is-sup : IsMinSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd) + is-sup : IsMinSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (cf nmx) (MinSUP.asm spd) 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 @@ -1589,7 +1571,7 @@ -- u<x : ZChain.supf zc u o< ZChain.supf zc d -- supf u o< spuf c → order - not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) d (cf nmx) + not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) (cf nmx) d not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ⊥-elim ( <-irr z31 z30 ) where z30 : * d < * (cf nmx d) z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd))