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

changeset 733:15f3bcc4ae3f

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 Tue, 19 Jul 2022 09:36:02 +0900
parents ddeb107b6f71
children 753780183ddf
files src/zorn.agda
diffstat 1 files changed, 22 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jul 19 07:36:10 2022 +0900
+++ b/src/zorn.agda	Tue Jul 19 09:36:02 2022 +0900
@@ -266,6 +266,8 @@
    field
       u>0      : o∅ o< u    -- ¬ ch-init
       supf=u   : supf u ≡ u  
+      supf-mono  : {a b : Ordinal } → a o≤ b → supf a o≤ supf b
+      supf-<  : {a b : Ordinal } → a o≤ b → (supf a ≡ supf b) ∨ (supf a << supf b)
       au       : odef A u
       ¬u=fx    : {x : Ordinal} → ¬ ( u ≡ f x )
       asup     : (x : Ordinal) → odef A (supf x)
@@ -315,7 +317,6 @@
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {init : Ordinal} (ay : odef A init)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    field
-      chain≤x : { b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) b → odef (UnionCF A f mf ay (ZChain.supf zc) z) b
       chain-mono2 : { a b c : Ordinal }  → 
           a o≤ b → b o≤ z → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
       is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) z) a ) →  b o< z  → (ab : odef A b) 
@@ -436,34 +437,32 @@
      SZ1 A f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
-        ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 ; chain≤x = bchain } where
-           -- supf u ≡ u ?
+        ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 } where
            px = Oprev.oprev op
-           bchain : {b : Ordinal} → b o≤ x →
-                odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) b →
-                odef (UnionCF A f mf ay (ZChain.supf zc) x) b
-           bchain {b} b≤x ⟪ ab , record { u = u0 ; u<x = u<x ; uchain = ch-init .b x } ⟫ = 
-                 ⟪ ab , record { u = u0 ; u<x = case2 refl ; uchain = ch-init b x } ⟫ 
-           bchain {b} b≤x ub@record { proj1 =  ab ; proj2 =  record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } } with osuc-≡< b≤x
-           ... | case2 lt = ⟪ ab , record { u = UChain.u (proj2 sz00) ; u<x = ? ; uchain = UChain.uchain (proj2 sz00) } ⟫ where
-                 sz00 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
-                 sz00 = ZChain1.chain≤x (prev px ? ) ?  ub
-           ... | case1 refl = ?
-
            chain-mono2 :  {a b c : Ordinal} → a o≤ b → b o≤ x →
                 odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
-           chain-mono2 {a} {b} {c} a≤b b≤x uac = {!!}
+           chain-mono2 {a} {b} {c} a≤b b≤x ⟪ ua , record { u = _ ; u<x = u<x ; uchain = ch-init .c x } ⟫ = 
+                    ⟪ ua , record { u = _ ; u<x = case2 refl  ; uchain = ch-init c x } ⟫ 
+           chain-mono2 {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 } ⟫ 
            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 {a} {b} ua b<x ab (case2 is-sup) a<b with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ab f )
-           ... | case1 has-prev = m03 (subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) k ) {!!} m02 ) {!!} where
-                 m03 : odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) b → b o< x → odef (UnionCF A f mf ay (ZChain.supf zc) x) b 
-                 m03 = {!!}
-                 m02 : odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) (f (HasPrev.y has-prev))
-                 m02 = ZChain.f-next zc (HasPrev.ay has-prev) 
+           is-max {a} {b} ua b<x ab (case2 is-sup) a<b with ODC.p∨¬p O ( HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f )
+           ... | case1 has-prev = m04 where
+                 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
+                 m04 = ⟪ m07   , record { u = UChain.u (proj2 m06) ; u<x = UChain.u<x (proj2 m06) ; uchain = ? } ⟫ where
+                     m06 : odef (UnionCF A f mf ay (ZChain.supf zc) x) (HasPrev.y has-prev )
+                     m06 = HasPrev.ay has-prev
+                     m07 : odef A b 
+                     m07 = subst (λ k → odef A k ) (sym (HasPrev.x=fy has-prev)) (proj2 (mf _ (proj1 m06) ))
+                     m08 :  Chain A f mf ay (ZChain.supf zc) (UChain.u (proj2 m06)) (f ( HasPrev.y has-prev ))
+                     m08 with proj2 m06
+                     ... | record { u = _ ; u<x = u<x ; uchain = ch-init .(HasPrev.y has-prev) fc } = 
+                          ch-init (f (HasPrev.y has-prev)) (fsuc _ fc) 
+                     ... | record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } = ch-is-sup ? (fsuc _ fc) 
            ... | case2  ¬fy<x  = {!!} where
                  m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
                  m01 with trio< px b
@@ -657,8 +656,8 @@
           psupf0 : (z : Ordinal) → Ordinal
           psupf0 z with trio< z x
           ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
-          ... | tri≈ ¬a b ¬c = y
-          ... | tri> ¬a ¬b c = y
+          ... | tri≈ ¬a b ¬c = & A
+          ... | tri> ¬a ¬b c = & A
 
           pchain : HOD
           pchain = UnionCF A f mf ay psupf0 x