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

changeset 761:9307f895891c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
edge case done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 25 Jul 2022 08:29:15 +0900
parents 0dc7999b1d50
children eb68d0870cc6
files src/zorn.agda
diffstat 1 files changed, 24 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Jul 25 06:41:40 2022 +0900
+++ b/src/zorn.agda	Mon Jul 25 08:29:15 2022 +0900
@@ -294,9 +294,9 @@
       f-total : IsTotalOrderSet chain
 
       csupf : {z : Ordinal } → odef chain (supf z) 
-      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 
+      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 
       fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → w << supf u     -- different from order because y o< supf 
-      order : {b sup1 z1 : Ordinal} → b o< z → sup1 o≤ b → FClosure A f (supf sup1) z1 → z1 << supf b
+      order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → z1 << supf b
 
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
@@ -469,13 +469,26 @@
                  m01 with trio< b px    --- px  < b < x
                  ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)
                  ... | tri< b<px ¬b ¬c = chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl m04 where
-                    m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a
+                    m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a -- if a ∈ chain of px, is-max of px can be used
                     m03 with proj2 ua
                     ... | ch-init fc = ⟪ proj1 ua ,  ch-init fc ⟫
-                    ... | ch-is-sup u u≤x is-sup fc with trio< u px
-                    ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup fc ⟫ -- u o< osuc x
-                    ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup fc ⟫
-                    ... | tri> ¬a ¬b c = ?   -- u = x → u = sup →  (b o< x →  b  < a ) → ⊥  
+                    ... | ch-is-sup u u≤x is-sup-a fc with trio< u px
+                    ... | tri< a ¬b ¬c    = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup-a fc ⟫ -- u o< osuc x
+                    ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup-a fc ⟫
+                    ... | tri> ¬a ¬b c = ⊥-elim (<-irr u≤a (ptrans a<b b<u) ) where
+                         su=u : ZChain.supf zc u ≡ u
+                         su=u = ChainP.supfu=u is-sup-a 
+                         u<A : u o< & A
+                         u<A = z09 (subst (λ k → odef A k ) su=u (proj1 (ZChain.csupf zc )))
+                         u≤a : (* u ≡ * a) ∨ (u << a)
+                         u≤a = s≤fc u f mf (subst (λ k → FClosure A f k a) su=u fc ) 
+                         m07 : osuc b o≤ x
+                         m07 = osucc (ordtrans b<px px<x )
+                         fcb : FClosure A f (ZChain.supf zc b) b
+                         fcb = subst (λ k → FClosure A f k b ) (sym (ZChain.sup=u zc ab (z09 ab) 
+                            (record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x m07 o≤-refl lt)  } ) )) ( init ab )
+                         b<u : b << u
+                         b<u = subst (λ k → b << k ) su=u ( ZChain.order zc u<A (ordtrans b<px c)  fcb )
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
@@ -483,9 +496,8 @@
                     m06 : ChainP A f mf ay (ZChain.supf zc) b b
                     m06 = ?
                     m05 : b ≡ ZChain.supf zc b
-                    m05 = sym ( ZChain.sup=u zc {b} {ab} (z09 ab) 
+                    m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono2 x (osucc b<x) o≤-refl uz )  }  )
-                    -- b = px case,  u = px  u< osuc x 
         ... | 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 →
               b o< x → (ab : odef A b) →
@@ -501,9 +513,9 @@
                  m07 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b
                  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 (o<→≤ s<b) fc
+                 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} m09
+                 m05 = sym (ZChain.sup=u zc ab m09
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<x)) o≤-refl lt )} )   -- ZChain on x
                  m06 : ChainP A f mf ay (ZChain.supf zc) b b
                  m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 
@@ -590,7 +602,7 @@
 
      inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
      inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = ? ; fcy<sup = ? 
-      ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
+      ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
           isupf : Ordinal → Ordinal
           isupf z =  & (SUP.sup (ysup f mf ay))
           cy : odef (UnionCF A f mf ay isupf o∅) y