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

changeset 1046:e99e2bcb885c

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 Mon, 05 Dec 2022 15:09:41 +0900
parents 022d2ef3f20b
children aebab71cc386
files src/zorn.agda
diffstat 1 files changed, 38 insertions(+), 28 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Dec 05 00:39:14 2022 +0900
+++ b/src/zorn.agda	Mon Dec 05 15:09:41 2022 +0900
@@ -332,9 +332,8 @@
    field
       supf :  Ordinal → Ordinal
 
-      order : {x y w : Ordinal } → y o≤ z → x o< y → supf x o< z → FClosure A f (supf x) w → w ≤ supf y
-
-      cfcs : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
+      cfcs  : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
+      order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b
 
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
@@ -397,13 +396,13 @@
      subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where
          fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
          fc-total with trio< ua ub
-         ... | tri< a₁ ¬b ¬c with ≤-ftrans  (order (o<→≤ sub<x) a₁ (subst (λ k → k o< z) (sym sua=ua) sua<x) fca ) (s≤fc (supf ub) f mf fcb )
+         ... | tri< a₁ ¬b ¬c with ≤-ftrans  (order (o<→≤ sub<x) (subst₂ (λ j k → j o< k) (sym sua=ua) (sym sub=ub) a₁) fca ) (s≤fc (supf ub) f mf fcb )
          ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                   ct00 : * (& a) ≡ * (& b)
                   ct00 = cong (*) eq1
          ... | case2 a<b =  tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)
          fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb
-         fc-total | tri> ¬a ¬b c with ≤-ftrans  (order (o<→≤ sua<x) c (subst (λ k → k o< z) (sym sub=ub) sub<x) fcb ) (s≤fc (supf ua) f mf fca )
+         fc-total | tri> ¬a ¬b c with ≤-ftrans  (order (o<→≤ sua<x) (subst₂ (λ j k → j o< k) (sym sub=ub) (sym sua=ua) c) fcb ) (s≤fc (supf ua) f mf fca )
          ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                   ct00 : * (& a) ≡ * (& b)
                   ct00 = cong (*) (sym eq1)
@@ -454,7 +453,7 @@
    supf-idem {b} b≤z sfb≤x = z52 where
        z54 :  {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
        z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
-       z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z u<b (ordtrans<-≤ (subst (λ k → k o< b) (sym su=u) u<b) b≤z) fc where
+       z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z (subst (λ k → k o< supf b) (sym su=u) u<x)  fc where
                u<b : u o< b
                u<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
        z52 : supf (supf b) ≡ supf b
@@ -655,7 +654,6 @@
         ... | ⟪ ab0 , ch-is-sup u u<x su=u fc ⟫ = ⟪ ab , subst (λ k → UChain ay x k )
                       (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x su=u (fsuc _ fc))  ⟫
 
-
         supf = ZChain.supf zc
 
         zc1 :  (x : Ordinal ) → x o≤ & A →   ZChain1 A f mf< ay zc x
@@ -859,9 +857,7 @@
           m13 : supf0 px o< x → supf0 px o≤ sp1
           m13 spx<x = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1)  m14 where
              m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1)
-             m14 {z} ⟪ as , ch-init fc ⟫ = ≤-ftrans (ZChain.fcy<sup zc o≤-refl fc) (sfpx≤sp1 spx<x)
-             m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = 
-                ≤-ftrans (ZChain.order zc o≤-refl u<x (subst (λ k → k o< px) (sym (su=u)) u<x ) fc) (sfpx≤sp1 spx<x )
+             m14 {z} uz = MinSUP.x≤sup sup1 (case1 uz)
 
           zc41 : ZChain A f mf< ay x
           zc41 =  record { supf = supf1 ; sup=u = sup=u ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order
@@ -1096,23 +1092,37 @@
                                 u≤px : u o≤ px
                                 u≤px = ordtrans u<x z≤px
 
-                 order1 : {a b : Ordinal} {w : Ordinal} →
-                    b o≤ x → a o< b → supf1 a o< x  → FClosure A f (supf1 a) w → w ≤ supf1 b
-                 order1 {a} {b} {w} b≤x a<b sa<x fc with cfcs a<b b≤x ? fc
-                 ... | t = ?
+                 order : {a b : Ordinal} {w : Ordinal} →
+                    b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
+                 order {a} {b} {w} b≤x sa<sb fc with osuc-≡< b≤x
+                 ... | case2 b<x = 
+                    subst ( λ k → w ≤ k ) (sym (sf1=sf0 ?)) ( ZChain.order zc (zc-b<x _ b<x) 
+                       (subst₂ (λ j k → j o< k ) (sf1=sf0 ?) (sf1=sf0 ?) sa<sb) (fcup fc ?)  )
+                 ... | case1 eq with zc43 (supf1 a) b
+                 ... | case1 sa<b = subst (λ k → w ≤ k ) (sym (sf1=sp1 ? )) ( MinSUP.x≤sup sup1 ?)  where
+                     z26 : odef pchainpx w 
+                     z26 =  zc11 (chain-mono f mf ay supf1 supf1-mono ? (cfcs ? b≤x ? fc))
+                 ... | case2 b≤sa = ⊥-elim ( o≤> z27 sa<sb ) where
+                     z28 : supf1 (supf0 a) ≡ supf1 a -- x o≤ supf1 a  → 
+                     z28 with zc43 (supf0 a) x
+                     ... | case1 sa<x = subst₂ (λ j k → j ≡ k) ? ? ( ZChain.supf-idem zc ? ? )
+                     ... | case2 x≤sa with osuc-≡< ( supf1-mono x≤sa )   -- = ?  --  sp1 ≡ supf0 a   --- sp1 o≤ supf0 a
+                     ... | case1 eq = sym (trans z29 eq ) where
+                          z30 : supf1 (supf0 a) ≡ supf1 (supf0 a) 
+                          z30 = ?
+                          z29 : supf1 a ≡ supf1 x
+                          z29 = ?
+                          z32 : supf1 x ≡ supf1 (supf0 a) -- supf1 (supf0 a) ≡ supf1 a
+                          z32 = eq 
+                     ... | case2 lt = ? where
+                          z31 : supf1 x o< supf1 (supf0 a)
+                          z31 = lt
 
-                 order : {a b : Ordinal} {w : Ordinal} →
-                    b o≤ x → a o< b → supf1 a o< x  → FClosure A f (supf1 a) w → w ≤ supf1 b
-                 order {a} {b} {w} b≤x a<b sa<x fc with trio< b px
-                 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b ? (fcup fc (o<→≤ (ordtrans a<b b<px) ))
-                 ... | tri≈ ¬a b=px ¬c = ZChain.order zc (o≤-refl0 b=px) a<b ? (fcup fc (o<→≤ (subst (λ k → a o< k) b=px a<b )))
-                 ... | tri> ¬a ¬b px<b with trio< a px
-                 ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px ? fc) (sfpx≤sp1  ? ) --   supf1 a ≡ supf0 a
-                 ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (
-                     case2 ⟪ (subst (λ k → FClosure A f (supf0 k) w) a=px fc ) , subst (λ k → supf0 k o< x) a=px sa<x ⟫ )
-                 ... | tri> ¬a ¬b px<a = ⊥-elim (¬p<x<op ⟪ px<a , zc22 ⟫ ) where  --   supf1 a ≡ sp1
-                     zc22 : a o< osuc px
-                     zc22 = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
+                     z27 : supf1 b o≤ supf1 a
+                     z27 = begin 
+                       supf1 b ≤⟨ ? ⟩
+                       supf1 (supf1 a) ≡⟨ ? ⟩
+                       supf1 a ∎ where open o≤-Reasoning O
 
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b
@@ -1178,14 +1188,14 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 with trio< (IChain.i ia)  (IChain.i ib)
                ... | tri< ia<ib ¬b ¬c with
-                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ia<ib ? (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib))
+                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ? (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib))
                ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                    ct00 : * (& a) ≡ * (& b)
                    ct00 = cong (*) eq1
                ... | case2 lt = tri< lt  (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)
                uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib))
                uz01 | tri> ¬a ¬b ib<ia  with
-                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ib<ia ? (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia))
+                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ? (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia))
                ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                    ct00 : * (& a) ≡ * (& b)
                    ct00 = sym (cong (*) eq1)