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

changeset 813:1627cc8f193e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
< on ZChain.sup
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 16 Aug 2022 16:01:42 +0900
parents 96e6643c833d
children 95db436cce67
files src/zorn.agda
diffstat 1 files changed, 39 insertions(+), 43 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Aug 16 15:24:14 2022 +0900
+++ b/src/zorn.agda	Tue Aug 16 16:01:42 2022 +0900
@@ -283,18 +283,18 @@
       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=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
-      supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
+      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 (osuc b)) ab → supf b ≡ b 
+      supf-is-sup : {x : Ordinal } → (x≤z : x o< z) → supf x ≡ & (SUP.sup (sup x≤z) )
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
 
    -- 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 : 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)  
        , 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 u<z ) ) ))
+   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u<z ))) ) lt )
        
    order : {b s z1 : Ordinal} → b o< z → s o< b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
    order {b} {s} {z1} b<z s<b fc = zc04 where
@@ -311,12 +311,12 @@
             zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 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) ⟫ 
-      zc00 : ( * z1  ≡  SUP.sup (sup (o<→≤ b<z) )) ∨ ( * z1  < SUP.sup ( sup (o<→≤ b<z) ) )
-      zc00 = SUP.x<sup (sup (o<→≤ b<z)) (zc01 fc )
+      zc00 : ( * z1  ≡  SUP.sup (sup b<z )) ∨ ( * z1  < SUP.sup ( sup b<z ) )
+      zc00 = SUP.x<sup (sup  b<z) (zc01 fc )
       zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
       zc04 with zc00
-      ... | 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 )
+      ... | 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 )
 
 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
@@ -511,15 +511,15 @@
               b<A : b o< & A
               b<A = z09 ab
               m05 : b ≡ ZChain.supf zc b
-              m05 = sym ( ZChain.sup=u zc ab (o<→≤ (z09 ab)) 
+              m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) uz )  }  )
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
-              m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
+              m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
               m09 : {sup1 z1 : Ordinal} → sup1 o< b 
                            → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
               m09 {sup1} {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 )
+              m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = ZChain.sup=u zc ab b<A 
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) uz ) } }  
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
@@ -534,15 +534,15 @@
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
               m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
-              m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
+              m07 {z} fc = ZChain.fcy<sup zc  m09 fc
               m08 : {sup1 z1 : Ordinal} → sup1 o< b 
                        → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
               m08 {sup1} {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)
+              m05 = sym (ZChain.sup=u zc ab  m09
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} )   -- ZChain on x
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
-              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = ZChain.sup=u zc ab (o<→≤ m09)
+              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = ZChain.sup=u zc ab m09
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} } 
 
      ---
@@ -803,21 +803,19 @@
                       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 (o<→≤ a)) ( ZChain.sup zc (o<→≤ a) )
-                 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl z≤x (o≤-refl0 b)) ( ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl ))
-                 ... | tri> ¬a ¬b c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = {!!} }
+                 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 ? (o<→≤ a)) ( ZChain.sup zc  a )
+                 ... | tri> ¬a ¬b px<z = ?
+                 ... | 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=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
-                 sup=u {b} ab b≤x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = {!!} }
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) record { x<sup = {!!} }
-                 ... | tri> ¬a ¬b px<b = {!!} where
-                     zc30 : x ≡ b
-                     zc30 with osuc-≡< b≤x
-                     ... | case1 eq = sym (eq)
-                     ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
+                    b o< x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
+                 sup=u {b} ab b<x is-sup with trio< b px
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab a record { x<sup = {!!} }
+                 ... | tri≈ ¬a b ¬c = ?
+                 ... | tri> ¬a ¬b px<b = {!!} 
                  csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
                  csupf {b} b≤x with trio< b px | inspect supf1 b
                  ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) b≤x ( ZChain.csupf zc (o<→≤ a) )
@@ -833,7 +831,7 @@
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
                      zc31 : ChainP A f mf ay supf1 b
                      zc31 = record { fcy<sup = {!!} ; order = {!!} ; supu=u = {!!} }
-                 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 = {!!}
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
@@ -959,20 +957,18 @@
 --                      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 = SUP⊆ (UnionCFR⊆ {!!}) usup
-                 ... | tri> ¬a ¬b c = SUP⊆ (UnionCFR⊆ {!!}) usup
-                 sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup x≤z))
-                 sis {z} z≤x with trio< z x
+                 ... | tri≈ ¬a b ¬c = ?
+                 ... | tri> ¬a ¬b c = ?
+                 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) o≤-refl 
-                 ... | tri≈ ¬a b ¬c = refl
-                 ... | tri> ¬a ¬b c with osuc-≡< z≤x
-                 ... | case1 eq = ⊥-elim ( ¬b eq )
-                 ... | case2 lt = ⊥-elim ( ¬a lt )
-                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
+                     zc8 = ZChain.supf-is-sup (pzc z a) ?
+                 ... | tri≈ ¬a b ¬c = ?
+                 ... | tri> ¬a ¬b c = ?
+                 sup=u : {b : Ordinal} (ab : odef A b) → b o< x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
                  sup=u {b} ab b<x is-sup with trio< b x
                  ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x<sup = {!!} }
                  ... | tri≈ ¬a b ¬c = {!!}