Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 755:b22327e78b03
u < osuc x
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Jul 2022 09:42:02 +0900 |
| parents | db177d911091 |
| children | 60a2340e892d |
| files | src/zorn.agda |
| diffstat | 1 files changed, 78 insertions(+), 50 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Jul 23 18:40:35 2022 +0900 +++ b/src/zorn.agda Sun Jul 24 09:42:02 2022 +0900 @@ -270,7 +270,7 @@ 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 ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z - ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x ) ( is-sup : ChainP A f mf ay supf u z) + ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o≤ x ) ( is-sup : ChainP A f mf ay supf u z) ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z ∈∧P→o< : {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A @@ -428,11 +428,11 @@ chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ uaa , ch-is-sup ua u<x is-sup fc ⟫ = - ⟪ uaa , ch-is-sup ua (ordtrans<-≤ u<x a≤b ) is-sup fc ⟫ + ⟪ uaa , ch-is-sup ua (OrdTrans u<x a≤b) is-sup fc ⟫ chain<ZA : {x : Ordinal } → UnionCF A f mf ay (ZChain.supf zc) x ⊆' UnionCF A f mf ay (ZChain.supf zc) (& A) chain<ZA {x} ux with proj2 ux ... | ch-init fc = ⟪ proj1 ux , ch-init fc ⟫ - ... | ch-is-sup u pu<x is-sup fc = ⟪ proj1 ux , ch-is-sup u u<x is-sup fc ⟫ where + ... | ch-is-sup u pu<x is-sup fc = ⟪ proj1 ux , ch-is-sup u (o<→≤ u<x) is-sup fc ⟫ where u<A : (& ( * ( ZChain.supf zc u))) o< & A u<A = c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fcs _ f mf fc) ) u<x : u o< & A @@ -472,14 +472,13 @@ m03 with proj2 ua ... | ch-init fc = ⟪ proj1 ua , ch-init fc ⟫ ... | ch-is-sup u u<x is-sup fc with trio< u px - ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u a is-sup fc ⟫ - ... | tri≈ ¬a u=px ¬c = ? --- supf u < a < b , - ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) - -- = ⟪ proj1 ua , ? ⟫ + ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup fc ⟫ -- u o< osuc x + ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup fc ⟫ + ... | tri> ¬a ¬b c = ? -- u = x m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b m04 = ZChain1.is-max (prev px px<x) m03 b<px ab (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤ (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) o≤-refl lt) } ) a<b - ... | tri≈ ¬a b=px ¬c = ? -- b = px case, u = px u<x + ... | tri≈ ¬a b=px ¬c = ? -- b = px case, u = px u< osuc x ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = fcy<sup ; sup=u = sup=u ; order = order } where fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u fcy<sup {u} {w} u<x fc = ZChain1.fcy<sup (prev (osuc u) (ob<x lim u<x)) <-osuc fc @@ -512,7 +511,7 @@ m06 = record { fcy<sup = m07 ; csupz = subst (λ k → FClosure A f k b ) m05 (init ab) ; order = m08 ; y<s = y<s ; supfu=u = sym m05 } m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b - m04 = ⟪ ab , ch-is-sup b <-osuc m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ + m04 = ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc) m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ --- --- the maximum chain has fix point of any ≤-monotonic function @@ -647,7 +646,7 @@ csupf : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) (supf0 z) csupf {z} with ZChain.csupf zc {z} ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u (ordtrans u<px px<x ) is-sup fc ⟫ + ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u (ordtrans u<px ? ) is-sup fc ⟫ -- if previous chain satisfies maximality, we caan reuse it -- @@ -679,24 +678,70 @@ psupf0 : (z : Ordinal) → Ordinal psupf0 z with trio< z x - ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z - ... | tri≈ ¬a b ¬c = & A - ... | tri> ¬a ¬b c = & A + ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z + ... | tri≈ ¬a b ¬c = & A -- Sup of FClosure A f y z ? + ... | tri> ¬a ¬b c = & A -- + + pchain0 : HOD + pchain0 = UnionCF A f mf ay psupf0 x + + ptotal0 : IsTotalOrderSet pchain0 + ptotal0 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where + uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) + uz01 = chain-total A f mf ay psupf0 ( (proj2 ca)) ( (proj2 cb)) + + + usup : SUP A pchain0 + usup = supP pchain0 (λ lt → proj1 lt) ptotal0 + spu = & (SUP.sup usup) + + psupf : Ordinal → Ordinal + psupf z with trio< z x + ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z + ... | tri≈ ¬a b ¬c = spu + ... | tri> ¬a ¬b c = spu + + psupf>z : {z : Ordinal } → x o< z → spu ≡ psupf z + psupf>z {z} x<z with trio< z x + ... | tri< a ¬b ¬c = ⊥-elim ( ¬c x<z) + ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c x<z) + ... | tri> ¬a ¬b c = refl + + psupf=x : spu ≡ psupf x + psupf=x = zc20 refl where + zc20 : {z : Ordinal } → z ≡ x → spu ≡ psupf x + zc20 {z} z=x with trio< z x | inspect psupf z + ... | tri< a ¬b ¬c | _ = ⊥-elim ( ¬b z=x) + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = subst (λ k → spu ≡ psupf k) b (sym eq1) + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬b z=x) + + csupf :{z : Ordinal} → odef (UnionCF A f mf ay psupf x) (psupf z) + csupf {z} with trio< z x | inspect psupf z + ... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where + ozc = pzc (osuc z) (ob<x lim z<x) + zc12 : odef A (ZChain.supf ozc z) + ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z) + zc12 = ZChain.csupf ozc {z} + zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z) + zc11 with zc12 + ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + ... | ⟪ az , ch-is-sup u u<z is-sup fc ⟫ = ⟪ az , ch-is-sup z (o<→≤ z<x) + zc14 (subst (λ k → FClosure A f k (ZChain.supf ozc z)) (sym eq1) (init az)) ⟫ where + zc14 : ChainP A f mf ay psupf z (ZChain.supf ozc z) + zc14 = ? + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x <-osuc zc15 + (subst (λ k → FClosure A f k spu) zc17 (init (SUP.A∋maximal usup))) ⟫ where + zc15 : ChainP A f mf ay psupf x spu + zc15 = ? + zc17 : spu ≡ psupf x + zc17 = subst (λ k → spu ≡ psupf k ) b (sym eq1) + ... | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x <-osuc zc16 + (subst (λ k → FClosure A f k spu) psupf=x (init (SUP.A∋maximal usup))) ⟫ where + zc16 : ChainP A f mf ay psupf x spu + zc16 = ? pchain : HOD - pchain = UnionCF A f mf ay psupf0 x - - psupf0=pzc : {z : Ordinal} → (z<x : z o< x) → psupf0 z ≡ ZChain.supf (pzc z z<x) z - psupf0=pzc {z} z<x with trio< z x - ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x) - ... | tri> ¬a ¬b c = ⊥-elim (¬a z<x) - ... | tri< a ¬b ¬c with o<-irr z<x a - ... | refl = refl - - ptotal : IsTotalOrderSet pchain - ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where - uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) - uz01 = chain-total A f mf ay psupf0 ( (proj2 ca)) ( (proj2 cb)) + pchain = UnionCF A f mf ay psupf x pchain⊆A : {y : Ordinal} → odef pchain y → odef A y pchain⊆A {y} ny = proj1 ny @@ -707,35 +752,18 @@ pinit {a} ⟪ aa , ua ⟫ with ua ... | ch-init fc = s≤fc y f mf fc ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc) where - zc7 : y << psupf0 ? + zc7 : y << psupf ? zc7 = ChainP.fcy<sup is-sup (init ay) pcy : odef pchain y pcy = ⟪ ay , ch-init (init ay) ⟫ - - usup : SUP A pchain - usup = supP pchain (λ lt → proj1 lt) ptotal - spu = & (SUP.sup usup) - psupf : Ordinal → Ordinal - psupf z with trio< z x - ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z - ... | tri≈ ¬a b ¬c = spu - ... | tri> ¬a ¬b c = spu - - - csupf :{z : Ordinal} → odef (UnionCF A f mf ay psupf x) (psupf z) - csupf {z} with trio< z x - ... | tri< a ¬b ¬c = zc11 where - zc11 : odef A (ZChain.supf (pzc z a) z) ∧ UChain A f mf ay psupf x (ZChain.supf (pzc z a) z) - zc11 with ZChain.csupf (pzc z a) {z} - ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - ... | ⟪ az , ch-is-sup u u<z is-sup fc ⟫ = ⟪ az , ch-is-sup u (ordtrans u<z a) ? (pfc a fc) ⟫ - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? + ptotal : IsTotalOrderSet pchain + ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where + uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) + uz01 = chain-total A f mf ay psupf ( (proj2 ca)) ( (proj2 cb)) no-extension : ZChain A f mf ay x - no-extension = record { initial = ? ; chain∋init = ? ; supf = psupf ; csupf = ? - ; chain⊆A = ? ; f-next = ? ; f-total = ? } - + no-extension = record { initial = pinit ; chain∋init = pcy ; supf = psupf ; csupf = csupf + ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } zc5 : ZChain A f mf ay x zc5 with ODC.∋-p O A (* x)