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

changeset 957:ce42b1c5cf42

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
MinSup onlu ZChain1 is-max have to be hold all b o< z, by induction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 03 Nov 2022 19:01:54 +0900
parents a2b13a4b6727
children 33891adf80ea
files src/zorn.agda
diffstat 1 files changed, 31 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Nov 03 12:11:38 2022 +0900
+++ b/src/zorn.agda	Thu Nov 03 19:01:54 2022 +0900
@@ -240,7 +240,11 @@
       ay : odef B y
       x=fy :  x ≡ f y 
 
-record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
+-- record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
+--    field
+--       x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
+
+record IsMinSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
    field
       x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
       minsup : { sup1 : Ordinal } → odef A sup1 
@@ -404,7 +408,7 @@
    field
       supf :  Ordinal → Ordinal 
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  
-           → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 
+           → IsMinSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 
 
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
@@ -467,9 +471,9 @@
 
    IsSup< : {b x : Ordinal }  (ab : odef A b ) 
           → b o< x 
-          → IsSup A (UnionCF A f mf ay supf x) ab → IsSup A (UnionCF A f mf ay supf b) ab
+          → IsMinSup A (UnionCF A f mf ay supf x) ab → IsMinSup A (UnionCF A f mf ay supf b) ab
    IsSup< {b} {x}  ab b<x is-sup = record { 
-           x≤sup =  λ {z} uz → IsSup.x≤sup is-sup (chain-mono f mf ay supf supf-mono (o<→≤ b<x) uz)
+           x≤sup =  λ {z} uz → IsMinSup.x≤sup is-sup (chain-mono f mf ay supf supf-mono (o<→≤ b<x) uz)
          ; minsup = m07 } where
              m10 : {s : Ordinal }  →  (odef A s ) 
                 →  ( {w : Ordinal} → odef (UnionCF A f mf ay supf b) w → (w ≡ s) ∨ (w << s) ) 
@@ -481,17 +485,17 @@
                 ... | tri< a ¬b ¬c = b-is-sup ⟪ aa , ch-is-sup u {w} a is-sup-z fc ⟫ 
                 ... | tri≈ ¬a b ¬c = ?
                 ... | tri> ¬a ¬b c = ?
-                -- <=-trans (IsSup.x≤sup is-sup ⟪ aa , ch-is-sup u u<x is-sup-z fc ⟫) b<=s
+                -- <=-trans (IsMinSup.x≤sup is-sup ⟪ aa , ch-is-sup u u<x is-sup-z fc ⟫) b<=s
              m07 :  {s : Ordinal} → odef A s → ({z : Ordinal} →
                 odef (UnionCF A f mf ay supf b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
-             m07 {s} as b-is-sup = IsSup.minsup is-sup as (m10 as b-is-sup )
+             m07 {s} as b-is-sup = IsMinSup.minsup is-sup as (m10 as b-is-sup )
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {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 ) → 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  
+          → HasPrev A (UnionCF A f mf ay supf z) b f ∨  IsMinSup 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)
 
@@ -667,7 +671,7 @@
            zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt  )
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
               ZChain.supf zc b o< ZChain.supf zc 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 →
+              HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsMinSup A (UnionCF A f mf ay supf b) 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 ab has-prev a<b 
@@ -682,15 +686,15 @@
                     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 (o<→≤ b<x) uz) 
+                      ⟪ record { x≤sup = λ {z} uz → IsMinSup.x≤sup (proj2 is-sup) ? -- (chain-mono1 (o<→≤ b<x) uz) 
                           ; minsup = m07 }  , m04 ⟫ where
                  m10 : {s : Ordinal }  →  (odef A s ) 
                     →  ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) ) 
-                    →    {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) z → (z ≡ s) ∨ (z << s)
+                    →    {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s)
                  m10 = ?
                  m07 :  {s : Ordinal} → odef A s → ({z : Ordinal} →
                      odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
-                 m07 {s} as s-is-sup = IsSup.minsup (proj2 is-sup) as (m10 as s-is-sup)
+                 m07 {s} as s-is-sup = ? -- IsSup.minsup (proj2 is-sup) as (m10 as s-is-sup)
               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 
@@ -701,11 +705,11 @@
         ... | no lim = record { is-max = is-max ; order = order }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
               ZChain.supf zc b o< ZChain.supf zc 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 →
+              HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsMinSup A (UnionCF A f mf ay supf b) 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 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 )
+           is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsMinSup.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
               m09 : b o< & A
@@ -723,7 +727,7 @@
                  ; 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 (o<→≤ b<x) lt )
+                      ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj2 is-sup) ? -- (chain-mono1 (o<→≤ b<x) lt )
                          ; minsup = ? } , m04 ⟫    -- ZChain on x
               m06 : ChainP A f mf ay supf b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
@@ -748,7 +752,7 @@
      record xSUP (B : HOD) (x : Ordinal) : Set n where
         field
            ax : odef A x
-           is-sup : IsSup A B ax
+           is-sup : IsMinSup A B ax
 
      --
      -- create all ZChains under o< x
@@ -1233,10 +1237,10 @@
                           zc37 : MinSUP A (UnionCF A f mf ay supf0 z)
                           zc37 = record { sup = ? ; asm = ? ; x≤sup = ? }
                  sup=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 b ≡ b
+                    b o≤ x → IsMinSup A (UnionCF A f mf ay supf0 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) b f ) → supf0 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) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj1 is-sup) lt ; minsup = ? } , proj2 is-sup ⟫ 
                  ... | tri> ¬a ¬b px<b = zc31 ? where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -1245,7 +1249,7 @@
                      zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
                      zcsup with zc30
                      ... | refl = record { ax = ab ; is-sup = record { x≤sup = λ {w} lt → 
-                        IsSup.x≤sup (proj1 is-sup) ? ; minsup = ? } } 
+                        IsMinSup.x≤sup (proj1 is-sup) ? ; minsup = ? } } 
                      zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A (UnionCF A f mf ay supf0 px) x f) → supf0 b ≡ b
                      zc31 (case1 ¬sp=x) with zc30
                      ... | refl = ⊥-elim (¬sp=x zcsup )
@@ -1337,7 +1341,7 @@
                      zc8 = ZChain.supf-is-minsup (pzc z a) {!!}
                  ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) 
-                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) b f ) → supf1 b ≡ b
+                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsMinSup A (UnionCF A f mf ay supf1 b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) b f ) → supf1 b ≡ b
                  sup=u {z} ab z≤x is-sup with trio< z x
                  ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x≤sup = {!!} }
                  ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x≤sup = {!!} }
@@ -1349,7 +1353,7 @@
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain x f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extension {!!} 
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsMinSup A pchain ax )
           ... | case1 is-sup = ? -- record { supf = supf1  ; sup=u = {!!} 
                -- ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!};  asupf = {!!}  } -- where -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention
@@ -1387,9 +1391,9 @@
            asp : odef A sp
            asp = SUP.as sp1
            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 
+              →  HasPrev A chain b f ∨  IsMinSup A (UnionCF A f mf ab (ZChain.supf zc) b) ab
               → * a < * b  → odef chain b
-           z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
+           z10 = ? -- ZChain1.is-max (SZ1 f mf as0 zc (& A) )
            z22 : sp o< & A
            z22 = z09 asp
            x≤sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 )
@@ -1403,8 +1407,8 @@
                z13 with x≤sup ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
                ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
-               z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1)
-               z19 = record {   x≤sup = z20 ; minsup = ? }  where
+               z19 : IsMinSup A (UnionCF A f mf as0 (ZChain.supf zc) sp) asp
+               z19 = record {   x≤sup = ? ; minsup = ? }  where
                    z20 :  {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
                    z20 {y} zy with x≤sup (subst (λ k → odef chain k ) (sym &iso) zy)
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
@@ -1533,7 +1537,7 @@
 
           sc=c : supf mc ≡ mc
           sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where
-              is-sup :  IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1)
+              is-sup :  IsMinSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1)
               is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )
                           ; minsup = ? } 
               not-hasprev :  ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) mc (cf nmx)
@@ -1553,7 +1557,7 @@
                    z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
                    z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc  _ fc )))
 
-          is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd)
+          is-sup : IsMinSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd)
           is-sup = record { x≤sup = z22 ; minsup = ? } where
                 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
                 z23 lt = MinSUP.x≤sup spd lt