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

changeset 711:b1d468186e68

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial chain?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 15 Jul 2022 05:52:23 +0900
parents d20ba4b64ef3
children 92275389e623
files src/zorn.agda
diffstat 1 files changed, 72 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Jul 14 06:00:18 2022 +0900
+++ b/src/zorn.agda	Fri Jul 15 05:52:23 2022 +0900
@@ -255,7 +255,7 @@
       order    : {sup1 z1 : Ordinal} → (lt : sup1 o< sup ) → FClosure A f (supf sup1 ) z1 → z1 << supf sup
 
 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) : Ordinal →  Ordinal → Set n where
-    ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay supf y z 
+    ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay supf o∅ z 
     ch-is-sup : {sup z : Ordinal } 
          → ( is-sup : ChainP A f mf ay supf sup z)
          → ( fc : FClosure A f (supf sup) z ) → Chain A f mf ay supf sup z
@@ -267,7 +267,7 @@
        (supf : Ordinal → Ordinal) (x : Ordinal)  (z : Ordinal) : Set n where 
    field
       u : Ordinal
-      u<x : (u o< x ) ∨ ( u ≡ y )
+      u<x : (u o< x ) ∨ ( u ≡ o∅)
       uchain : Chain A f mf ay supf u z
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -468,6 +468,36 @@
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total
           c = & (SUP.sup sp1)
 
+     inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
+     inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy
+      ; initial = isy ; f-next = inext ; f-total = itotal ; is-max = imax } where
+          isupf : Ordinal → Ordinal
+          isupf z = y
+          cy : odef (UnionCF A f mf ay isupf o∅) y
+          cy = ⟪ ay , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  } ⟫
+          isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
+          isy {z} ⟪ az , uz ⟫ with UChain.uchain uz 
+          ... | ch-init z fc = s≤fc y f mf fc 
+          ... | ch-is-sup is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
+          inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
+          inext {a} ua with UChain.uchain (proj2 ua)
+          ... | ch-init a fc = ⟪ proj2 (mf _ (proj1 ua))  , record { u = o∅ ; u<x = case2 refl ; uchain = ch-init _ (fsuc _ fc ) } ⟫
+          ... | ch-is-sup is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
+          itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 
+          itotal {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 ay isupf (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
+          imax : {a b : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a →
+            b o< osuc o∅ → (ab : odef A b) →
+            HasPrev A (UnionCF A f mf ay isupf o∅) ab f ∨ IsSup A (UnionCF A f mf ay isupf o∅) ab →
+            * a < * b → odef (UnionCF A f mf ay isupf o∅) b
+          imax {a} {b} ua b<ox ab (case1 hasp) a<b = subst (λ k → odef  (UnionCF A f mf ay isupf o∅) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
+          imax {a} {b} ua b<ox ab (case2 sup)  a<b = ?
+          -- with IsSup.x<sup sup (inext 
+          -- ... | case1 a=b = ?
+          -- ... | case2 a<b = ?
+          -- ⊥-elim ( <-irr (case2 ? ) ( IsSup  ) )
+
      --
      -- create all ZChains under o< x
      --
@@ -510,7 +540,7 @@
                zc7 : y << (ZChain.supf zc) (UChain.u ua)
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
-          pcy = ⟪ ay , record { u =  y ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
+          pcy = ⟪ ay , record { u =  o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
@@ -531,10 +561,14 @@
 
           chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain
           chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = zc11 ; uchain = UChain.uchain (proj2 za)  }  ⟫ where
-              zc11 : (UChain.u (proj2 za) o< x) ∨ (UChain.u (proj2 za) ≡ y)
+              zc11 : (UChain.u (proj2 za) o< x) ∨ (UChain.u (proj2 za) ≡ o∅)
               zc11 with UChain.u<x (proj2 za)
               ... | case1 z<x = case1 (ordtrans z<x px<x )
-              ... | case2 z=y = case2 z=y
+              ... | case2 z=0 = case2 z=0
+
+          chain-≡ : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) 
+             → pchain ≡ UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) 
+          chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
@@ -544,9 +578,14 @@
                             * a < * b → odef pchain b
                 zc1 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
-                ... | case2 lt = zcp za ? lt ab P a<b where
-                     zc10 : odef pchain b
-                     zc10 = ZChain.is-max ? za ?  ab P a<b
+                ... | case2 lt = zcp za (chain-≡ zc10) lt ab P a<b where
+                     zc10 : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)
+                     zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
+                                   ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ 
+                     zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ = 
+                                   ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-init z fc } ⟫ 
+                     zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = 
+                                   ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-is-sup is-sup fc } ⟫ 
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extenion ? where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
@@ -611,7 +650,7 @@
                zc7 : y << psupf0 (UChain.u ua)
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
-          pcy = ⟪ ay , record { u =  y ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
+          pcy = ⟪ ay , record { u =  o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
 
           no-extenion : ( {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
                     HasPrev A pchain ab f ∨  IsSup A pchain ab →
@@ -628,13 +667,19 @@
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
 
-          zcp : {a b : Ordinal} → odef pchain a 
-              → pchain ≡ UnionCF A f mf ay psupf x
+          uzc : {a : Ordinal } → (za : odef pchain a) → ZChain A f mf ay (UChain.u (proj2 za))
+          uzc {a} za with UChain.u<x (proj2 za)
+          ... | case1 u<x = pzc _ u<x
+          ... | case2 u=0 = ?
+
+          zcp : {a b : Ordinal} → (za : odef pchain a )
+              → pchain ≡ ?
               → b o< x → (ab : odef A b) 
               → HasPrev A pchain ab f ∨  IsSup A pchain ab 
               → * a < * b → odef pchain b
           zcp {a} {b} za cheq b<x ab P a<b = ? where
-              zc12 = ZChain.is-max (pzc _ ? ) ? ? ab 
+              zc12 : odef ? b
+              zc12 = ZChain.is-max (pzc _ ?) ? ? ab 
                        (subst (λ k → HasPrev A k ab f ∨  IsSup A k ab ) ? P)  a<b 
 
           chain-mono : pchain ⊆'  UnionCF A f mf ay psupf x  
@@ -644,6 +689,10 @@
               ... | ch-init .a x = ch-init a x
               ... | ch-is-sup is-sup fc = ch-is-sup ? ?
 
+          chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain 
+             → UnionCF A f mf ay psupf x ≡ pchain 
+          chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
+
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extenion ? where -- ¬ A ∋ p, just skip
@@ -652,7 +701,17 @@
           ... | case1 pr = {!!} where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
           ... | case1 is-sup = {!!} -- x is a sup of (zc ?) 
-          ... | case2 ¬x=sup =  {!!} -- no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
+          ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
+                z18 :  {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
+                            HasPrev A pchain ab f ∨ IsSup A pchain   ab →
+                            * a < * b → odef pchain b
+                z18 {a} {b} za b<x ab P a<b with osuc-≡< b<x
+                ... | case2 lt = zcp za ? lt ab P a<b
+                ... | case1 b=x with P
+                ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )
+                ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
+                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) 
+                          (IsSup.x<sup b=sup ? )  } ) 
 
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)