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

changeset 844:0855fce6ee92

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, 31 Aug 2022 19:48:12 +0900
parents ef0433f41e55
children ef7c721b32dc
files src/zorn.agda
diffstat 1 files changed, 63 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Aug 30 14:30:36 2022 +0900
+++ b/src/zorn.agda	Wed Aug 31 19:48:12 2022 +0900
@@ -765,12 +765,62 @@
           pcy1 : odef pchain1 y
           pcy1 = ⟪ ay , ch-init (init ay refl)    ⟫
 
+          supf0=1 : {z : Ordinal } → z o≤ px  → supf0 z ≡ supf1 z
+          supf0=1 {z} z≤px with trio< z px
+          ... | tri< a ¬b ¬c = refl
+          ... | tri≈ ¬a b ¬c = refl
+          ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c )
+
           supf1≤sp1 : {a : Ordinal } → supf1 a o≤ sp1
           supf1≤sp1 = ?
 
           supf-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b 
           supf-mono = ?
 
+          zc70 : HasPrev A pchain x f → ¬ xSUP pchain x 
+          zc70 pr xsup = ?
+
+          fc0→1 : {s z : Ordinal } → s o≤ px  → FClosure A f (supf0 s) z → FClosure A f (supf1 s) z  
+          fc0→1 {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (supf0=1 s≤px) fc
+
+          fc1→0 : {s z : Ordinal } → s o≤ px  → FClosure A f (supf1 s) z → FClosure A f (supf0 s) z  
+          fc1→0 {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (sym (supf0=1 s≤px)) fc
+
+          CP0→1 : {u : Ordinal } → u o≤ px  → ChainP A f mf ay supf0 u → ChainP A f mf ay supf1 u  
+          CP0→1 {u} u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym (supf0=1 u≤px)) (ChainP.supu=u cp) } where
+                  fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u )
+                  fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (supf0=1 u≤px) ( ChainP.fcy<sup cp fc )
+                  order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z2 →
+                    (z2 ≡ supf1 u) ∨ (z2 << supf1 u)
+                  order {s} {z2} s<u fc = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (supf0=1 u≤px) ( ChainP.order cp ss<su (fc1→0 s≤px fc )) where
+                      s≤px : s o≤ px
+                      s≤px = ordtrans (supf-inject0 supf-mono s<u) u≤px
+                      ss<su : supf0 s o< supf0 u
+                      ss<su = subst₂ (λ j k → j o< k ) (sym (supf0=1 s≤px )) (sym (supf0=1 u≤px)) s<u
+
+          CP1→0 : {u : Ordinal } → u o≤ px  → ChainP A f mf ay supf1 u → ChainP A f mf ay supf0 u  
+          CP1→0 {u} u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (supf0=1 u≤px) (ChainP.supu=u cp) } where
+                  fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u) ∨ (z << supf0 u )
+                  fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym (supf0=1 u≤px)) ( ChainP.fcy<sup cp fc )
+                  order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z2 →
+                    (z2 ≡ supf0 u) ∨ (z2 << supf0 u)
+                  order {s} {z2} s<u fc = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym (supf0=1 u≤px)) ( ChainP.order cp ss<su (fc0→1 s≤px fc )) where
+                      s≤px : s o≤ px
+                      s≤px = ordtrans (supf-inject0 (ZChain.supf-mono zc) s<u) u≤px
+                      ss<su : supf1 s o< supf1 u
+                      ss<su = subst₂ (λ j k → j o< k ) (supf0=1 s≤px ) (supf0=1 u≤px) s<u
+
+          UnionCF0⊆1  : {z : Ordinal } → z o≤ px →  UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay supf1 z
+          UnionCF0⊆1  {z} z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+          UnionCF0⊆1  {z} z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = 
+               ⟪ au , ch-is-sup u u≤z (CP0→1 (OrdTrans u≤z z≤px ) is-sup) (fc0→1 (OrdTrans u≤z z≤px ) fc) ⟫ 
+
+          UnionCF1⊆0  : {z : Ordinal } → z o≤ px →  UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf0 z
+          UnionCF1⊆0  {z} z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+          UnionCF1⊆0  {z} z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = 
+               ⟪ au , ch-is-sup u u≤z (CP1→0 (OrdTrans u≤z z≤px ) is-sup) 
+                                      (fc1→0 (OrdTrans u≤z z≤px ) fc) ⟫ 
+
           -- zc100  : xSUP (UnionCF A f mf ay supf0 px) x → x ≡ sp1
           -- zc100  = ?
 
@@ -778,7 +828,7 @@
           --
           --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
 
-          no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x
+          no-extension : ¬ xSUP (UnionCF A f mf ay supf0 px) x → ZChain A f mf ay x
           no-extension ¬sp=x = record { supf = supf1 ;  sup = sup ; supf-mono = supf-mono
                ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
               ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
@@ -853,7 +903,7 @@
                               ... | tri> ¬a ¬b px<s | _ = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k ) b zc14)))  where --  px o< s < u1 = px
                                  zc14 :  s o< u1
                                  zc14 = ZChain.supf-inject zc s<u1 
-                          ... | tri> ¬a ¬b px<u1 | record { eq = eq2 } = ⊥-elim ? where
+                          ... | tri> ¬a ¬b px<u1 | record { eq = eq2 } = ⊥-elim (¬sp=x zcsup)  where
                              zc31 : x ≡ u1 
                              zc31 with trio< x u1 
                              ... | tri≈ ¬a b ¬c = b
@@ -882,8 +932,8 @@
 
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z px | inspect supf1 z
-                 ... | tri< a ¬b ¬c | record { eq = eq1} = ? -- ZChain.sup zc (o<→≤   a) 
-                 ... | tri≈ ¬a b ¬c | record { eq = eq1} = ?  -- ZChain.sup zc (o≤-refl0 b) 
+                 ... | tri< a ¬b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 (o<→≤ a)) (ZChain.sup zc (o<→≤ a) ) 
+                 ... | tri≈ ¬a b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 (o≤-refl0 b)) (ZChain.sup zc (o≤-refl0 b) )
                  ... | tri> ¬a ¬b px<z | record { eq = eq1} = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc31 } where
                      zc30 : z ≡ x
                      zc30 with osuc-≡< z≤x
@@ -906,8 +956,10 @@
                      -- ... | refl = case1 record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup ? } } 
                  csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
                  csupf {b} b≤x with trio< b px | inspect supf0 b
-                 ... | tri< a ¬b ¬c | _ = ? -- ZChain.csupf zc (o<→≤ a )
-                 ... | tri≈ ¬a refl ¬c | _ = ? -- ZChain.csupf zc o≤-refl 
+                 ... | tri< a ¬b ¬c | _ =  ? where
+                     zc31 = ZChain.csupf zc (o<→≤ a )
+                 ... | tri≈ ¬a refl ¬c | _ = ? where
+                     zc32 = ZChain.csupf zc o≤-refl 
                  ... | tri> ¬a ¬b px<b | record { eq = eq1 } = ? where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -981,7 +1033,7 @@
           ptotal0 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay supf0 ( (proj2 ca)) ( (proj2 cb)) 
-
+  
           usup : SUP A pchain
           usup = supP pchain (λ lt → proj1 lt) ptotal0
           spu = & (SUP.sup usup)
@@ -1023,7 +1075,10 @@
                      subst (λ k → UChain A f mf ay supf x k )
                           (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫ 
 
-          no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) ∨ HasPrev A pchain x f → ZChain A f mf ay x
+          zc70 : HasPrev A pchain x f → ¬ xSUP pchain x 
+          zc70 pr xsup = ?
+
+          no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x
           no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = sup=u
                ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!}
                ; csupf = csupf ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where