Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 631:1150b006059b
... give up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 20 Jun 2022 18:46:43 +0900 |
| parents | d5cd551e0ed9 |
| children | 1b57a07d7604 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 25 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Jun 20 17:39:28 2022 +0900 +++ b/src/zorn.agda Mon Jun 20 18:46:43 2022 +0900 @@ -339,8 +339,9 @@ --- the maximum chain has fix point of any ≤-monotonic function --- fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (& A) ) + → ( {x y : Ordinal} → x o≤ (& A) → IsTotalOrderSet (ZChain.chain zc) ) → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc )) - fixpoint f mf zc = z14 where + fixpoint f mf zc total = z14 where chain = ZChain.chain zc sp1 = sp0 f mf zc z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) @@ -366,31 +367,30 @@ ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ? (SUP.x<sup sp1 ? ) } z14 : f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc)) - z14 = {!!} - -- with ZChain.f-total zc {& A} {& A} o≤-refl (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 - -- ... | tri< a ¬b ¬c = ⊥-elim z16 where - -- z16 : ⊥ - -- z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 )) - -- ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) )) - -- ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt )) - -- ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b ) - -- ... | tri> ¬a ¬b c = ⊥-elim z17 where - -- z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) - -- z15 = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) - -- z17 : ⊥ - -- z17 with z15 - -- ... | case1 eq = ¬b eq - -- ... | case2 lt = ¬a lt + z14 with total {& A} {& A} o≤-refl (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 + ... | tri< a ¬b ¬c = ⊥-elim z16 where + z16 : ⊥ + z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 )) + ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) )) + ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt )) + ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b ) + ... | tri> ¬a ¬b c = ⊥-elim z17 where + z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) + z15 = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) + z17 : ⊥ + z17 with z15 + ... | case1 eq = ¬b eq + ... | case2 lt = ¬a lt -- ZChain contradicts ¬ Maximal -- -- ZChain forces fix point on any ≤-monotonic function (fixpoint) -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain -- - z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx) (& A)) → ⊥ - z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal sp1)))) + z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx) (& A)) → ({x y : Ordinal} → x o≤ & A → IsTotalOrderSet (ZChain.chain zc)) → ⊥ + z04 nmx zc total = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal sp1)))) (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) ) - (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) -- x ≡ f x ̄ + (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc total ))) -- x ≡ f x ̄ (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where -- x < f x sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc c = & (SUP.sup sp1) @@ -538,6 +538,11 @@ 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 @@ -603,11 +608,6 @@ z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc ) ... | case1 y=b = subst (λ k → odef chain0 k ) y=b ( ZChain.chain∋x zc ) ... | case2 y<b = ZChain.is-max zc (ZChain.chain∋x zc ) (zc-b<x b b<x) ab (case2 (z24 p)) y<b - 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 seq : schain ≡ supf0 x seq with trio< x x ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) @@ -722,7 +722,7 @@ zorn01 = proj1 zorn03 zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x) zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x ) - ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04) where + ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04 {!!} ) where -- if we have no maximal, make ZChain, which contradict SUP condition nmx : ¬ Maximal A nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where