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

changeset 920:a2f8d14012aa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixpoint?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 16 Oct 2022 17:26:49 +0900
parents 213f12f27003
children c0cf2b383064
files src/zorn.agda
diffstat 1 files changed, 18 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Oct 16 10:09:54 2022 +0900
+++ b/src/zorn.agda	Sun Oct 16 17:26:49 2022 +0900
@@ -572,14 +572,6 @@
      cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
-         (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc)
-     sp0 f mf ay zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ztotal where
-        ztotal : IsTotalOrderSet (ZChain.chain zc) 
-        ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
-               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
-
      --
      -- Second TransFinite Pass for maximality
      --
@@ -590,23 +582,22 @@
         chain-mono1 :  {a b c : Ordinal} → a o≤ b
             → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
         chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b
-        is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
-            ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
-            HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b 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 with HasPrev.ay has-prev
+        is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (ab : odef A b) 
+            → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f 
+            → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
+        is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev
         ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 
         ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
                       (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫ 
 
         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
+        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
+                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 (z09 (ZChain.asupf zc))
                 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
@@ -627,7 +618,7 @@
         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 (o<→≤ b<z) ss<sb fc ))
+          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
@@ -645,7 +636,7 @@
               HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
               * a < * b → odef (UnionCF A f mf ay supf x) b
            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 b<x ab has-prev a<b 
+           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 sb<sx ab P a<b | case2 is-sup 
              = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
               b<A : b o< & A
@@ -671,7 +662,7 @@
               HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
               * a < * b → odef (UnionCF A f mf ay supf x) b
            is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P
-           is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua sb<sx ab has-prev a<b 
+           is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b 
            is-max {a} {b} ua sb<sx 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 = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
@@ -697,6 +688,10 @@
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
+         (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc)
+     sp0 f mf {x} ay zc = ZChain.sup zc o≤-refl
+
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
             → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc  ))
      fixpoint f mf zc = z14 where
@@ -708,6 +703,8 @@
               →  HasPrev A chain b f ∨  IsSup A chain {b} ab 
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
+           z22 : & (SUP.sup sp1) o< & A
+           z22 = c<→o< ( SUP.as sp1 )
            z21 : supf (& (SUP.sup sp1)) o< supf (& A)
            z21 = ?
            -- z21 : supf (& (SUP.sup sp1)) o< & A
@@ -715,7 +712,7 @@
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1)
+           ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1)
                 (case2 z19 ) z13 where
                z13 :  * (& s) < * (& (SUP.sup sp1))
                z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc )
@@ -731,7 +728,6 @@
            ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf as0 supf ( (proj2 ca)) ( (proj2 cb)) 
-
            z14 :  f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc ))
            z14 with ztotal (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
            ... | tri< a ¬b ¬c = ⊥-elim z16 where