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

changeset 1081:7089a047e49f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
strange bug of agda
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 17 Dec 2022 06:07:18 +0900
parents 11e869f92504
children 83d9000bf72f
files src/zorn.agda
diffstat 1 files changed, 85 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Dec 16 20:03:01 2022 +0900
+++ b/src/zorn.agda	Sat Dec 17 06:07:18 2022 +0900
@@ -1238,15 +1238,40 @@
 
      ... | no lim with trio< x o∅
      ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
-     ... | tri≈ ¬a b ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = ?
+     ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; 0<supfz = 0<supfz
               ; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s )
-              ; zo≤sz = ? ; 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 )
+              ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = λ a<b b≤0 → ⊥-elim ( ¬x<0 (subst (λ k → _ o< k ) x=0 (ordtrans<-≤ a<b b≤0)))    } 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 )
+          ym = MinSUP.sup (ysup f mf ay)
+          0<supfz : o∅ o< MinSUP.sup (ysup f mf ay)
+          0<supfz with trio< o∅ (MinSUP.sup (ysup f mf ay) )
+          ... | tri< a ¬b ¬c = a
+          ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ ? (MinSUP.minsup (ysup f mf ay) (proj2 (mf _ (MinSUP.as (ysup f mf ay) )))  mf01 )) where
+                mf01 : {w : Ordinal} → odef (uchain f mf ay) w → w ≤ f (MinSUP.sup (ysup f mf ay))
+                mf01 {w} uw = ≤-ftrans (MinSUP.x≤sup (ysup f mf ay) uw) (proj1 (mf _ (MinSUP.as (ysup f mf ay) )))
+          ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0  c )
+          zo≤sz : {z : Ordinal} → z o≤ x → z o≤ MinSUP.sup (ysup f mf ay)
+          zo≤sz {z} z≤x with osuc-≡< z≤x
+          ... | case1 refl = o<→≤ (subst (λ k → k o< MinSUP.sup (ysup f mf ay)) (sym x=0) 0<supfz )
+          ... | case2 lt = ⊥-elim ( ¬x<0  (subst (λ k → z o< k ) x=0 lt ) )
+          is-minsup : {z : Ordinal} → z o≤ x →
+            IsMinSUP A (UnionCF A f ay (λ _ → MinSUP.sup (ysup f mf ay)) z) (MinSUP.sup (ysup f mf ay))
+          is-minsup {z} z≤x with osuc-≡< z≤x
+          ... | case1 refl = record { as = MinSUP.as  (ysup f mf ay) ; x≤sup = λ {w} uw → is00 uw ; minsup = λ {s} as sup → is01 as sup } where
+              is00 : {w : Ordinal } → odef (UnionCF A f ay (λ _ → MinSUP.sup (ysup f mf ay)) x ) w → w ≤ MinSUP.sup (ysup f mf ay)
+              is00 {w} ⟪ aw , ch-init fc ⟫ = MinSUP.x≤sup (ysup f mf ay) fc
+              is00 {w} ⟪ aw , ch-is-sup u u<z su=u fc ⟫ = ⊥-elim (¬x<0 (subst (λ k → u o< k ) x=0 u<z ))
+              is01 : { s : Ordinal } → odef A s →  ( {w : Ordinal  } → odef (UnionCF A f ay (λ _ → MinSUP.sup (ysup f mf ay)) x )  w → w ≤ s )
+                  → ym o≤ s
+              is01 {s} as sup = MinSUP.minsup (ysup f mf ay) as is02 where
+                  is02 : {w : Ordinal } →  odef (uchain f mf ay) w → (w ≡ s) ∨ (w << s)
+                  is02 fc = sup ⟪ A∋fc _ f mf fc , ch-init fc ⟫
+          ... | case2 lt = ⊥-elim ( ¬x<0  (subst (λ k → z o< k ) x=0 lt ) )
      ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = order ; 0<supfz = 0<sufz
-              ; zo≤sz = ?   ; is-minsup = is-minsup ; cfcs = cfcs    }  where
+              ; zo≤sz = zo≤sz   ; is-minsup = is-minsup ; cfcs = cfcs    }  where
 
           mf : ≤-monotonic-f A f
           mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
@@ -1427,21 +1452,6 @@
           ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x<z )
           ... | tri> ¬a ¬b c = refl
 
-          zc11 : {z : Ordinal } → odef pchain z → odef pchainS z
-          zc11 {z} lt = ?
-
-          sfpx≤spu : {z : Ordinal } → supf1 z ≤ sps
-          sfpx≤spu {z} with trio< z x
-          ... | tri< a ¬b ¬c = ? -- MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc  (ob<x lim a)) ) refl )
-          ... | tri≈ ¬a b ¬c = case1 ?
-          ... | tri> ¬a ¬b c = case1 ?
-
-          sfpxo≤spu : {z : Ordinal } → supf1 z o≤ sps
-          sfpxo≤spu {z} with trio< z x
-          ... | tri< a ¬b ¬c = ? -- MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc  (ob<x lim a)) ) refl )
-          ... | tri≈ ¬a b ¬c = o≤-refl0 ?
-          ... | tri> ¬a ¬b c = o≤-refl0 ?
-
           asupf : {z : Ordinal } → odef A (supf1 z)
           asupf {z} with trio< z x
           ... | tri< a ¬b ¬c = ZChain.asupf (pzc  (ob<x lim a))
@@ -1588,34 +1598,78 @@
                    zc44 : FClosure A f (supf1 u) w
                    zc44 = subst (λ k → FClosure A f k w ) (sym zc45) fc
 
+
           zo≤sz : {z : Ordinal} →  z o≤ x → z o≤ supf1 z
           zo≤sz {z} z≤x with osuc-≡< z≤x
           ... | case2 z<x = subst (λ k → z o≤ k) (sym (trans (sf1=sf z<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl)))) ( ZChain.zo≤sz (pzc z<x) o≤-refl )
-          ... | case1 refl = subst (λ k → x o≤ k) (sf1=spu refl) z47 where
+          ... | case1 refl = ? where -- subst (λ k → x o≤ k) (sf1=spu refl) ? where
                z47 : x o≤ spu
                z47 with x<y∨y≤x spu x
                ... | case2 lt = lt
                ... | case1 spu<x = ⊥-elim ( <<-irr (MinSUP.x≤sup usup z48) (proj1 ( mf< spu (MinSUP.as usup))))  where
                    z49 : supfz spu<x ≡ spu
                    z49 with trio< (supfz spu<x) spu
-                   ... | tri< a ¬b ¬c = ⊥-elim ( o≤> ( IsMinSUP.minsup (is-minsup (o<→≤ spu<x)) (MinSUP.as usup) z51 ) a ) where
+                   ... | tri< a ¬b ¬c = ⊥-elim ( o≤> ( IsMinSUP.minsup (is-minsup (o<→≤ spu<x)) (MinSUP.as usup) z51 ) ? ) where
                        z51 : {w : Ordinal  } → odef (UnionCF A f ay supf1 spu)  w → w ≤ spu
                        z51 {w}  ⟪ aw , ch-init fc ⟫  = MinSUP.x≤sup usup  ⟪ aw , ic-init fc ⟫
-                       z51 {w}  ⟪ aw , ch-is-sup u u<b su=u fc  ⟫  = MinSUP.x≤sup usup ⟪ aw , ic-isup u (ordtrans u<b spu<x) ? ? ⟫
+                       z51 {w}  ⟪ aw , ch-is-sup u u<b su=u fc  ⟫  = MinSUP.x≤sup usup ⟪ aw , ic-isup u (ordtrans u<b spu<x) z55 z56 ⟫ where
+                            u<z : u o< z
+                            u<z = ordtrans u<b spu<x
+                            z57 : supfz (ordtrans u<b spu<x) ≡ u
+                            z57 = trans (trans (zeq _ _ o≤-refl (o<→≤ <-osuc) ) (sym (sf1=sf u<z))) su=u
+                            z55 : supfz (ordtrans u<b spu<x) o≤ u
+                            z55 = o≤-refl0 z57
+                            z56 : FClosure A f (supfz (ordtrans u<b spu<x)) w
+                            z56 = subst (λ k → FClosure A f k w ) (sym (trans (zeq _ _  o≤-refl (o<→≤ <-osuc) ) (sym (sf1=sf u<z)))) fc
                    ... | tri≈ ¬a b ¬c = b
-                   ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( MinSUP.minsup usup (ZChain.asupf (pzc (ob<x lim spu<x)))  z52 ) c ) where
+                   ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( MinSUP.minsup usup (ZChain.asupf (pzc (ob<x lim spu<x)))  z52 ) ? ) where
                        z52 : {w : Ordinal  } → odef pchainU  w → w ≤ supfz spu<x
                        z52 {w} uw = subst (λ k → w ≤ k ) (sf1=sf spu<x) ( IsMinSUP.x≤sup (is-minsup (o<→≤ spu<x)) z53  ) where
                             z53 : odef (UnionCF A f ay supf1 spu) w
                             z53 with pchainU⊆chain uw
                             ... |  ⟪ aw , ch-init fc ⟫  = ⟪ aw , ch-init fc ⟫
-                            ... |  ⟪ aw , ch-is-sup u u<b su=u fc  ⟫  = ⟪ aw , ch-is-sup u ? ? ?  ⟫
+                            ... |  ⟪ aw , ch-is-sup u u<b su=u fc  ⟫  = ⟪ aw , ch-is-sup u u<spu
+                                (trans (trans (sf1=sf u<z) (zeq _ _ z54 (o<→≤ <-osuc))) su=u )
+                                (subst (λ k → FClosure A f k w) (sym (trans (sf1=sf u<z) (zeq _ _ z54 (o<→≤ <-osuc))))  fc)  ⟫  where
+                               u<spu : u o< spu
+                               u<spu = ? -- ordtrans u<b (pic<x (proj2 uw))
+                               u<z : u o< z
+                               u<z = ordtrans u<spu spu<x
+                               z54 : osuc u o≤ osuc (IChain-i (proj2 uw))
+                               z54 = osucc u<b
+                                -- u<b : u o< osuc (IChain-i (proj2 uw))
                    z50 : supfz spu<x o≤ x
-                   z50 = o<→≤ ( subst (λ k → k o< x) z49 spu<x )
+                   z50 = ? -- o<→≤ ( subst (λ k → k o< x) z49 ?) -- spu<x )
                    z48 : odef pchainU (f spu)
-                   z48 = ⟪  proj2 (mf _ (MinSUP.as usup) ) , ic-isup _ (subst (λ k → k o< x) refl spu<x) z50
+                   z48 = ⟪  proj2 (mf _ (MinSUP.as usup) ) , ic-isup _ (subst (λ k → k o< x) refl spu<x) ? -- z50
                         (fsuc _ (init (ZChain.asupf (pzc (ob<x lim spu<x))) z49)) ⟫
 
+
+          supfeq1 : {a b : Ordinal } → a o≤ x →  b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b
+          supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b)
+          ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
+                IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb )
+          ... | tri≈ ¬a b ¬c = b
+          ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
+                IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa )
+
+          union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b
+          union-max1 {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
+              z47 : {w : Ordinal } → odef (UnionCF A f ay supf1 a ) w → odef ( UnionCF A f ay supf1 b ) w
+              z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+              z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
+                  u<b : u o< b
+                  u<b = ordtrans u<a (supf-inject0 supf-mono sa<sb )
+              z48 : {w : Ordinal } → odef (UnionCF A f ay supf1 b ) w → odef ( UnionCF A f ay supf1 a ) w
+              z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+              z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where
+                  u<a : u o< a
+                  u<a = supf-inject0 supf-mono ( osucprev (begin
+                     osuc (supf1 u)  ≡⟨ cong osuc su=u ⟩
+                     osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
+                     x  ≤⟨ z≤sa ⟩
+                     supf1 a ∎ )) where open o≤-Reasoning O
+
           order : {a b w : Ordinal } → b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
           order {a} {b} {w} b≤x sa<sb fc with osuc-≡< b≤x
           ... | case2 b<x = subst (λ k → w ≤ k ) (sym (trans (sf1=sf b<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl ))))  (
@@ -1627,8 +1681,8 @@
                a<b = supf-inject0 supf-mono sa<sb
                a<x : a o< x
                a<x = ordtrans<-≤ a<b b≤x
-          ... | case1 refl = zc40 (subst₂ (λ j k → j o< k) (sf1=sf a<x) (sf1=spu refl) sa<sb)
-                   (subst (λ k → FClosure A f k w) (sf1=sf a<x) fc ) where
+          ... | case1 refl = ? where -- zc40 (subst₂ (λ j k → j o< k) (sf1=sf a<x) (sf1=spu refl) sa<sb)
+                   -- (subst (λ k → FClosure A f k w) (sf1=sf a<x) fc ) where
                a<x : a o< x
                a<x = supf-inject0 supf-mono sa<sb
                zc40 : ZChain.supf (pzc  (ob<x lim a<x )) a o< spu → FClosure A f (ZChain.supf (pzc  (ob<x lim a<x )) a) w → w ≤ spu