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

changeset 735:5dacaf73eba8

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 13:44:33 +0900
parents 753780183ddf
children 3c3e3a1291bb
files src/zorn.agda
diffstat 1 files changed, 41 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jul 19 10:01:59 2022 +0900
+++ b/src/zorn.agda	Tue Jul 19 13:44:33 2022 +0900
@@ -306,13 +306,13 @@
    chain : HOD
    chain = UnionCF A f mf ay supf z
    field
-      -- chain-mono : {z1 : Ordinal} → z1 o≤ z → UnionCF A f mf ay supf z1 ⊆' UnionCF A f mf ay supf z 
       chain<A : {z : Ordinal } → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf (& A) 
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
+      sup=u : {b : Ordinal} → (ab : odef A b)  → IsSup A chain ab → supf b ≡ b 
 
 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
@@ -438,51 +438,63 @@
         chain-mono2 : (x : Ordinal) {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 x {a} {b} {c} a≤b b≤x ⟪ ua , record { u = _ ; u<x = u<x ; uchain = ch-init .c fc } ⟫ = 
-                ⟪ ua , record { u = _ ; u<x = case2 refl  ; uchain = ch-init c fc } ⟫ 
+            ⟪ 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 } ⟫ 
+            ⟪ ua , record { u = u ; u<x = case1 (ordtrans<-≤ u<x a≤b) ; uchain = ch-is-sup is-sup fc } ⟫ 
+        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 → 
+            * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
+        is-max-hp x {a} {b} ua b<x ab has-prev a<b = 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 = subst (λ k → Chain A f mf ay (ZChain.supf zc) (UChain.u (proj2 m06)) k) (sym (HasPrev.x=fy has-prev)) m08 } ⟫ 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) 
         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 x } where
            px = Oprev.oprev op
+           zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
+           zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
            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 = m04 where
-                 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
-                 m04 = ?
+           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 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) 
+           ... | case1 has-prev = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            ... | case2  ¬fy<x  = m01 where
+                 px<x : px o< x
+                 px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc
                  m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
-                 m01 with trio< px b
-                 ... | tri< a ¬b ¬c = ZChain1.chain-mono2 (prev px {!!}) {!!} {!!} m04 where
+                 m01 with trio< b px 
+                 ... | tri> ¬a ¬b c = ⊥-eim ()
+                 ... | 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 = ?
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
-                    m04 = ZChain1.is-max (prev px {!!}) {!!} {!!} ab {!!} a<b
-                 ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b c = {!!}
-        ... | no lim = record { is-max = {!!} ; chain-mono2 = chain-mono2 x  }  where
+                    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 = {!!}
+        ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x  }  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) →
               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 (UnionCF A f mf ay (ZChain.supf zc) x) ab f )
-           --- m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
-           --- m04 = ZChain1.is-max (prev (osuc b) {!!} ) {!!} <-osuc ab {!!} a<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≤-refl m04 where
+                 m05 : b ≡ ZChain.supf zc b
+                 m05 = sym (ZChain.sup=u ? ab is-sup)
+                 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 ? (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function