Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 698:3837fa940cd9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 12 Jul 2022 15:29:41 +0900 |
| parents | 96184d542e20 |
| children | 4df0b36db305 0278f0d151f2 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 35 insertions(+), 101 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Tue Jul 12 09:56:18 2022 +0900 +++ b/src/zorn.agda Tue Jul 12 15:29:41 2022 +0900 @@ -344,6 +344,11 @@ ... | case1 eq = subst (λ k → * b < k ) eq ct05 ... | case2 lt = IsStrictPartialOrder.trans POO ct05 lt +ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) + → {x z : Ordinal } → ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z ) +ChainP-next A f mf {y} ay supf {x} {z} cp = record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp + ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp } + Zorn-lemma : { A : HOD } → o∅ o< & A → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B ) -- SUP condition @@ -579,111 +584,40 @@ ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr)) ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax ) ... | case1 is-sup = -- x is a sup of zc - record { chain⊆A = pchain⊆A ; f-next = {!!} ; f-total = {!!} - ; initial = {!!} ; chain∋init = {!!} ; is-max = {!!} } where - sup0 : SUP A (ZChain.chain zc ) - sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where - x21 : {y : HOD} → ZChain.chain zc ∋ y → (y ≡ * x) ∨ (y < * x) - x21 {y} zy with IsSup.x<sup is-sup zy - ... | case1 y=x = case1 ( subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x) ) - ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x ) - sp : HOD - sp = SUP.sup sup0 - x=sup : x ≡ & sp - x=sup = sym &iso + record { chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal + ; initial = pinit ; chain∋init = pcy ; is-max = p-ismax } where pchain : HOD pchain = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A) + psupf = ZChain1.supf (zc0 (& A)) pchain⊆A : {y : Ordinal} → odef pchain y → odef A y pchain⊆A {y} ny = proj1 ny - - -- odef A z ∧ UChain A f mf ay (ZChain1.supf (zc0 (& A))) (& A) z - chain0 = ZChain.chain zc - -- ≡ odef chain0 z ∨ FClosure A f (& sp) z - sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A - sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A zc (subst (λ k → odef chain0 k) (sym &iso) zx ))) - sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) ) - schain : HOD - schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy } - supf0 : Ordinal → HOD - supf0 z with trio< z x - ... | tri< a ¬b ¬c = {!!} -- supf z - ... | tri≈ ¬a b ¬c = schain - ... | tri> ¬a ¬b c = schain - A∋schain : {x : HOD } → schain ∋ x → A ∋ x - A∋schain (case1 zx ) = ZChain.chain⊆A zc zx - A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx - s⊆A : schain ⊆' A - s⊆A {x} (case1 zx) = ZChain.chain⊆A zc zx - s⊆A {x} (case2 fx) = A∋fc (& sp) f mf fx - cmp : {a b : HOD} (za : odef chain0 (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a ) - cmp {a} {b} za fb with SUP.x<sup sup0 za | s≤fc (& sp) f mf fb - ... | case1 sp=a | case1 sp=b = tri≈ (λ lt → <-irr (case1 (sym eq)) lt ) eq (λ lt → <-irr (case1 eq) lt ) where - eq : a ≡ b - eq = trans sp=a (subst₂ (λ j k → j ≡ k ) *iso *iso sp=b ) - ... | case1 sp=a | case2 sp<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b) lt ) where - a<b : a < b - a<b = subst (λ k → k < b ) (sym sp=a) (subst₂ (λ j k → j < k ) *iso *iso sp<b ) - ... | case2 a<sp | case1 sp=b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b) lt ) where - a<b : a < b - a<b = subst (λ k → a < k ) (trans sp=b *iso ) (subst (λ k → a < k ) (sym *iso) a<sp ) - ... | case2 a<sp | case2 sp<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b) lt ) where - a<b : a < b - a<b = ptrans (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b ) - scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a ) - scmp {a} {b} (case1 za) (case1 zb) = {!!} -- ZChain.f-total zc {px} {px} o≤-refl za zb - scmp {a} {b} (case1 za) (case2 fb) = cmp za fb - scmp (case2 fa) (case1 zb) with cmp zb fa - ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq)) a - ... | tri≈ ¬a b ¬c = tri≈ ¬c (sym b) ¬a - ... | tri> ¬a ¬b c = tri< c (λ eq → ¬b (sym eq)) ¬a - scmp (case2 fa) (case2 fb) = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp (& sp) f mf fa fb) - scnext : {a : Ordinal} → odef schain a → odef schain (f a) - scnext {x} (case1 zx) = case1 (ZChain.f-next zc zx) - scnext {x} (case2 sx) = case2 ( fsuc x sx ) - scinit : {x : Ordinal} → odef schain x → * y ≤ * x - scinit {x} (case1 zx) = ZChain.initial zc zx - scinit {x} (case2 sx) with (s≤fc (& sp) f mf sx ) | SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋init zc ) ) - ... | case1 sp=x | case1 y=sp = case1 (trans y=sp (subst (λ k → k ≡ * x ) *iso sp=x ) ) - ... | case1 sp=x | case2 y<sp = case2 (subst (λ k → * y < k ) (trans (sym *iso) sp=x) y<sp ) - ... | case2 sp<x | case1 y=sp = case2 (subst (λ k → k < * x ) (trans *iso (sym y=sp )) sp<x ) - ... | case2 sp<x | case2 y<sp = case2 (ptrans y<sp (subst (λ k → k < * x ) *iso sp<x) ) - A∋za : {a : Ordinal } → odef chain0 a → odef A a - A∋za za = ZChain.chain⊆A zc za - za<sup : {a : Ordinal } → odef chain0 a → ( * a ≡ sp ) ∨ ( * a < sp ) - za<sup za = SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) za ) - s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ab : odef A b) - → HasPrev A schain ab f ∨ IsSup A schain ab - → * a < * b → odef schain b - s-ismax {a} {b} sa b<ox ab p a<b with osuc-≡< b<ox -- b is x? - ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) )) - s-ismax {a} {b} (case1 za) b<ox ab (case1 p) a<b | case2 b<x = z21 p where -- has previous - z21 : HasPrev A schain ab f → odef schain b - z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } = - case1 (ZChain.is-max zc za {!!} ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b ) - z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) ) - s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max zc za {!!} ab (case2 z22) a<b ) where -- previous sup - z22 : IsSup A (ZChain.chain zc ) ab - z22 = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) } - s-ismax {a} {b} (case2 sa) b<ox ab (case1 p) a<b | case2 b<x with HasPrev.ay p - ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc zy )) -- in previous closure of f - ... | case2 sy = case2 (subst (λ k → FClosure A f (& (* x)) k ) (sym (HasPrev.x=fy p)) (fsuc (HasPrev.y p) sy )) -- in current closure of f - s-ismax {a} {b} (case2 sa) b<ox ab (case2 p) a<b | case2 b<x = case1 z23 where -- sup o< x is already in zc - z24 : IsSup A schain ab → IsSup A (ZChain.chain zc ) ab - z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) } - z23 : odef chain0 b - z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋init zc ) - ... | case1 y=b = subst (λ k → odef chain0 k ) y=b ( ZChain.chain∋init zc ) - ... | case2 y<b = ZChain.is-max zc (ZChain.chain∋init zc ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b - seq : schain ≡ supf0 x - seq with trio< x x - ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) - ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b c = refl - seq<x : {b : Ordinal } → b o< x → {!!} -- supf b ≡ supf0 b - seq<x {b} b<x with trio< b x - ... | tri< a ¬b ¬c = refl - ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) - ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) + pnext : {a : Ordinal} → odef pchain a → odef pchain (f a) + pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = fua } ⟫ where + afa : odef A ( f a ) + afa = proj2 ( mf a aa ) + fua : Chain A f mf ay psupf (UChain.u ua) (f a) + fua with UChain.chain∋z ua + ... | ch-init a fc = ch-init (f a) ( fsuc _ fc ) + ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) + ptotal : {a b : HOD } → odef pchain (& a) → odef pchain (& b) + → Tri ( a < b) ( a ≡ b) ( b < a ) + 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 _ (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) + pinit : {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁ + pinit {a} ⟪ aa , ua ⟫ with UChain.chain∋z ua + ... | ch-init a fc = s≤fc y f mf fc + ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc) where + zc7 : y << psupf (UChain.u ua) + zc7 = ChainP.fcy<sup is-sup (init ay) + pcy : odef pchain y + pcy = ⟪ ay , record { u = y ; u<x = ∈∧P→o< ⟪ ay , lift true ⟫ ; chain∋z = ch-init _ (init ay) } ⟫ + p-ismax : {a b : Ordinal} → odef pchain a → + b o< osuc x → (ab : odef A b) → + ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) → + * a < * b → odef pchain b + p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ? + p-ismax {a} {b} ua b<ox ab (case2 sup) a<b = ? ... | case2 ¬x=sup = no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention z18 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →