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

changeset 743:71556e611842

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 Thu, 21 Jul 2022 07:58:34 +0900
parents de9d9c70a0d7
children d92ad9e365b6
files src/zorn.agda
diffstat 1 files changed, 24 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Jul 21 04:18:12 2022 +0900
+++ b/src/zorn.agda	Thu Jul 21 07:58:34 2022 +0900
@@ -261,6 +261,8 @@
       fcy<sup  : {z : Ordinal } → FClosure A f y z → z << supf u
       csupz    : FClosure A f (supf u) z 
       order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → z1 << supf u
+      y<s      : y << supf u  -- not a initial chain
+      supfu=u  : supf u ≡ u 
 
 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) : Ordinal →  Ordinal → Set n where
     ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay supf o∅ z 
@@ -357,6 +359,10 @@
           ... | case1 eq =  subst (λ k → * b < k ) eq ct05
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
 
+init-uchain : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y ) 
+    { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y
+init-uchain A f mf ay = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  } ⟫
+
 ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    → {x z : Ordinal } →  ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
 ChainP-next A f mf {y} ay supf {x} {z} cp = {!!} --record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp  ; au = ChainP.au cp
@@ -431,6 +437,14 @@
             ⟪ ua , record { u = _ ; u<x = case2 refl  ; uchain = ch-init c fc } ⟫ 
         chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 
             ⟪ ua , record { u = u ; u<x = case1 (ordtrans<-≤ u<x a≤b) ; uchain = ch-is-sup is-sup fc } ⟫ 
+        chain<ZA : {x : Ordinal } → UnionCF A f mf ay (ZChain.supf zc) x ⊆' UnionCF A f mf ay (ZChain.supf zc) (& A)
+        chain<ZA {x} ux with UChain.uchain (proj2 ux)
+        ... | ch-init _ fc = ⟪ proj1 ux , record { u = UChain.u (proj2 ux) ; u<x = case2 refl ; uchain = ch-init _ fc  } ⟫
+        ... | ch-is-sup is-sup fc = ⟪ proj1 ux , record { u = UChain.u (proj2 ux) ; u<x = case1 u<x ; uchain = UChain.uchain (proj2 ux) } ⟫ where
+            u<A : (& ( * ( ZChain.supf zc (UChain.u (proj2 ux)))))  o< & A
+            u<A = c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fcs _ f mf fc) )
+            u<x : UChain.u (proj2 ux) o< & A
+            u<x = subst (λ k → k o< & A ) (trans &iso (ChainP.supfu=u is-sup)) u<A
         is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
             b o< x → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f → 
@@ -482,13 +496,20 @@
                     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
                  ... | tri≈ ¬a b=px ¬c = ? -- b = px case
-        ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x  }  where
+        ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = ? }  where
+           fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u
+           fcy<sup {u} {w} u<x fc = ?
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
               * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
-           is-max {a} {b} ua b<x ab (case2 is-sup) a<b = chain-mono2 x (o<→≤ ob<x) o≤-refl m04 where
+           is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay )
+           ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA (chain-mono2 (osuc x) (o<→≤ <-osuc ) o≤-refl ua )) )
+                       (subst (λ k → * a < * k ) (sym b=y) a<b ) )
+           ... | case2 y<b = chain-mono2 x (o<→≤ ob<x) o≤-refl m04 where
+                 y<s : y << ZChain.supf zc b
+                 y<s = y<s 
                  ob<x : osuc b o< x
                  ob<x with trio< (osuc b) x
                  ... | tri< a ¬b ¬c = a
@@ -502,7 +523,7 @@
                  m05 = sym (ZChain1.sup=u (prev (osuc b) ob<x) {_} {ab} <-osuc 
                         record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ ob<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 }
+                 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 ; y<s = y<s }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
                  m04 = ⟪ ab , record { u = b ; u<x = case1 <-osuc ; uchain = ch-is-sup m06 (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫