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

changeset 1024:ab72526316bd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
supf-< and ZChain1.order is removed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 25 Nov 2022 18:21:08 +0900
parents 52272b5c9d58
children e4919cc0cfe8
files src/zorn.agda
diffstat 1 files changed, 8 insertions(+), 66 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Nov 25 16:57:33 2022 +0900
+++ b/src/zorn.agda	Fri Nov 25 18:21:08 2022 +0900
@@ -435,7 +435,6 @@
 
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
-      supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
       supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 
       minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x)
@@ -468,19 +467,6 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay supf ( (proj2 ca)) ( (proj2 cb))
 
-   supf-<= : {x y : Ordinal } → supf x <= supf  y → supf x o≤ supf y
-   supf-<= {x} {y} (case1 sx=sy) = o≤-refl0 sx=sy
-   supf-<= {x} {y} (case2 sx<sy) with trio< (supf x) (supf y)
-   ... | tri< a ¬b ¬c = o<→≤ a
-   ... | tri≈ ¬a b ¬c = o≤-refl0 b
-   ... | tri> ¬a ¬b c = ⊥-elim (<-irr (case2 sx<sy ) (supf-< c) )
-
-   supf-<inject : {x y : Ordinal } → supf x << supf  y → supf x o< supf y
-   supf-<inject {x} {y} sx<sy with trio< (supf x) (supf y)
-   ... | tri< a ¬b ¬c = a
-   ... | tri≈ ¬a b ¬c = ⊥-elim (<-irr (case1 (cong (*) (sym b)) ) sx<sy )
-   ... | tri> ¬a ¬b c = ⊥-elim (<-irr (case2 sx<sy ) (supf-< c) )
-
    supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y
    supf-inject {x} {y} sx<sy with trio< x y
    ... | tri< a ¬b ¬c = a
@@ -653,7 +639,6 @@
       is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z  → (ab : odef A b)
           → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsSUP A (UnionCF A f mf ay supf b) ab
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
-      order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -791,42 +776,9 @@
 
         supf = ZChain.supf zc
 
-        csupf-fc : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
-        csupf-fc {b} {s} {z1} b<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
-                s<b : s o< b
-                s<b = ZChain.supf-inject zc ss<sb
-                s<z : s o< & A
-                s<z = ordtrans s<b b<z
-                zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
-                zc04 = ZChain.csupf zc mf< (ordtrans<-≤ ss<sb (ZChain.supf-mono zc (o<→≤ b<z))) (ZChain.supf<A zc)
-                zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
-                zc05 with zc04
-                ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫
-                ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ZChain.supf-inject zc zc08) is-sup fc ⟫ where
-                    zc07 : FClosure A f (supf u) (supf s)   -- supf u ≤ supf s  → supf u o≤ supf s
-                    zc07 = fc
-                    zc06 : supf u ≡ u
-                    zc06 = ChainP.supu=u is-sup
-                    zc08 : supf u o< supf b
-                    zc08 = ordtrans≤-< (ZChain.supf-<= zc (≤to<= ( s≤fc _ f mf fc ))) ss<sb
-        csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
-                zc04 : odef (UnionCF A f mf ay supf b) (f x)
-                zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc  )
-                ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫
-                ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u<x is-sup (fsuc _ fc) ⟫
-        order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-        order {b} {s} {z1} b<z ss<sb fc = zc04 where
-          zc00 : ( z1  ≡  MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1  << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) )
-          zc00 = MinSUP.x≤sup (ZChain.minsup zc (o<→≤  b<z) ) (subst (λ k →  odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc b<z ss<sb fc ))
-          -- supf (supf b) ≡ supf b
-          zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
-          zc04 with zc00
-          ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z))  ) eq )
-          ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt )
-
         zc1 :  (x : Ordinal ) → x o≤ & A →   ZChain1 A f mf ay zc x
         zc1 x x≤A with Oprev-p x  
-        ... | yes op = record { is-max = is-max ; order = order  } where
+        ... | yes op = record { is-max = is-max } where
                px = Oprev.oprev op
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
                   b o< x → (ab : odef A b) →
@@ -835,7 +787,7 @@
                is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
                is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
                is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
-               ... | case2 sb<sx = ⟪ ab , ch-is-sup b b<x  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+               ... | case2 sb<sx = m10 where
                   b<A : b o< & A
                   b<A = z09 ab
                   m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
@@ -843,13 +795,8 @@
                         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) uz  }  , m04 ⟫
-                  m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
-                  m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
-                  m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
-                               → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
-                  m09 {s} {z} s<b fcz = order b<A s<b fcz
-                  m06 : ChainP A f mf ay supf b
-                  m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
+                  m10 : odef (UnionCF A f mf ay supf x) b
+                  m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
                   m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
@@ -869,7 +816,7 @@
                           m13 :  odef (UnionCF A f mf ay supf x) z
                           m13 = ZChain.cfcs zc mf< b<x x≤A m14 fc
 
-        ... | no lim = record { is-max = is-max ; order = order }  where
+        ... | no lim = record { is-max = is-max }  where
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
                   b o< x → (ab : odef A b) →
                   HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
@@ -879,22 +826,17 @@
                is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
                ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
                ... | case2 y<b with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
-               ... | case2 sb<sx = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+               ... | case2 sb<sx = m10 where
                   m09 : b o< & A
                   m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-                  m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
-                  m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
-                  m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
-                           → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
-                  m08 {s} {z1} s<b fc = order m09 s<b fc
                   m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
                   m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                           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<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
-                  m06 : ChainP A f mf ay supf b
-                  m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
+                  m10 : odef (UnionCF A f mf ay supf x) b
+                  m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
                   m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A