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

changeset 955:bc27df170a1e

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, 03 Nov 2022 10:16:02 +0900
parents e43a5cc72287
children a2b13a4b6727
files src/zorn.agda
diffstat 1 files changed, 28 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Nov 02 13:53:10 2022 +0900
+++ b/src/zorn.agda	Thu Nov 03 10:16:02 2022 +0900
@@ -73,11 +73,11 @@
 ≤-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
 ≤-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
 
-<-ftrans : {x y z : Ordinal } →  x <=  y →  y <=  z →  x <=  z 
-<-ftrans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl
-<-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z
-<-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
-<-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
+<=-trans : {x y z : Ordinal } →  x <=  y →  y <=  z →  x <=  z 
+<=-trans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl
+<=-trans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z
+<=-trans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
+<=-trans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
 
 ftrans<=-< : {x y z : Ordinal } →  x <=  y →  y << z →  x <<  z 
 ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) (sym (cong (*) eq))  y<z
@@ -465,6 +465,27 @@
 
    -- ordering is not proved here but in ZChain1 
 
+   IsSup< : {b x : Ordinal }  (ab : odef A b ) 
+          → b o< x 
+          → IsSup A (UnionCF A f mf ay supf x) ab → IsSup A (UnionCF A f mf ay supf b) ab
+   IsSup< {b} {x}  ab b<x is-sup = record { 
+           x≤sup =  λ {z} uz → IsSup.x≤sup is-sup (chain-mono f mf ay supf supf-mono (o<→≤ b<x) uz)
+         ; minsup = m07 } where
+             m10 : {s : Ordinal }  →  (odef A s ) 
+                →  ( {w : Ordinal} → odef (UnionCF A f mf ay supf b) w → (w ≡ s) ∨ (w << s) ) 
+                →    {w : Ordinal} → odef (UnionCF A f mf ay supf x) w → (w ≡ s) ∨ (w << s)
+             m10 {s} as b-is-sup ⟪ aa , ch-init fc ⟫ = ?
+             m10 {s} as b-is-sup ⟪ aa , ch-is-sup u {w} u<x is-sup-z fc ⟫ = m01 where
+                m01 : w <= s
+                m01 with trio< (supf u) (supf b)
+                ... | tri< a ¬b ¬c = b-is-sup ⟪ aa , ch-is-sup u {w} a is-sup-z fc ⟫ 
+                ... | tri≈ ¬a b ¬c = <=-trans  ?  ( b-is-sup ⟪ aa , ch-is-sup u {w} ? is-sup-z fc ⟫ )
+                ... | tri> ¬a ¬b c = ?
+                -- <=-trans (IsSup.x≤sup is-sup ⟪ aa , ch-is-sup u u<x is-sup-z fc ⟫) b<=s
+             m07 :  {s : Ordinal} → odef A s → ({z : Ordinal} →
+                odef (UnionCF A f mf ay supf b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
+             m07 {s} as b-is-sup = IsSup.minsup is-sup as (m10 as b-is-sup )
+
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
@@ -661,8 +682,7 @@
                     chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )
-                      ⟪ record { x≤sup = λ {z} uz → IsSup.x≤sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz)
-                          ; minsup = m07 }  , m04 ⟫ where
+                      ⟪ ?  , m04 ⟫ where
                              m10 : {s : Ordinal }  →  (odef A s ) 
                                 →  ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) ) 
                                 →    {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) z → (z ≡ s) ∨ (z << s)
@@ -784,7 +804,7 @@
              zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a <= b
              zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb ))
              ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
-             ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) 
+             ... | case2 lt = <=-trans (zc05 fb) (case2 lt) 
              zc05 (init b1 refl) with MinSUP.x≤sup (ZChain.minsup zc o≤-refl) 
                 (subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca )
              ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq )