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

changeset 1058:12ce8d0224d2

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 Sat, 10 Dec 2022 09:56:32 +0900
parents cd3237120dec
children bd2a258f309c
files src/zorn.agda
diffstat 1 files changed, 45 insertions(+), 58 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Dec 10 07:01:34 2022 +0900
+++ b/src/zorn.agda	Sat Dec 10 09:56:32 2022 +0900
@@ -341,15 +341,15 @@
 
       is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x)
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
-           → IsSUP A (UnionCF A f ay supf b) b ∧ (¬ HasPrev A (UnionCF A f ay supf b) f b ) → supf b ≡ b
+           → IsSUP A (UnionCF A f ay supf b) b → supf b ≡ b
 
    chain : HOD
    chain = UnionCF A f ay supf z
    chain⊆A : chain ⊆' A
    chain⊆A = λ lt → proj1 lt
 
-   chain∋init : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) y
-   chain∋init {x} x≤z = ⟪ ay , ch-init (init ay refl)  ⟫
+   chain∋init : {x : Ordinal } → odef (UnionCF A f ay supf x) y
+   chain∋init {x} = ⟪ ay , ch-init (init ay refl)  ⟫
 
    mf : ≤-monotonic-f A f
    mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
@@ -430,25 +430,6 @@
    f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ =
       subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso  (fcn-cmp y f mf fca fcb )
 
-   IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp
-       → ({y : Ordinal} → odef (UnionCF A f ay supf x) y → (y ≡ sp ) ∨ (y << sp ))
-       → ( {a : Ordinal } → odef A a → a << f a )
-       → ¬ ( HasPrev A (UnionCF A f ay supf x) f sp )
-   IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<<-irr fsp≤sp sp<fsp ) where
-       sp<fsp : sp << f sp
-       sp<fsp = <-mono-f asp
-       pr = HasPrev.y hp
-       im00 : f (f pr) ≤ sp
-       im00 = is-sup ( f-next (f-next (HasPrev.ay hp)))
-       fsp≤sp : f sp ≤  sp
-       fsp≤sp = subst (λ k → f k ≤ sp ) (sym (HasPrev.x=fy hp)) im00
-
-   supf-¬hp : {x  : Ordinal } → x o≤ z
-       → ( {a : Ordinal } → odef A a → a << f a )
-       → ¬ ( HasPrev A (UnionCF A f ay supf x) f (supf x) )
-   supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw →
-       (subst (λ k → w ≤ k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp
-
    supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
    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)
@@ -457,7 +438,7 @@
                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
-       z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf  ; x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫
+       z52 = sup=u asupf sfb≤x  record { ax = asupf  ; x≤sup = z54  } 
 
    x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x 
    x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x
@@ -470,6 +451,17 @@
          z45 : f (supf x) ≤ supf x
          z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46 
 
+   sup=u0 : {b : Ordinal} → (ab : odef A b) → b o≤ z
+       → IsSUP A (UnionCF A f ay supf b) b  → supf b ≡ b
+   sup=u0 {b} ab b≤z is-sup with trio< (supf b) b
+   ... | tri< sb<b ¬b ¬c = ⊥-elim ( o≤> z47 sb<b ) where
+         z47 : b o≤ supf b
+         z47 = x≤supfx b≤z ?
+   ... | tri≈ ¬a b ¬c = b
+   ... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb ) where
+         z48 : supf b o≤ b
+         z48 = IsMinSUP.minsup (is-minsup b≤z) ab (λ ux → IsSUP.x≤sup is-sup ux )
+
    supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b 
    supf-mono< {a} {b} b≤z sa<sb  with order {a} {b} b≤z sa<sb (init asupf refl)
    ... | case2 lt = lt
@@ -708,11 +700,8 @@
                ... | case2 sb<sx = m10 where
                   b<A : b o< & A
                   b<A = z09 ab
-                  m04 : ¬ HasPrev A (UnionCF A f 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<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
+                  m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )  record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  } 
                   m10 : odef (UnionCF A f ay supf x) b
                   m10 = ZChain.cfcs zc 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
@@ -728,7 +717,7 @@
                           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 { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
+                          m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )  record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
                           m13 :  odef (UnionCF A f ay supf x) z
@@ -741,18 +730,14 @@
                   * a < * b → odef (UnionCF A f 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 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) (ZChain.chain∋init zc (ordtrans b<x x≤A) )
+               is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (ZChain.chain∋init zc  )
                ... | 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 = m10 where
                   m09 : b o< & A
                   m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-                  m04 : ¬ HasPrev A (UnionCF A f 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 { ax = ab ; x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
+                  m05 = ZChain.sup=u zc ab (o<→≤  m09) record { ax = ab ; x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } 
                   m10 : odef (UnionCF A f ay supf x) b
                   m10 = ZChain.cfcs zc 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
@@ -764,11 +749,7 @@
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
-                          m04 : ¬ HasPrev A (UnionCF A f 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<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
+                          m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } 
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
                           m13 :  odef (UnionCF A f ay supf x) z
@@ -1137,22 +1118,21 @@
                                 u≤px = ordtrans u<x z≤px
 
                  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
+                    b o≤ x → IsSUP A (UnionCF A f ay supf1 b) b  → supf1 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ zc40 , ZChain.IsMinSUP→NotHasPrev zc ab zc42 (λ ax → proj1 (mf< _ ax))  ⟫ where
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a)  zc40 where
                      zc42 : {w : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) b) w → w ≤ b
-                     zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup (proj1 is-sup)  ⟪ ua , ch-init fc ⟫ 
-                     zc42 {w} ⟪ ua ,  ch-is-sup u u<x su=u fc  ⟫ = IsSUP.x≤sup (proj1 is-sup) ⟪ ua ,  
+                     zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup is-sup  ⟪ ua , ch-init fc ⟫ 
+                     zc42 {w} ⟪ ua ,  ch-is-sup u u<x su=u fc  ⟫ = IsSUP.x≤sup is-sup ⟪ ua ,  
                          ch-is-sup u u<x (trans (sf1=sf0 zc44) su=u) (fcpu fc zc44)  ⟫ where
                            zc44 : u o≤ px
                            zc44 = ordtrans u<x (o<→≤ a)
                      zc40 : IsSUP A (UnionCF A f ay supf0 b) b
                      zc40 = record { ax = ab ; x≤sup = zc42 } 
-                 ... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ab (o≤-refl0 b=px) ⟪ record { ax = ab ; x≤sup = zc42 } , 
-                                ZChain.IsMinSUP→NotHasPrev zc ab zc42 (λ ax → proj1 (mf< _ ax))  ⟫ where
+                 ... | tri≈ ¬a b=px ¬c = ZChain.sup=u zc ab (o≤-refl0 b=px)  record { ax = ab ; x≤sup = zc42 } where
                      zc42 : {w : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) b) w → w ≤ b
-                     zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup (proj1 is-sup)  ⟪ ua , ch-init fc ⟫ 
-                     zc42 {w} ⟪ ua ,  ch-is-sup u u<x su=u fc  ⟫ = IsSUP.x≤sup (proj1 is-sup) ⟪ ua ,  
+                     zc42 {w} ⟪ ua , ch-init fc ⟫ = IsSUP.x≤sup is-sup  ⟪ ua , ch-init fc ⟫ 
+                     zc42 {w} ⟪ ua ,  ch-is-sup u u<x su=u fc  ⟫ = IsSUP.x≤sup is-sup ⟪ ua ,  
                          ch-is-sup u u<x (trans (sf1=sf0 zc44) su=u) (fcpu fc zc44)  ⟫ where
                            zc44 : u o≤ px
                            zc44 = o<→≤ ( subst (λ k → u o< k ) b=px u<x )
@@ -1164,15 +1144,15 @@
                      zc31 : sp1 o≤ b
                      zc31 = MinSUP.minsup sup1 ab zc32 where
                          zc32 : {w : Ordinal } → odef pchainpx w → (w ≡ b) ∨ (w << b)
-                         zc32 {w} (case1 ⟪ ua , ch-init fc ⟫ ) = IsSUP.x≤sup (proj1 is-sup) ⟪ ua , ch-init fc ⟫
-                         zc32 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc ⟫ ) = IsSUP.x≤sup (proj1 is-sup) ⟪ ua , ch-is-sup u z01 z02 z03 ⟫ where
+                         zc32 {w} (case1 ⟪ ua , ch-init fc ⟫ ) = IsSUP.x≤sup is-sup ⟪ ua , ch-init fc ⟫
+                         zc32 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc ⟫ ) = IsSUP.x≤sup is-sup ⟪ ua , ch-is-sup u z01 z02 z03 ⟫ where
                              z01 : u o< b 
                              z01 = ordtrans u<x (subst (λ k → px o< k ) x=b px<x )
                              z02 : supf1 u ≡ u
                              z02 = trans (sf1=sf0 (o<→≤ u<x)) su=u
                              z03 : FClosure A f (supf1 u) w
                              z03 = fcpu fc (o<→≤ u<x)
-                         zc32 {w} (case2 fc) = IsSUP.x≤sup (proj1 is-sup) ⟪ A∋fc _ f mf (proj1 fc) , ch-is-sup (supf0 px) sa<x su=u fc1 ⟫ where
+                         zc32 {w} (case2 fc) = IsSUP.x≤sup is-sup ⟪ A∋fc _ f mf (proj1 fc) , ch-is-sup (supf0 px) sa<x su=u fc1 ⟫ where
                              su=u : supf1 (supf0 px) ≡ supf0 px
                              su=u = trans (sf1=sf0 (zc-b<x _ (proj2 fc))) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ (proj2 fc)) )
                              fc1 : FClosure A f (supf1 (supf0 px)) w
@@ -1305,8 +1285,13 @@
 
      ... | no lim with trio< x o∅
      ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
-     ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ?
-              ; supfmax = ? ; is-minsup = ? ; cfcs = ?    }
+     ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; sup=u = ? ; asupf = MinSUP.as (ysup f mf ay) 
+              ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s )
+              ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ?    } where
+              mf : ≤-monotonic-f A f
+              mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
+                 mf00 : * x < * (f x)
+                 mf00 = proj1 ( mf< x ax )
      ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
               ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
 
@@ -1471,7 +1456,8 @@
                zcm = ZChain.cfcs (pzc  (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
                zc40 : odef (UnionCF A f ay supf1 b) w
                zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
-               ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫
+               ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
+               ... | ⟪ az , ch-is-sup u u<x su=u fc ⟫ = ⟪ az , ch-is-sup u ? ? ?  ⟫
           ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           cfcs {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where
@@ -1485,10 +1471,11 @@
                zcb = ZChain.cfcs (pzc (ob<x lim b<x)) a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb
                zc40 : odef (UnionCF A f ay supf1 b) w
                zc40 with zcb
-               ... | ⟪ az , cp  ⟫ = ⟪ az , ? ⟫
+               ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
+               ... | ⟪ az , ch-is-sup u u<x su=u fc ⟫ = ⟪ az , ch-is-sup u ? ? ?  ⟫
 
           sup=u : {b : Ordinal} (ab : odef A b) →
-                b o≤ x → IsMinSUP A (UnionCF A f ay supf1 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf1 b) f b ) → supf1 b ≡ b
+                b o≤ x → IsMinSUP A (UnionCF A f ay supf1 b) b  → supf1 b ≡ b
           sup=u {b} ab b≤x is-sup with osuc-≡< b≤x
           ... | case1 b=x = ? where
                  zc31 : spu o≤ b
@@ -1527,10 +1514,10 @@
            z22 = z09 asp
            z12 : odef chain sp
            z12 with o≡? (& s) sp
-           ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ? )
-           ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ? ) (z09 asp) asp (case2 z19 ) z13 where
+           ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
+           ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ) (z09 asp) asp (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
-               z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc ? )
+               z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne eq )
                ... | case2 lt = lt
                z19 : IsSUP A (UnionCF A f ay (ZChain.supf zc) sp) sp