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

changeset 912:870a6b57dd39

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 12 Oct 2022 14:03:38 +0900
parents 3105feb3c4e1
children d5293a7c2ec4
files src/zorn.agda
diffstat 1 files changed, 18 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Oct 12 11:11:42 2022 +0900
+++ b/src/zorn.agda	Wed Oct 12 14:03:38 2022 +0900
@@ -407,7 +407,7 @@
 
       minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x) 
       supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
-      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
+      csupf : {b x : Ordinal } → supf b o< x → x o≤ z → odef (UnionCF A f mf ay supf x) (supf b) -- supf z is not an element of this chain
 
    chain : HOD
    chain = UnionCF A f mf ay supf z
@@ -456,6 +456,9 @@
 
    -- ordering is not proved here but in ZChain1 
 
+   -- csupf< : {a b : Ordinal } → a o≤ b → odef (UnionCF A f mf ay supf z) (supf a) → odef (UnionCF A f mf ay supf z) (supf b) 
+   -- csupf< = ?
+
 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
    supf = ZChain.supf zc
@@ -608,7 +611,7 @@
                 s≤<z : s o≤ & A
                 s≤<z = ordtrans s<b b≤z
                 zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
-                zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc))
+                zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) o≤-refl
                 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
                 zc05 with zc04
                 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
@@ -816,7 +819,7 @@
 
           zc41 : supf0 px o< x →  ZChain A f mf ay x 
           zc41 sfpx<x =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
-              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1    }  where
+              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupfp    }  where
                  --  supf0 px is included by the chain
                  --  ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x 
                  --  supf1 x ≡ sp1, which is not included now
@@ -1014,10 +1017,10 @@
                                   sf<px : supf0 s o< px
                                   sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx
                                   csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
-                                  csupf17 (init as refl ) = ZChain.csupf zc sf<px 
+                                  csupf17 (init as refl ) = ZChain.csupf zc sf<px o≤-refl
                                   csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
 
-                        ... | case2 sfp<px  with ZChain.csupf zc sfp<px --  odef (UnionCF A f mf ay supf0 px) (supf0 px)
+                        ... | case2 sfp<px  with ZChain.csupf zc sfp<px o≤-refl --  odef (UnionCF A f mf ay supf0 px) (supf0 px)
                         ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ 
                         ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u (ordtrans u≤x px<x) 
                               record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ (o<→≤ u≤x) ) ⟫  where
@@ -1078,13 +1081,13 @@
                      psz1≤px :  supf1 z1 o≤ px
                      psz1≤px =  subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 
                      cs01 : supf0 px o< px → odef (UnionCF A f mf ay supf0 px) (supf0 px)
-                     cs01 spx<px = ZChain.csupf zc spx<px
+                     cs01 spx<px = ZChain.csupf zc spx<px o≤-refl
                      csupf2 :  odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
                      csupf2 with  trio< z1 px | inspect supf1 z1
                      csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
                      ... | case2 lt  = zc12 (case1 cs03)  where
                            cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1)
-                           cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
+                           cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) o≤-refl
                      ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) )
                      ... | case1 sfz=sfpx =  zc12 (case2 (init (ZChain.asupf zc) cs04 )) where
                            supu=u : supf1 (supf1 z1) ≡ supf1 z1
@@ -1098,7 +1101,7 @@
                      ... | case2 sfz<sfpx =  ? ---   supf0 z1 o< supf0 px
                      csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
                      csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 }  with trio< sp1 px
-                     ... | tri< sp1<px ¬b ¬c = ? --  sp1 o< px, supf0 sp1 ≡  supf0 px, sp1 o< z1
+                     ... | tri< sp1<px ¬b ¬c = ? --  sp1 o< px, supf0 sp1 o≤ px,  supf0 sp1 o≤ supf0 px, sp1 o< z1
                      ... | tri≈ ¬a sp1=px ¬c = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
                              record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where 
                           --  supf1 z1 ≡ sp1, px o< z1, sp1 o< x  -- sp1 o< z1
@@ -1114,6 +1117,13 @@
                           supu=u = ?
                      ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x  ⟫ )
 
+                 csupfp : {w z : Ordinal } → supf1 w o< z → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 w) 
+                 csupfp {w} {z} sw1<z z≤x with osuc-≡< z≤x
+                 ... | case1 eq = ?
+                 ... | case2 lt = ?  where
+                     csupfpx : odef (UnionCF A f mf ay supf0 z) (supf0 w) 
+                     csupfpx = ZChain.csupf zc ? ?
+
           zc4 : ZChain A f mf ay x     --- x o≤ supf px 
           zc4 with trio< x (supf0 px)
           ... | tri> ¬a ¬b c = zc41 c