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

changeset 782:e8cf9c453431

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 Mon, 01 Aug 2022 09:38:00 +0900
parents 460df9965d63
children 195c3c7de021
files src/zorn.agda
diffstat 1 files changed, 86 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Jul 31 19:45:40 2022 +0900
+++ b/src/zorn.agda	Mon Aug 01 09:38:00 2022 +0900
@@ -265,6 +265,8 @@
       sup : HOD
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
+      min-sup : {z : HOD } → B ∋ z → ( {x : HOD } → B ∋ x → (x ≡ z ) ∨ (x < z ) ) 
+          → (z ≡ sup ) ∨ (sup < z )  
 
 --
 --  sup and its fclosure is in a chain HOD
@@ -281,10 +283,6 @@
 -- Union of supf z which o< x
 --
 
---     data DChain  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : (z : Ordinal) → Set n where
---        dinit :  DChain f mf ay (& (SUP.sup (ysup f mf ay)))
---        dsuc  : {u : Ordinal } → (au : odef A u) → DChain  f mf ay u → DChain f mf ay ( & (SUP.sup (ysup f mf au)) )
-
 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
@@ -312,9 +310,30 @@
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
 
+      sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
+      supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
       sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
+      csupf : (z : Ordinal ) → odef chain (supf z) 
+      csupf' : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
       fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
       order : {b sup1 z1 : Ordinal} → b o< z → supf sup1 o< supf b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+   supf∈A : {u : Ordinal } → odef A (supf u)
+   supf∈A = ?
+   fcy<sup'  : {u w : Ordinal } → u o< z  → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
+   fcy<sup'  {u} {w} u<z fc with SUP.x<sup (sup ?) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} init f mf fc)  , ? ⟫ 
+   ... | case1 eq = ?
+   ... | case2 lt = ?
+   fc∈A : {s z1 : Ordinal} → FClosure A f (supf s) z1 → odef chain z1
+   fc∈A {s} (fsuc x fc) = f-next (fc∈A {s} fc )  -- (supf s) ≡ z1 → init (supf s)
+   order' : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+   order' {b} {s} {z1} b<z sf<sb fc with SUP.x<sup (sup (o<→≤ b<z)) (subst (λ k → odef (UnionCF A f mf ay supf b) k) (sym &iso) ( csupf' (o<→≤ b<z)) )
+   ... | case1 eq = case1 (begin
+     ? ≡⟨ ? ⟩
+     ? ∎ ) where open ≡-Reasoning
+   ... | case2 lt = case2 ? where
+        zc00 : ?
+        zc00 = ?
+   -- case2 ( subst (λ k → * z1 < k ) (subst₂ (λ j k → j ≡ k )  *iso ? (cong (*) (sym supf-is-sup)))  lt )
 
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
@@ -330,6 +349,26 @@
       A∋maximal : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
+-- 
+
+supf-unique : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)  
+        → {a b : Ordinal } → a o< b
+        → (za : ZChain A f mf ay (osuc a) ) → (zb : ZChain A f mf ay (osuc b) )
+        → odef (UnionCF A f mf ay (ZChain.supf za) (osuc a)) (ZChain.supf za a) 
+        → odef (UnionCF A f mf ay (ZChain.supf zb) (osuc b)) (ZChain.supf zb a) → ZChain.supf za a ≡ ZChain.supf zb a 
+supf-unique A f mf {y} ay {a} {b} a<b za zb ⟪ aa , ch-init fca ⟫ ⟪ ab , ch-init fcb ⟫ = ? where
+       supf = ZChain.supf za
+       supb = ZChain.supf zb
+       su00 :  {u w : Ordinal } → u o< osuc a  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) 
+       su00 = ZChain.fcy<sup za
+       su01 :  (supf a ≡ supb b ) ∨ ( supf a << supb b ) 
+       su01 = ZChain.fcy<sup zb <-osuc fca
+       su02 :  (supb a ≡ supf a ) ∨ ( supb a << supf a ) 
+       su02 = ZChain.fcy<sup za <-osuc fcb
+supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-init fca ⟫ ⟪ ab , ch-is-sup ub is-supb fcb ⟫ = ?
+supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-is-sup ua is-supa fca ⟫ ⟪ ab , ch-init fcb ⟫ = ?
+supf-unique A f mf {y} ay {a} a<b za zb ⟪ aa , ch-is-sup ua is-supa fca ⟫ ⟪ ab , ch-is-sup ub is-supb fcb ⟫ = ?
+
 -- data UChain is total
 
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
@@ -474,11 +513,11 @@
      SZ1 :( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
      SZ1 A f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
-        chain-mono2 : (x : Ordinal) {a b c : Ordinal} → a o≤ b → b o≤ x →
+        chain-mono1 : (x : Ordinal) {a b c : Ordinal} → 
             odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
-        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , ch-init fc  ⟫ = 
+        chain-mono1 x {a} {b} {c} ⟪ ua , ch-init fc  ⟫ = 
             ⟪ ua , ch-init fc  ⟫ 
-        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ uaa ,  ch-is-sup ua is-sup fc  ⟫ = 
+        chain-mono1 x {a} {b} {c} ⟪ uaa ,  ch-is-sup ua is-sup fc  ⟫ = 
             ⟪ uaa , ch-is-sup ua  is-sup fc  ⟫ 
         chain<ZA : {x : Ordinal } → UnionCF A f mf ay (ZChain.supf zc) x ⊆' UnionCF A f mf ay (ZChain.supf zc) (& A)
         chain<ZA {x} ux with proj2 ux
@@ -512,20 +551,20 @@
                  m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
                  m01 with trio< b px    --- px  < b < x
                  ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)
-                 ... | tri< b<px ¬b ¬c = chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl m04 where
+                 ... | tri< b<px ¬b ¬c = chain-mono1 x m04 where
                     m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a -- if a ∈ chain of px, is-max of px can be used
                     m03 with proj2 ua
                     ... | ch-init fc = ⟪ proj1 ua ,  ch-init fc ⟫
                     ... | ch-is-sup u is-sup-a fc = ⟪ proj1 ua , ch-is-sup u  is-sup-a fc ⟫
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
-                         (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
+                         (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono1 x lt)  } ) a<b
                  ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫   where
                     b<A : b o< & A
                     b<A = z09 ab
                     m05 : b ≡ ZChain.supf zc b
                     m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
-                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono2 x (osucc b<x) o≤-refl uz )  }  )
+                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 x uz )  }  )
                     m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
                     m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
                     m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
@@ -540,9 +579,9 @@
               * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay )
-           ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA (chain-mono2 (osuc x) (o<→≤ <-osuc ) o≤-refl ua )) )
+           ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA {x} (chain-mono1 (osuc x) ua )) )
                        (subst (λ k → * a < * k ) (sym b=y) a<b ) )
-           ... | case2 y<b = chain-mono2 x (o<→≤ (ob<x lim b<x) ) o≤-refl m04 where
+           ... | case2 y<b = chain-mono1 x m04 where
                  m09 : b o< & A
                  m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
                  m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
@@ -552,7 +591,7 @@
                  m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
                  m05 : b ≡ ZChain.supf zc b
                  m05 = sym (ZChain.sup=u zc ab m09
-                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<x)) o≤-refl lt )} )   -- ZChain on x
+                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 x lt )} )   -- ZChain on x
                  m06 : ChainP A f mf ay (ZChain.supf zc) b b
                  m06 = record { fcy<sup = m07 ;  order = m08 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
@@ -717,6 +756,11 @@
 
           supf0 = ZChain.supf zc
 
+          csupf : (z : Ordinal) → odef (UnionCF A f mf ay supf0 x) (supf0 z)
+          csupf z with ZChain.csupf zc z
+          ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+          ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , ch-is-sup u is-sup fc ⟫ 
+
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extension : ZChain A f mf ay x
@@ -796,6 +840,13 @@
                    szc = pzc (osuc s) (ob<x lim s<x)
                    zc23 :  ZChain.supf (pzc (osuc s) (ob<x lim s<x)) s ≡ ZChain.supf (pzc (osuc b) (ob<x lim a)) s
                    zc23 = ?
+                   zc24 : odef (UnionCF A f mf ay (ZChain.supf (pzc (osuc s) (ob<x lim s<x))) (osuc s)) 
+                                (ZChain.supf (pzc (osuc s) (ob<x lim s<x)) s )
+                   zc24 = ZChain.csupf (pzc (osuc s) (ob<x lim s<x)) s
+                   zc25 : odef (UnionCF A f mf ay (ZChain.supf (pzc (osuc b) (ob<x lim a))) (osuc b)) 
+                                (ZChain.supf (pzc (osuc b) (ob<x lim a)) b )
+                   zc25 = ZChain.csupf (pzc (osuc b) (ob<x lim a)) b
+
                ... | tri≈ ¬a b ¬c = ?
                ... | tri> ¬a ¬b c = ?
                zc21 :  ZChain.supf uzc s o< ZChain.supf uzc b
@@ -805,6 +856,28 @@
           ... | tri≈ ¬a b ¬c = ⊥-elim (¬a b<x)
           ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x)
 
+          csupf : (z : Ordinal) → odef (UnionCF A f mf ay psupf x) (psupf z)
+          csupf z with trio< z x | inspect psupf z
+          ... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where
+                ozc = pzc (osuc z) (ob<x lim z<x)
+                zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
+                zc12  = ZChain.csupf ozc z
+                zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
+                zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az) ) ⟫ where
+                      az : odef A ( ZChain.supf ozc z )
+                      az = proj1 zc12
+                      zc20 : {z1  : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
+                      zc20 {z1} fc with ZChain.fcy<sup ozc <-osuc fc
+                      ... | case1 eq = case1 (trans eq (sym eq1) )
+                      ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
+                      cp1 : ChainP A f mf ay psupf z (ZChain.supf ozc z)
+                      cp1 = record {  fcy<sup = zc20   ; order = order z<x  }
+                     ---  u = supf u = supf z 
+          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup {!!} {!!} {!!} ⟫ where
+                sa = SUP.A∋maximal usup
+          ... | tri> ¬a ¬b c | record { eq = eq1 } = {!!}
+
+
           fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ psupf u) ∨ (w << psupf u)
           fcy<sup {u} {w} u<x fc with trio< u x 
           ... | tri< a ¬b ¬c = ZChain.fcy<sup uzc <-osuc fc where