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

changeset 709:6795b58f2f0c

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 Wed, 13 Jul 2022 21:29:53 +0900
parents 7c0aa5a9ab3f
children d20ba4b64ef3
files src/zorn.agda
diffstat 1 files changed, 37 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Jul 13 10:40:28 2022 +0900
+++ b/src/zorn.agda	Wed Jul 13 21:29:53 2022 +0900
@@ -484,8 +484,8 @@
           zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
-          zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px
-          zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
+          zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
+          zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
 
           pchain : HOD
           pchain  = UnionCF A f mf ay (ZChain.supf zc) x
@@ -520,6 +520,27 @@
           no-extenion is-max  = record { initial = pinit ; chain∋init = pcy 
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; is-max = is-max }
 
+          same-chain : ¬ (odef pchain x) → pchain ≡ UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op )
+          same-chain = ?
+
+          zcp : {a b : Ordinal} → odef pchain a → 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 b<x ab P a<b = zc6 where
+                zc7 : {z : Ordinal } → (z o< x) ∨  (z ≡ y) →  (z o< Oprev.oprev op) ∨ (z ≡ y)
+                zc7 {z} (case1 z<x) = ?
+                zc7 {z} (case2 z=y) = case2 z=y
+                zc5 : odef pchain a → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) a
+                zc5 za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = zc7 (UChain.u<x (proj2 za))  ; uchain = UChain.uchain (proj2 za)  } ⟫
+                zc2 : odef (UnionCF A f mf ay (ZChain.supf zc) px ) b
+                zc2 = ZChain.is-max zc (zc5 za) (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x) ab ? a<b
+                zc3 : (UChain.u (proj2 zc2) o< x) ∨ (UChain.u (proj2 zc2) ≡ y)
+                zc3 with UChain.u<x (proj2 zc2) 
+                ... | case1 lt = case1 (ordtrans lt px<x)
+                ... | case2 eq = case2 eq
+                zc6 : odef pchain b
+                zc6 = ⟪ ab , record { u = UChain.u (proj2 zc2) ; u<x = zc3 ; uchain = UChain.uchain (proj2 zc2) } ⟫ 
+
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip
@@ -528,17 +549,9 @@
                             * 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 = zc6 where
-                    zc5 : odef pchain a → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) a
-                    zc5 za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = ? ; uchain = UChain.uchain (proj2 za)  } ⟫
-                    zc2 : odef (UnionCF A f mf ay (ZChain.supf zc) px ) b
-                    zc2 = ZChain.is-max zc ? (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt) ab ? a<b
-                    zc3 : (UChain.u (proj2 zc2) o< x) ∨ (UChain.u (proj2 zc2) ≡ y)
-                    zc3 with UChain.u<x (proj2 zc2) 
-                    ... | case1 lt = case1 (ordtrans lt px<x)
-                    ... | case2 eq = case2 eq
-                    zc6 : odef pchain b
-                    zc6 = ⟪ ab , record { u = UChain.u (proj2 zc2) ; u<x = zc3 ; uchain = UChain.uchain (proj2 zc2) } ⟫ 
+                ... | case2 lt = zcp za lt ab P a<b where
+                     zc10 : odef pchain b
+                     zc10 = ZChain.is-max ? za ?  ab P a<b
           ... | 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
@@ -546,7 +559,7 @@
                     HasPrev A pchain ab f ∨  IsSup A pchain ab →
                             * a < * b → odef pchain b
                 zc7 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
-                ... | case2 lt = ? -- ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab P a<b
+                ... | case2 lt = zcp za lt ab P a<b
                 ... | case1 b=x = ? 
                 -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
@@ -564,9 +577,9 @@
                 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 = ? -- ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab p a<b 
-                ... | case1 b=x with p
+                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 = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = ? ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy 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 ? )  } ) 
@@ -604,6 +617,12 @@
           pcy : odef pchain y
           pcy = ⟪ ay , record { u =  y ; 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 →
+                            * a < * b → odef pchain b ) → ZChain A f mf ay x
+          no-extenion is-max  = record { initial = pinit ; chain∋init = pcy 
+              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; is-max = is-max }
+
           usup : SUP A pchain
           usup = supP pchain (λ lt → proj1 lt) ptotal
           spu = & (SUP.sup usup)
@@ -615,7 +634,7 @@
 
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
-          ... | no noax = {!!} where -- ¬ A ∋ p, just skip
+          ... | no noax = no-extenion ? where -- ¬ A ∋ p, just skip
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = {!!} where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next