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

changeset 1062:88731edfa691

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 Sun, 11 Dec 2022 20:38:22 +0900
parents fc37082d2a8a
children 091e7a80bfe3
files src/zorn.agda
diffstat 1 files changed, 29 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Dec 11 09:06:35 2022 +0900
+++ b/src/zorn.agda	Sun Dec 11 20:38:22 2022 +0900
@@ -283,16 +283,16 @@
 
 -- Union of chain lower than x
 
-record IChain  (A : HOD)  ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
+record IChain  {A : HOD}  { f : Ordinal → Ordinal } {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
   field
      i : Ordinal
      i<x : i o< x
-     s<x : supfz i<x o< x
+     s<x : supfz i<x o≤ i 
      fc : FClosure A f (supfz i<x) z
 
-UnionIC : ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) (supfz : {z : Ordinal } → z o< x → Ordinal) ( x : Ordinal ) → HOD
-UnionIC A f ay supf x
-   = record { od = record { def = λ z → odef A z ∧ IChain {A} {f} supf ay x z } ;
+UnionIC : ( A : HOD ) ( f : Ordinal → Ordinal ) { x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal)  → HOD
+UnionIC A f supfz 
+   = record { od = record { def = λ z → odef A z ∧ IChain {A} {f} supfz z } ;
        odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
@@ -1267,12 +1267,7 @@
           supfz {z} z<x = ZChain.supf (pzc  (ob<x lim z<x)) z
 
           pchainx : HOD
-          pchainx = record { od = record { def = λ z → IChain A f supfz z } ; odmax = & A ; <odmax = zc00 } where
-               zc00 : {z : Ordinal } → IChain A f supfz z → z o< & A
-               zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) )
-
-          aic : {z : Ordinal } → IChain A f supfz z → odef A z
-          aic {z} ic =  A∋fc _ f mf (IChain.fc ic )
+          pchainx = UnionIC A f supfz 
 
           zeq : {xa xb z : Ordinal }
              → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa
@@ -1283,30 +1278,45 @@
           iceq : {ix iy : Ordinal } → ix ≡ iy → {i<x : ix o< x } {i<y : iy o< x } → supfz i<x ≡ supfz i<y
           iceq refl = cong supfz  o<-irr
 
-          ifc≤ : {za zb : Ordinal } ( ia : IChain A f supfz za ) ( ib : IChain A f supfz zb ) → (ia≤ib : IChain.i ia o≤ IChain.i ib )
+          ifc≤ : {za zb : Ordinal } ( ia : IChain supfz za ) ( ib : IChain supfz zb ) → (ia≤ib : IChain.i ia o≤ IChain.i ib )
               → FClosure A f (ZChain.supf (pzc (ob<x lim (IChain.i<x ib))) (IChain.i ia)) za
           ifc≤ {za} {zb} ia ib ia≤ib = subst (λ k → FClosure A f k _ ) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc) )   (IChain.fc ia)
 
+          pic<x : {z : Ordinal } → (ic : IChain supfz z ) → osuc (IChain.i ic) o< x
+          pic<x {z} ic = ob<x lim (IChain.i<x ic)
+
+          pchainx⊆chain : {z : Ordinal } → (pz : odef pchainx z) → odef (ZChain.chain (pzc (pic<x (proj2 pz)))) z
+          pchainx⊆chain {z} ⟪ aw , ic ⟫ = ZChain.cfcs (pzc (pic<x  ic) ) <-osuc o≤-refl uz03 (IChain.fc ic) where
+               uz02 : FClosure A f (ZChain.supf (pzc (pic<x ic )) (IChain.i ic)) z
+               uz02 = IChain.fc ic
+               uz03 : ZChain.supf (pzc (pic<x ic)) (IChain.i ic) o≤ IChain.i ic
+               uz03 = IChain.s<x ic
+
+          chain⊆pchainx : {z : Ordinal } → (z<x : z o< x) → odef (ZChain.chain (pzc (ob<x lim z<x))) z → odef pchainx z 
+          chain⊆pchainx {z} z<x ⟪ ua , ch-init fc ⟫ = ⟪ ua , record { i = o∅ ; i<x = ? ; s<x = ? ; fc = ?  }  ⟫
+          chain⊆pchainx {z} z<x ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , record {  i = ? ; i<x = ? ; s<x = ? 
+             ; fc = subst (λ  k → FClosure A f k z ) ? fc }  ⟫
+
           ptotalx : IsTotalOrderSet pchainx
-          ptotalx {a} {b} ia ib = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
+          ptotalx {a} {b} ⟪ _ , ia ⟫ ⟪ _ , ib ⟫ = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 with trio< (IChain.i ia)  (IChain.i ib)
+               uz01 with trio< (supfz (IChain.i<x ia))  (supfz (IChain.i<x ib))
                ... | tri< ia<ib ¬b ¬c with
-                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ? (ifc≤ ia ib (o<→≤ ia<ib))) (s≤fc _ f mf (IChain.fc ib))
+                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ? (ifc≤ ia ib (o<→≤ ?))) (s≤fc _ f mf (IChain.fc ib))
                ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                    ct00 : * (& a) ≡ * (& b)
                    ct00 = cong (*) eq1
                ... | case2 lt = tri< lt  (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)
-               uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib))
+               uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym ia=ib) (IChain.fc ib))
                uz01 | tri> ¬a ¬b ib<ia  with
-                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ? (ifc≤ ib ia (o<→≤ ib<ia))) (s≤fc _ f mf (IChain.fc ia))
+                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ? ? (ifc≤ ib ia (o<→≤ ?))) (s≤fc _ f mf (IChain.fc ia))
                ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
                    ct00 : * (& a) ≡ * (& b)
                    ct00 = sym (cong (*) eq1)
-               ... | case2 lt = tri> (λ lt1 → <-irr (case2 lt) lt1)    (λ eq → <-irr (case1 eq) lt) lt
+               ... | case2 lt = tri> (λ lt1 → <-irr (case2 lt) lt1) (λ eq → <-irr (case1 eq) lt) lt
 
           usup : MinSUP A pchainx
-          usup = minsupP pchainx (λ ic → A∋fc _ f mf (IChain.fc ic ) ) ptotalx
+          usup = minsupP pchainx (λ ic → A∋fc _ f mf (IChain.fc (proj2 ic) ) ) ptotalx
           spu = MinSUP.sup usup
 
           supf1 : Ordinal → Ordinal