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

changeset 787:56df4675e15a

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 Tue, 02 Aug 2022 11:34:28 +0900
parents 1db222b676d8
children c164f4f7cfd1
files src/zorn.agda
diffstat 1 files changed, 25 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Aug 02 07:29:41 2022 +0900
+++ b/src/zorn.agda	Tue Aug 02 11:34:28 2022 +0900
@@ -273,22 +273,18 @@
 --    minimum index is y not ϕ 
 --
 
-record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where
+record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u : Ordinal) : Set n where
    field
       fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) 
       order    : {sup1 z1 : Ordinal} → (lt : supf sup1 o< supf u ) → FClosure A f (supf sup1 ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
 
-ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
-   → {x z : Ordinal } →  ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
-ChainP-next A f mf {y} ay supf {x} {z} cp = record {  fcy<sup = ChainP.fcy<sup cp ; order = ChainP.order cp }
-
 -- Union of supf z which o< x
 --
 
 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
-    ch-is-sup  : (u : Ordinal) {z : Ordinal }  ( is-sup : ChainP A f mf ay supf u z) 
+    ch-is-sup  : (u : Ordinal) {z : Ordinal }  ( is-sup : ChainP A f mf ay supf u ) 
         ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -341,7 +337,7 @@
             zc04 : odef (UnionCF A f mf ay supf b) (f x)
             zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc  )
             ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ 
-            ... | ⟪ as , ch-is-sup u is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) ⟫ 
+            ... | ⟪ as , ch-is-sup u is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u is-sup (fsuc _ fc) ⟫ 
         zc00 : ( * z1  ≡  SUP.sup (sup b<z )) ∨ ( * z1  < SUP.sup ( sup b<z ) )
         zc00 = SUP.x<sup (sup b<z) (zc01 fc )
         zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
@@ -521,7 +517,7 @@
         ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 
         ... | ⟪ ab0 , ch-is-sup u is-sup fc ⟫ = ⟪ ab , 
                  subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
-                      (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
+                      (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u is-sup (fsuc _ fc))  ⟫ 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
         ... | yes op = record { is-max = is-max } where
@@ -560,7 +556,7 @@
                     m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
                            → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
                     m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
-                    m06 : ChainP A f mf ay (ZChain.supf zc) b b
+                    m06 : ChainP A f mf ay (ZChain.supf zc) b 
                     m06 = record {  fcy<sup = m08  ; order = m09 } 
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
@@ -582,7 +578,7 @@
                  m05 : b ≡ ZChain.supf zc b
                  m05 = sym (ZChain.sup=u zc ab m09
                       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 : ChainP A f mf ay (ZChain.supf zc) b 
                  m06 = record { fcy<sup = m07 ;  order = m08 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
                  m04 = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl))  ⟫
@@ -685,7 +681,7 @@
           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 (proj2 ua)
           ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫
-          ... | ch-is-sup u is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) ,  ch-is-sup u (ChainP-next A f mf ay isupf is-sup) (fsuc _ fc) ⟫
+          ... | ch-is-sup u is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) ,  ch-is-sup u is-sup (fsuc _ fc) ⟫
           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) )
@@ -703,7 +699,7 @@
                ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt )
                uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
                uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi )
-               uz02 :  ChainP A f mf ay isupf spi (isupf z)
+               uz02 :  ChainP A f mf ay isupf spi 
                uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} }
 
 
@@ -736,7 +732,7 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-          pnext {a} ⟪ aa , ch-is-sup u is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc ) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u is-sup (fsuc _ fc ) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
@@ -751,9 +747,20 @@
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extension : ZChain A f mf ay x
-          no-extension = record { supf = supf0 ; supf-mono = ZChain.supf-mono zc ; sup = ?
+          no-extension = record { supf = supf0 ; supf-mono = ZChain.supf-mono zc ; sup = sup
                ; initial = pinit ; chain∋init = pcy  ; sup=u = {!!} ; supf-is-sup = ? ; csupf = ? 
-              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } 
+              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }  where
+                 sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf0 z)
+                 sup {z} z<x with trio< z px
+                 ... | tri< a ¬b ¬c = ZChain.sup zc a
+                 ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → z o< k) (sym (Oprev.oprev=x op)) z<x ⟫ )  --   px < z < x
+                 ... | tri≈ ¬a b ¬c = record { sup = * (supf0 px) ; A∋maximal = subst (λ k → odef A k) (sym &iso) (proj1 (ZChain.csupf zc o≤-refl ))
+                     ; x<sup = x<sup } where
+                     zc8 : odef (UnionCF A f mf ay supf0 z) (supf0 px)
+                     zc8 = subst (λ k → odef (UnionCF A f mf ay supf0 z) k ) (cong supf0 b)  (ZChain.csupf zc (subst (λ k → z o≤ k) b o≤-refl ))
+                     x<sup :  {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ * (supf0 px)) ∨ (w < * (supf0 px))
+                     x<sup {w} ⟪ aw , ch-init fc ⟫ = ?
+                     x<sup {w} ⟪ aw , ch-is-sup u is-sup fc ⟫ = ?
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* px)
@@ -831,7 +838,7 @@
                       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 : ChainP A f mf ay psupf z 
                       cp1 = record {  fcy<sup = zc20   ; order = ? } 
                      ---  u = supf u = supf z 
           ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup {!!} {!!} {!!} ⟫ where
@@ -852,7 +859,7 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫
-          pnext {a} ⟪ aa , ch-is-sup u is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u is-sup (fsuc _ fc) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
@@ -874,7 +881,7 @@
           ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 
           ... | ⟪ ab0 , ch-is-sup u is-sup fc ⟫ = ⟪ ab , 
                      subst (λ k → UChain A f mf ay supf x k )
-                          (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
+                          (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u is-sup (fsuc _ fc))  ⟫ 
 
           no-extension : ZChain A f mf ay x
           no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; sup=u = {!!}