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

changeset 894:b09e39629d86

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, 06 Oct 2022 15:57:08 +0900
parents 290c61498d62
children aa496c232604
files src/zorn.agda
diffstat 1 files changed, 38 insertions(+), 43 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Oct 05 21:36:52 2022 +0900
+++ b/src/zorn.agda	Thu Oct 06 15:57:08 2022 +0900
@@ -262,7 +262,7 @@
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
        (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where 
     ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
-    ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) ( is-sup : ChainP A f mf ay supf u ) 
+    ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : supf u o< supf x) ( is-sup : ChainP A f mf ay supf u ) 
         ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
 --
@@ -350,7 +350,7 @@
 UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) 
     ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
 UnionCF A f mf ay supf x
-   = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf (supf x) z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+   = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )   
    → supf x o< supf y → x o<  y 
@@ -458,7 +458,7 @@
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
    field
-      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) →  b o< z  → (ab : odef A b) 
+      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) →  supf b o< supf z  → (ab : odef A b) 
           → HasPrev A (UnionCF A f mf ay supf z) b f ∨  IsSup A (UnionCF A f mf ay supf z) ab  
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
 
@@ -598,13 +598,12 @@
             → 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) a≤b
         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) →
+            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
         ... | ⟪ 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) (ZChain.supf zc x) k )
+        ... | ⟪ 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
@@ -620,19 +619,13 @@
                 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 zc10 is-sup fc ⟫ where
+                ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u 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 : u o≤ supf s  
-                    zc08 = subst (λ k → k o≤ supf s) zc06 (ZChain.supf-<= zc (≤to<= ( s≤fc _ f mf fc )))
-                    zc09 : u o≤ supf s  →  u o< b 
-                    zc09 u≤s with osuc-≡< u≤s
-                    ... | case1 u=ss = ZChain.supf-inject zc (subst (λ k → k o< supf b) (sym (trans zc06 u=ss)) ss<sb )
-                    ... | case2 u<ss = ordtrans (ZChain.supf-inject zc (subst (λ k → k o< supf s) (sym zc06) u<ss)) s<b
-                    zc10 : u o< supf b
-                    zc10 = ordtrans≤-< zc08 ss<sb
+                    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  )
@@ -654,24 +647,23 @@
            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) →
+           is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
+              supf b o< supf x → (ab : odef A b) →
               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 | case2 is-sup 
-             = ⟪ ab , ch-is-sup b b<sfx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+             = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
               b<A : b o< & A
               b<A = z09 ab
-              b<sfx : b o< ZChain.supf zc x
-              b<sfx = ?
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
-              m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) (HasPrev.ay  nhp) 
+              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<→≤ (z09 ab) )
-                      ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) uz )  }  , m04 ⟫
+                      ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) 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 
@@ -681,29 +673,29 @@
               m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
         ... | 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) →
+              supf b o< supf x → (ab : odef A b) →
               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 | 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 b<sfx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+           ... | case2 y<b = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-              b<sfx : b o< ZChain.supf zc x
-              b<sfx = ? 
               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) b f
-              m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) (HasPrev.ay  nhp) 
+              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) (chain-mono1 (ZChain.supf-mono zc (o<→≤ b<x)) lt )} , m04 ⟫    -- ZChain on x
+                      ⟪ record { x<sup = λ lt → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) lt )} 
+                           , m04 ⟫    -- ZChain on x
               m06 : ChainP A f mf ay supf b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
@@ -714,13 +706,16 @@
             → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc  ))
      fixpoint f mf zc = z14 where
            chain = ZChain.chain zc
+           supf = ZChain.supf zc
            sp1 = sp0 f mf as0 zc 
-           z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) 
-              →  HasPrev A chain b f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
+           z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) 
+              →  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) )
-           z21 : & (SUP.sup sp1) o< & A
-           z21 = c<→o< ( SUP.as sp1)
+           z21 : supf (& (SUP.sup sp1)) o< supf (& A)
+           z21 with osuc-≡< ( ZChain.supf-mono zc (o<→≤ (c<→o< ( SUP.as sp1))) )
+           ... | case2 lt = lt
+           ... | case1 eq = ?
            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 )
@@ -736,11 +731,10 @@
                    z20 {y} zy with SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) zy)
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
                    ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
-                   -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ?  (SUP.x<sup sp1 ? ) }
            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 as0 (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
+               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 
@@ -836,7 +830,7 @@
           ... | case1 eq = case2 eq
           ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
 
-          zc4 : ZChain A f mf ay x
+          zc4 : ZChain A f mf ay x     --- supf px ≤ supf x
           zc4 with osuc-≡< ?
           ... | case1 sfpx=px = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf-mono1 ; supf-< = supf-<1  
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = ?    }  where
@@ -846,15 +840,15 @@
                  --     supf px is MinSUP of previous chain , supf x ≡ MinSUP of Union of UChain and  FClosure px 
 
                  pchainpx : HOD
-                 pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 (supf0 px) z ) ∨ FClosure A f px z  } ; odmax = & A ; <odmax = zc00 } where
-                      zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 (supf0 px) z ) ∨ FClosure A f px z → z o< & A
+                 pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z  } ; odmax = & A ; <odmax = zc00 } where
+                      zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → z o< & A
                       zc00 {z} (case1 lt) = z07 lt 
                       zc00 {z} (case2 fc) = z09 ( A∋fc px f mf fc )
-                 zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 (supf0 px) z ) ∨ FClosure A f px z → odef A z
+                 zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → odef A z
                  zc01 {z} (case1 lt) = proj1 lt 
                  zc01 {z} (case2 fc) = ( A∋fc px f mf fc )
 
-                 zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 (supf0 px) a → FClosure A f px b → a <= b
+                 zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f px b → a <= b
                  zc02 {a} {b} ca fb = zc05 fb where
                     zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ px
                     zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) (sym sfpx=px)
@@ -862,7 +856,8 @@
                     zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc 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) 
-                    zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) (subst (λ k → odef A k ∧ UChain A f mf ay supf0 (supf0 px) k) (sym &iso) ca )
+                    zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) ? --
+                       -- (subst (λ k → odef A k ∧ UChain A f mf ay supf0 (supf0 px) k) (sym &iso) ca )
                     ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq )
                     ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt ) 
 
@@ -1160,11 +1155,11 @@
 
                  zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
                  zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x ?) ?  ?  ⟫
+                 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ?  ?  ⟫
 
                  zc111 : {z : Ordinal} → z o< px → OD.def (od pchain1) z → OD.def (od pchain) z 
                  zc111 {z} z<px ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                 zc111 {z} z<px ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x ?) ?  ?  ⟫
+                 zc111 {z} z<px ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ?  ?  ⟫
 
                  zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  (HasPrev A pchain x f )
                         → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z )
@@ -1193,7 +1188,7 @@
                                  zc14 : u ≡ osuc px
                                  zc14 = begin
                                     u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩ 
-                                    supf0 u ≡⟨ eq1 ⟩ 
+                                    supf0 u ≡⟨ ? ⟩ 
                                     supf0 u1 ≡⟨ s1u=x ⟩ 
                                     x ≡⟨ sym (Oprev.oprev=x op) ⟩ 
                                     osuc px ∎ where open ≡-Reasoning