Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1482:4f597bc6b3d6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
zorn fixed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 30 Jun 2024 16:07:58 +0900
parents 42df464988e8
children 2435deeecda9
files src/zorn.agda
diffstat 1 files changed, 15 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Jun 30 13:05:00 2024 +0900
+++ b/src/zorn.agda	Sun Jun 30 16:07:58 2024 +0900
@@ -560,7 +560,7 @@
     → o∅ o< & A
     → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
     → Maximal A
-Zorn-lemma {A}  0<A supP = ? where
+Zorn-lemma {A}  0<A supP = zorn00 where
      z07 :   {y : Ordinal} {A : HOD } → {P : Set n} → odef A y ∧ P → y o< & A
      z07 {y} {A} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
      s : HOD
@@ -1287,7 +1287,7 @@
 
           sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc  (ob<x lim a)) z
           sf1=sf {z} z<x with trio< z x
-          ... | tri< a ¬b ¬c = ? -- cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr
+          ... | tri< a ¬b ¬c = cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr
           ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x)
           ... | tri> ¬a ¬b c = ⊥-elim (¬a z<x)
 
@@ -1388,11 +1388,9 @@
                m<x : m o< x
                m<x with trio< a sa 
                ... | tri< a<sa ¬b ¬c = ob<x lim (ordtrans<-≤ sa<b b≤x )
-               ... | tri≈ ¬a a=sa ¬c = subst (λ k → k o< x) ? zc41 where
-                   zc41 : omax a sa o< x
+               ... | tri≈ ¬a a=sa ¬c = zc41 where 
+                   zc41 : osuc a o< x
                    zc41 = osucprev ( begin
-                       osuc ( omax a sa ) ≡⟨ cong (λ k → osuc (omax a k)) (sym a=sa) ⟩
-                       osuc ( omax a a ) ≡⟨ cong osuc (omxx _) ⟩
                        osuc ( osuc  a ) ≤⟨ o<→≤ (ob<x lim (ob<x lim a<x))  ⟩
                        x ∎ ) where open o≤-Reasoning O
                ... | tri> ¬a ¬b c = ob<x lim a<x
@@ -1476,7 +1474,6 @@
                    z48 = ⟪  proj2 (mf _ (MinSUP.as usup) ) , ic-isup _ (subst (λ k → k o< x) refl spu<x) z50
                         (fsuc _ (init (ZChain.asupf (pzc (ob<x lim spu<x))) z49)) ⟫
 
-
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
@@ -1529,16 +1526,16 @@
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
                z16 with proj1 (mf (( MinSUP.sup sp1)) ( MinSUP.as sp1 ))
-               ... | case1 eq = ⊥-elim (¬b (sym ? ))
-               ... | case2 lt = ⊥-elim (¬c ? )
-           ... | tri≈ ¬a b ¬c = ? -- subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) b )
+               ... | case1 eq = ⊥-elim (¬b (sym (trans &iso (trans eq (sym &iso) ))))
+               ... | case2 lt = ⊥-elim (¬c (<-cong (==-sym *iso) (==-sym *iso) lt) )
+           ... | tri≈ ¬a b ¬c = trans (sym &iso) (trans b &iso )
            ... | tri> ¬a ¬b c = ⊥-elim z17 where
                z15 : (f sp ≡ MinSUP.sup sp1) ∨ (* (f sp) < * (MinSUP.sup sp1) )
                z15  = MinSUP.x≤sup sp1 (ZChain.f-next zc z12 )
                z17 : ⊥
                z17 with z15
-               ... | case1 eq = ¬b ?
-               ... | case2 lt = ¬a ?
+               ... | case1 eq = ¬b (trans &iso (trans eq (sym &iso)))
+               ... | case2 lt = ¬a (<-cong (==-sym *iso) (==-sym *iso) lt )
 
      -- ZChain contradicts ¬ Maximal
      --
@@ -1548,11 +1545,10 @@
 
      ¬Maximal→¬cf-mono :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-<-monotonic nmx) as (& A)) → ⊥
      ¬Maximal→¬cf-mono nmx zc = <-irr  {cf nmx c} {c}
-           ? -- (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.as  msp1 ))))
-           ? -- (subst (λ k → odef A k) (sym &iso) (MinSUP.as msp1) )
-           -- (case1 ( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) (cf-is-<-monotonic nmx ) zc msp1 ) -- x ≡ f x ̄
-           --     (proj1 (cf-is-<-monotonic nmx c (MinSUP.as msp1))))  where          -- x < f x
-             where
+           -- (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.as  msp1 ))))
+           -- (subst (λ k → odef A k) (sym &iso) (MinSUP.as msp1) )
+           (case1 ( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) (cf-is-<-monotonic nmx ) zc msp1 )) -- x ≡ f x ̄
+           (proj1 (cf-is-<-monotonic nmx c (MinSUP.as msp1)))  where          -- x < f x
           supf = ZChain.supf zc
           msp1 : MinSUP A (ZChain.chain zc)
           msp1 = msp0 (cf nmx) (cf-is-<-monotonic nmx) as zc
@@ -1568,13 +1564,13 @@
          zorn01 :  A ∋ minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq))
          zorn01  = proj1  zorn03
          zorn02 : {x : HOD} → A ∋ x → ¬ (minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
-         zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) ? ? m<x )
+         zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (<-cong (==-sym *iso) (==-sym *iso) m<x )
      ... | yes ¬Maximal = ⊥-elim ( ¬Maximal→¬cf-mono nmx (SZ (cf nmx) (cf-is-<-monotonic nmx) as (& A) )) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y))
-              zc5 = ⟪  Maximal.as mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) ? mx<y) ) ⟫
+              zc5 = ⟪  Maximal.as mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (<-cong *iso ==-refl mx<y) ) ⟫
 
 -- usage (see filter.agda )
 --