Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 764:bbf12d61143f
< is wrong
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 25 Jul 2022 17:53:18 +0900 |
| parents | 9aa0fc917100 |
| children | 7fff07748fde |
| files | src/zorn.agda |
| diffstat | 1 files changed, 43 insertions(+), 40 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Jul 25 16:36:36 2022 +0900 +++ b/src/zorn.agda Mon Jul 25 17:53:18 2022 +0900 @@ -269,7 +269,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 } ( 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 @@ -319,21 +319,21 @@ chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a) ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb - ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub ub<x supb fcb) = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where + ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub supb fcb) = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where ct00 : * a < * (supf ub) ct00 = ChainP.fcy<sup supb fca ct01 : * a < * b ct01 with s≤fc (supf ub) f mf fcb ... | case1 eq = subst (λ k → * a < 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-init fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where + ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-init fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where ct00 : * b < * (supf ua) ct00 = ChainP.fcy<sup supa fcb ct01 : * b < * a ct01 with s≤fc (supf ua) f mf fca ... | 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 + ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) with trio< ua ub ... | tri< a₁ ¬b ¬c = tri< ct02 (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt) where ct03 : * a < * (supf ub) ct03 = ChainP.order supb a₁ (ChainP.csupz supa) @@ -428,33 +428,27 @@ odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c 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 ⟫ + chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ uaa , ch-is-sup ua is-sup fc ⟫ = + ⟪ uaa , ch-is-sup ua 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 (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 - u≤x = subst (λ k → k o< & A ) (trans &iso (ChainP.supfu=u is-sup)) u<A + ... | ch-is-sup u is-sup fc = ⟪ proj1 ux , ch-is-sup u is-sup fc ⟫ 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 → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b is-max-hp 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 )) ⟫ - ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , + ... | ⟪ ab0 , ch-is-sup u 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 (ChainP-next A f mf ay _ is-sup) (fsuc _ fc)) ⟫ + (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u (ChainP-next A f mf ay _ is-sup) (fsuc _ fc)) ⟫ 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 px = Oprev.oprev op 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 - -- 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 = ? is-max : {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 ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab → @@ -472,9 +466,9 @@ m03 : odef (UnionCF A f mf ay (ZChain.supf zc) px) a -- if a ∈ chain of px, is-max of px can be used m03 with proj2 ua ... | ch-init fc = ⟪ proj1 ua , ch-init fc ⟫ - ... | ch-is-sup u u≤x is-sup-a fc with trio< u px - ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup-a fc ⟫ -- u o< osuc x - ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup-a fc ⟫ + ... | ch-is-sup u is-sup-a fc with trio< u px + ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u is-sup-a fc ⟫ -- u o< osuc x + ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u is-sup-a fc ⟫ ... | tri> ¬a ¬b c = ⊥-elim (<-irr u≤a (ptrans a<b b<u) ) where -- a and b is a sup of chain, order forces minimulity of sup su=u : ZChain.supf zc u ≡ u @@ -493,7 +487,7 @@ 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 = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ where + ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ where b<A : b o< & A b<A = z09 ab m05 : b ≡ ZChain.supf zc b @@ -529,7 +523,7 @@ m06 = record { fcy<sup = m07 ; csupz = subst (λ k → FClosure A f k b ) m05 (init ab) ; order = m08 ; supfu=u = sym m05 } m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b - m04 = ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc) m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ + m04 = ⟪ ab , ch-is-sup b m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ --- --- the maximum chain has fix point of any ≤-monotonic function @@ -611,8 +605,12 @@ 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 ; csupf = ? ; fcy<sup = ? ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where + spi = & (SUP.sup (ysup f mf ay)) isupf : Ordinal → Ordinal - isupf z = & (SUP.sup (ysup f mf ay)) + isupf z with trio< z spi + ... | tri< a ¬b ¬c = y + ... | tri≈ ¬a b ¬c = spi + ... | tri> ¬a ¬b c = spi sp = ysup f mf ay cy : odef (UnionCF A f mf ay isupf o∅) y cy = ⟪ ay , ch-init (init ay) ⟫ @@ -621,24 +619,29 @@ isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z isy {z} ⟪ az , uz ⟫ with uz ... | ch-init fc = s≤fc y f mf fc - ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup) (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc) + ... | ch-is-sup u is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup) (s≤fc (& (SUP.sup (ysup f mf ay))) f mf ? ) inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a) inext {a} ua with (proj2 ua) ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-init (fsuc _ fc ) ⟫ - ... | ch-is-sup u u≤x is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-is-sup u u≤x (ChainP-next A f mf ay isupf is-sup) (fsuc _ fc) ⟫ + ... | ch-is-sup u is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) , ch-is-sup u (ChainP-next A f mf ay isupf is-sup) (fsuc _ fc) ⟫ itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) itotal {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 isupf (proj2 ca) (proj2 cb) csupf : {z : Ordinal} → odef (UnionCF A f mf ay isupf o∅) (isupf z) - csupf {z} = ⟪ SUP.A∋maximal sp , ch-is-sup o∅ o≤-refl uz02 (init ( SUP.A∋maximal sp)) ⟫ where - uz02 : ChainP A f mf ay isupf o∅ (isupf z) - uz02 = record { csupz = init (SUP.A∋maximal sp) ; supfu=u = ? ; fcy<sup = ? ; order = ? } - uz03 : {z : Ordinal} → FClosure A f y z → z << isupf o∅ - uz03 = ? - uz04 : {sup1 z1 : Ordinal} → sup1 o< o∅ → FClosure A f (isupf sup1) z1 → z1 << isupf o∅ - uz04 = ? + csupf {z} with trio< z spi + ... | tri< a ¬b ¬c = ⟪ ay , ch-init (init ay ) ⟫ + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = ⟪ SUP.A∋maximal sp , ch-is-sup spi ? ? ⟫ where + uz03 : {z : Ordinal} → FClosure A f y z → z << isupf spi + uz03 {z} fcz with SUP.x<sup sp (subst (λ k → FClosure A f y k) (sym &iso) fcz) + ... | case2 lt = ? -- subst (λ k → * z < k ) (sym *iso) lt + ... | case1 eq = ? -- ⊥-elim (<-irr (case1 e) + uz04 : {sup1 z1 : Ordinal} → sup1 o< spi → FClosure A f (isupf sup1) z1 → z1 << isupf spi + uz04 {_} {z} _ fcz = ? + uz02 : ChainP A f mf ay isupf spi spi + uz02 = ? -- record { csupz = init (SUP.A∋maximal sp) ; supfu=u = refl ; fcy<sup = uz03 ; order = uz04 } -- -- create all ZChains under o< x @@ -669,11 +672,11 @@ pchain⊆A {y} ny = proj1 ny pnext : {a : Ordinal} → odef pchain a → odef pchain (f a) pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc) ⟫ - pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc ) ⟫ + pnext {a} ⟪ aa , ch-is-sup u is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc ) ⟫ pinit : {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁ 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 + ... | ch-is-sup u is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc) where zc7 : y << (ZChain.supf zc) u zc7 = ChainP.fcy<sup is-sup (init ay) pcy : odef pchain y @@ -684,7 +687,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 (o<→≤ px<x)) is-sup fc ⟫ + ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , ch-is-sup u is-sup fc ⟫ -- if previous chain satisfies maximality, we caan reuse it -- @@ -764,17 +767,17 @@ 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) + ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , ch-is-sup z 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 + ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x 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 + ... | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x 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 = ? @@ -786,11 +789,11 @@ pchain⊆A {y} ny = proj1 ny pnext : {a : Ordinal} → odef pchain a → odef pchain (f a) pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫ - pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-is-sup u u≤x (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) ⟫ + pnext {a} ⟪ aa , ch-is-sup u is-sup fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-is-sup u (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) ⟫ pinit : {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁ 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 + ... | ch-is-sup u is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc) where zc7 : y << psupf _ zc7 = ChainP.fcy<sup is-sup (init ay) pcy : odef pchain y @@ -806,9 +809,9 @@ * 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 )) ⟫ - ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , + ... | ⟪ ab0 , ch-is-sup u is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay supf x k ) - (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x (ChainP-next A f mf ay _ is-sup) (fsuc _ fc)) ⟫ + (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u (ChainP-next A f mf ay _ is-sup) (fsuc _ fc)) ⟫ no-extension : ZChain A f mf ay x no-extension = record { initial = pinit ; chain∋init = pcy ; supf = psupf ; csupf = csupf ; sup=u = ? ; order = ? ; fcy<sup = ?