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

changeset 710:d20ba4b64ef3

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 Thu, 14 Jul 2022 06:00:18 +0900
parents 6795b58f2f0c
children b1d468186e68
files src/zorn.agda
diffstat 1 files changed, 36 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Jul 13 21:29:53 2022 +0900
+++ b/src/zorn.agda	Thu Jul 14 06:00:18 2022 +0900
@@ -520,26 +520,21 @@
           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 
+              → pchain ≡ UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op )
+              → 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 = subst (λ k → odef k b ) (sym cheq) ( 
+                   ZChain.is-max zc (subst (λ k → odef k a) cheq za) (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x) ab 
+                       (subst (λ k → HasPrev A k ab f ∨  IsSup A k ab ) cheq P)  a<b )
 
-          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) } ⟫ 
+          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 with UChain.u<x (proj2 za)
+              ... | case1 z<x = case1 (ordtrans z<x px<x )
+              ... | case2 z=y = case2 z=y
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
@@ -549,7 +544,7 @@
                             * 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
+                ... | 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 )   
@@ -559,7 +554,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 = zcp za 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 )
@@ -578,11 +573,12 @@
                             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
+                ... | 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 ) } )
+                ... | 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 ? )  } ) 
+                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) 
+                          (IsSup.x<sup b=sup (chain-mono zy) )  } ) 
      ... | no op = zc5 where
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
           pzc z z<x = prev z z<x
@@ -632,6 +628,22 @@
           ... | 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
+              → 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 
+                       (subst (λ k → HasPrev A k ab f ∨  IsSup A k ab ) ? P)  a<b 
+
+          chain-mono : pchain ⊆'  UnionCF A f mf ay psupf x  
+          chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = UChain.u<x (proj2 za) ; uchain = zc11 }  ⟫ where
+              zc11 : Chain A f mf ay psupf (UChain.u (proj2 za)) a
+              zc11 with UChain.uchain (proj2 za)
+              ... | ch-init .a x = ch-init a x
+              ... | ch-is-sup is-sup fc = ch-is-sup ? ?
+
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extenion ? where -- ¬ A ∋ p, just skip