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

changeset 832:e61cbf28ec31

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
supf1 unnecessary
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Aug 2022 22:07:02 +0900
parents b91681b604d8
children 3fa321cbc337
files src/zorn.agda
diffstat 1 files changed, 39 insertions(+), 69 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Aug 22 11:03:00 2022 +0900
+++ b/src/zorn.agda	Mon Aug 22 22:07:02 2022 +0900
@@ -283,9 +283,9 @@
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
 
-      sup : {x : Ordinal } → x o< z  → SUP A (UnionCF A f mf ay supf x)
+      sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  → IsSup A (UnionCF A f mf ay supf b) ab → supf b ≡ b 
-      supf-is-sup : {x : Ordinal } → (x≤z : x o< z) → supf x ≡ & (SUP.sup (sup x≤z) )
+      supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) 
    supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y 
@@ -299,36 +299,13 @@
    -- ordering is proved here for totality and sup
 
    fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
-   fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup u<z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
+   fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
-   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u<z ) ) ))
-   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u<z ))) ) lt )
+   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
+   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
 
-   csupf-fc : {b s z1 : Ordinal} → b o≤ z → supf s o≤ supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
-   csupf-fc {b} {s} {z1} b≤z ss≤sb (init x refl ) with osuc-≡< ss≤sb
-   ... | case1 eq = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
-            zc04 : odef (UnionCF A f mf ay supf (supf s))  (supf s)
-            zc04 = subst (λ k → odef (UnionCF A f mf ay supf k)  k) (sym eq) ( csupf b≤z  )
-            zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
-            zc05 with zc04
-            ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
-            ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = zc09 u≤x where
-                zc06 : supf u ≡ u
-                zc06 = ChainP.supu=u is-sup
-                zc09 : u o≤ supf s  →  odef (UnionCF A f mf ay supf b)  (supf s)
-                zc09 u≤ss with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u≤ss)
-                ... | case1 su=ss = zc08 where
-                    zc07 : supf u o≤ supf b   
-                    zc07 = subst₂ (λ j k → j o≤ k) (sym zc06) eq u≤ss
-                    zc08 :  odef (UnionCF A f mf ay supf b)  (supf s)
-                    zc08 with osuc-≡< zc07
-                    ... | case2 lt =  ⟪ as , ch-is-sup u (o<→≤ (supf-inject lt )) is-sup fc ⟫ 
-                    ... | case1 su=sb with trio< u b
-                    ... | tri< u<b ¬b ¬c = ?
-                    ... | tri≈ ¬a u=b ¬c = ?
-                    ... | tri> ¬a ¬b b<u = ⟪ ? , ch-is-sup (supf b) ? ? ? ⟫
-                ... | case2 lt =  ⟪ as , ch-is-sup u (o<→≤ (supf-inject (subst (λ k → supf u o< k) eq lt ))) is-sup fc ⟫ 
-   ... | case2 ss<sb = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
+   csupf-fc : {b s z1 : Ordinal} → b o≤ z → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
+   csupf-fc {b} {s} {z1} b≤z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
             s<b : s o< b
             s<b = supf-inject ss<sb
             s≤<z : s o≤ z
@@ -356,14 +333,14 @@
             zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc  )
             ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ 
             ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ 
-   order : {b s z1 : Ordinal} → b o< z → supf s o≤ supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-   order {b} {s} {z1} b<z ss≤sb fc = zc04 where
-      zc00 : ( * z1  ≡  SUP.sup (sup b<z )) ∨ ( * z1  < SUP.sup ( sup b<z ) )
-      zc00 = SUP.x<sup (sup  b<z) (csupf-fc (o<→≤ b<z) ss≤sb fc )
+   order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+   order {b} {s} {z1} b<z ss<sb fc = zc04 where
+      zc00 : ( * z1  ≡  SUP.sup (sup (o<→≤ b<z) )) ∨ ( * z1  < SUP.sup ( sup (o<→≤ b<z) ) )
+      zc00 = SUP.x<sup (sup (o<→≤  b<z) ) (csupf-fc (o<→≤ b<z) ss<sb fc )
       zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
       zc04 with zc00
-      ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup  b<z)  ) (cong (&) eq) )
-      ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup b<z ) )))  lt )
+      ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup (o<→≤ b<z))  ) (cong (&) eq) )
+      ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup (o<→≤ b<z) ) )))  lt )
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
@@ -564,7 +541,7 @@
               m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                            → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
-              m09 {s} {z} s<b fcz = ZChain.order zc b<A (o<→≤ s<b) fcz    
+              m09 {s} {z} s<b fcz = ZChain.order zc b<A s<b fcz    
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
               m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = ZChain.sup=u zc ab (o<→≤ b<A )
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz ) } }  
@@ -584,7 +561,7 @@
               m07 {z} fc = ZChain.fcy<sup zc  m09 fc
               m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                        → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
-              m08 {s} {z1} s<b fc = ZChain.order zc m09 (o<→≤ s<b) fc
+              m08 {s} {z1} s<b fc = ZChain.order zc m09 s<b fc
               m05 : b ≡ ZChain.supf zc b
               m05 = sym (ZChain.sup=u zc ab (o<→≤  m09)
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} )   -- ZChain on x
@@ -740,33 +717,26 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) 
 
-          zc64 : {z : Ordinal } → z o< px → odef (UnionCF A f mf ay supf0 px) (supf0 z)
-          zc64 {z} z<px = chain-mono f mf ay supf0 zc72 zc70  where
+          zc64 : {z : Ordinal } → supf0 z o< supf0 px → odef (UnionCF A f mf ay supf0 px) (supf0 z)
+          zc64 {z} sz<spx = zc73 where
+               z<px = ZChain.supf-inject zc sz<spx
                zc70 : odef (UnionCF A f mf ay supf0 (supf0 z) ) (supf0 z)
                zc70 = ZChain.csupf zc (o<→≤ z<px )
-               zc71 : supf0 z o≤ supf0 px
-               zc71 = ZChain.supf-mono zc (o<→≤ z<px )
-               zc72 : supf0 z o≤ px
-               zc72 = ?
                zc73 : odef (UnionCF A f mf ay supf0 px ) (supf0 z)
-               zc73 = subst (λ k → odef (UnionCF A f mf ay supf0 px ) k ) &iso ( ZChain.csupf-fc zc  o≤-refl  ? (init (proj1 zc70) refl) )
+               zc73 with osuc-≡< (ZChain.supf-mono zc (o<→≤ z<px))
+               ... | case1 eq2 = ⊥-elim ( o<¬≡ eq2 sz<spx )
+               ... | case2 lt = subst (λ k → odef (UnionCF A f mf ay supf0 px ) k ) &iso ( ZChain.csupf-fc zc  o≤-refl lt (init (proj1 zc70) refl) )
 
           supf1<sp1 : {z : Ordinal } → supf1 z o≤ sp1
-          supf1<sp1 {z} with trio< z px | inspect supf1 z
-          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = o≤-refl 
-          ... | tri> ¬a ¬b c | record { eq = eq1 } = o≤-refl
-          ... | tri< a ¬b ¬c | record { eq = eq1 } with trio< (supf1 z) sp1
-          ... | tri< a₁ ¬b₁ ¬c₁ = subst (λ k → k o≤ sp1) eq1 (o<→≤ a₁)
-          ... | tri≈ ¬a b ¬c₁ = o≤-refl0 (trans (sym eq1) b )
-          ... | tri> ¬a ¬b₁ c = ? where
-              zc65 : sp1 o< ZChain.supf zc z
-              zc65 = subst (λ k → sp1 o< k ) eq1 c
-              zc66 :  ( * (ZChain.supf zc z) ≡ * sp1) ∨  (ZChain.supf zc z <<  sp1) 
-              zc66 = subst₂ (λ j k → ( j ≡   k) ∨ ( j  < k ) ) refl (sym *iso)  zc68 where
-                 zc68 : ( *( ZChain.supf zc z) ≡ SUP.sup sup1  ) ∨ ( * (ZChain.supf zc z) < SUP.sup sup1  )
-                 zc68 =  SUP.x<sup sup1 (subst (λ k → odef (UnionCF A f mf ay supf0 px) k ) (sym &iso) (zc64 a) )
-              zc67 : ZChain.supf zc sp1 ≡ sp1
-              zc67 = ?
+          supf1<sp1 {z} = ? where
+               zc50 : supf0 px ≡ sp1
+               zc50 = ? -- ZChain.sup=u zc ? ? ?
+               zc53 : SUP A ( UnionCF A f mf ay supf0 px )
+               zc53 = ZChain.sup zc o≤-refl 
+               zc52 : supf0 px ≡ ?
+               zc52 = ? -- ZChain.sup=u zc ? ? ?
+               zc51 : supf0 sp1 ≡ sp1
+               zc51 = ZChain.sup=u zc ? ? ?
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
@@ -850,13 +820,13 @@
                       zc60 (fsuc w1 fc) with zc60 fc
                       ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                       ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
-                 sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z)
-                 sup {z} z<x with trio< z px
-                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl z<x  ) ( ZChain.sup zc  a ) 
+                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
+                 sup {z} z≤x with trio< z px
+                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl ?  ) ( ZChain.sup zc (o<→≤   a) ) 
                  ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc61 } where
                      zc61 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
                      zc61 {w} lt = ? -- SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) z<x  lt )
-                 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
+                 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) ? ⟫ )
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
@@ -875,11 +845,11 @@
                  ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl a {!!}
                  ... | tri≈ ¬a refl ¬c | _ = {!!} -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc o≤-refl )
                  ... | tri> ¬a ¬b px<b | record { eq = eq1 } = {!!} --  UnionCF⊆ (o<→≤ px<b) o≤-refl ( ZChain.csupf zc o≤-refl ) 
-                 sis : {z : Ordinal} (z<x : z o< x) → supf1 z ≡ & (SUP.sup (sup z<x))
+                 sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x))
                  sis {z} z<x with trio< z px
-                 ... | tri< a ¬b ¬c = ZChain.supf-is-sup zc a
+                 ... | tri< a ¬b ¬c = ZChain.supf-is-sup zc (o<→≤ a )
                  ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x  ⟫ )
+                 ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) ?  ⟫ )
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
@@ -1004,12 +974,12 @@
 --                      UnionCF0⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
 --                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
 --                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
-                 sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z)
+                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z x
                  ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) {!!}) {!!} )
                  ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b c = {!!}
-                 sis : {z : Ordinal} (x≤z : z o< x) → supf1 z ≡ & (SUP.sup (sup {!!}))
+                 sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup {!!}))
                  sis {z} z<x with trio< z x
                  ... | tri< a ¬b ¬c = {!!} where
                      zc8 = ZChain.supf-is-sup (pzc z a) {!!}