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

changeset 1035:2144ef00cab9

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 Fri, 02 Dec 2022 11:07:51 +0900
parents 84881efe649b
children 23a8e4d558e0
files src/zorn.agda
diffstat 1 files changed, 47 insertions(+), 58 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Dec 01 18:00:44 2022 +0900
+++ b/src/zorn.agda	Fri Dec 02 11:07:51 2022 +0900
@@ -266,22 +266,6 @@
      fc00 :   b ≤  (f b)
      fc00 = proj1 (mf _ (subst (λ k → odef A k) a=b aa ))
 
-fc-total : (A : HOD ) ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) (supf : Ordinal → Ordinal )
-    (order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y)
-   {s s1 a b : Ordinal } ( fa : FClosure A f (supf s) a )( fb : FClosure A f (supf s1) b )  → Tri (* a < * b) (* a ≡ * b) (* b < * a )
-fc-total A f mf supf order {xa} {xb} {a} {b} ca cb with trio< xa xb
-... | tri< a₁ ¬b ¬c with ≤-ftrans  (order a₁ ca ) (s≤fc (supf xb) f mf cb )
-... | 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 a<b =  tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)  
-fc-total A f mf supf order {xa} {xb} {a} {b} ca cb | tri≈ _ refl _ = fcn-cmp _ f mf ca cb 
-fc-total A f mf supf order {xa} {xb} {a} {b} ca cb | tri> ¬a ¬b c with ≤-ftrans  (order c cb ) (s≤fc (supf xa) f mf ca )
-... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-          ct00 : * a ≡ * b
-          ct00 = cong (*) (sym eq1)  
-... | case2 b<a =  tri> (λ lt → <-irr (case2 b<a ) lt)  (λ eq → <-irr (case1 eq) b<a )  b<a
-
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
@@ -349,7 +333,7 @@
    field
       supf :  Ordinal → Ordinal
 
-      order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w ≤ supf y
+      order : {x y w : Ordinal } → y o≤ z → x o< y → FClosure A f (supf x) w → w ≤ supf y
 
       cfcs : (mf< : <-monotonic-f A f)
          {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
@@ -408,7 +392,20 @@
 
    f-total : IsTotalOrderSet chain
    f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ =
-     subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fc-total A f mf supf order fca fcb)
+     subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where
+         fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+         fc-total with trio< ua ub
+         ... | tri< a₁ ¬b ¬c with ≤-ftrans  (order (o<→≤ sub<x) a₁ fca ) (s≤fc (supf ub) f mf fcb )
+         ... | 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 a<b =  tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)  
+         fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb 
+         fc-total | tri> ¬a ¬b c with ≤-ftrans  (order (o<→≤ sua<x) c fcb ) (s≤fc (supf ua) f mf fca )
+         ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
+                  ct00 : * (& a) ≡ * (& b)
+                  ct00 = cong (*) (sym eq1)  
+         ... | case2 b<a =  tri> (λ lt → <-irr (case2 b<a ) lt)  (λ eq → <-irr (case1 eq) b<a )  b<a
    f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where
       ft01 : (& a) ≤ (& b) → Tri ( a <  b) ( a ≡  b) ( b <  a )
       ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b  (λ lt → ⊥-elim (<-irr (case1 a=b) lt))  where
@@ -455,7 +452,7 @@
    supf-idem  mf< {b} b≤z sfb≤x = z52 where
        z54 :  {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
        z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
-       z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order su<b fc where
+       z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z su<b fc where
                su<b : u o< b
                su<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
        z52 : supf (supf b) ≡ supf b
@@ -855,8 +852,8 @@
           m13 : supf0 px o≤ sp1
           m13 = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1)  m14 where
              m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1)
-             m14 {z} ⟪ as , ch-init fc ⟫ = ?
-             m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ? 
+             m14 {z} ⟪ as , ch-init fc ⟫ = ≤-ftrans (ZChain.fcy<sup zc o≤-refl fc) sfpx≤sp1
+             m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ≤-ftrans (ZChain.order zc o≤-refl u<x fc) sfpx≤sp1
 
           zc41 : ZChain A f mf ay x
           zc41 with zc43 x sp1
@@ -1033,41 +1030,25 @@
                     ... | case2 fc = case2 (fsuc _ fc)
                     zc21 (init asp refl ) = ?
 
-                 record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
-                     field
-                         tsup : MinSUP A (UnionCF A f ay supf1 z)
-                         tsup=sup : supf1 z ≡ MinSUP.sup tsup
+                 is-minsup :  {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
+                 is-minsup {z} z≤x with osuc-≡< z≤x
+                 ... | case1 z<x = ZChain.is-minsup zc (zc-b<x z<x)
+                 ... | case2 z=x = ?
 
-                 sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
-                 sup {z} z≤x with trio< z px
-                 ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.as m
-                         ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where
-                    m = ZChain.minsup zc (o<→≤ a)
-                    ms00 :  {x : Ordinal} → odef (UnionCF A f ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
-                    ms00 {w} ⟪ az , cp ⟫ = MinSUP.x≤sup m ⟪ az , ? ⟫ 
-                    ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
-                        odef (UnionCF A f ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
-                    ms01 {sup2} us P = MinSUP.minsup m us ?
-                 ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.as m
-                         ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
-                    m = ZChain.minsup zc (o≤-refl0 b)
-                    ms00 :  {x : Ordinal} → odef (UnionCF A f ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
-                    ms00 {x} ux = MinSUP.x≤sup m ?
-                    ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
-                        odef (UnionCF A f ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
-                    ms01 {sup2} us P = MinSUP.minsup m us ?
-                 ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.as sup1
-                         ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where
-                    m = sup1
-                    ms00 :  {x : Ordinal} → odef (UnionCF A f ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
-                    ms00 {x} ux = MinSUP.x≤sup m ?
-                    ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
-                        odef (UnionCF A f ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
-                    ms01 {sup2} us P = MinSUP.minsup m us ?
-
+                 order : {a b : Ordinal} {w : Ordinal} →
+                    b o≤ x → a o< b → FClosure A f (supf1 a) w → w ≤ supf1 b
+                 order {a} {b} {w} b≤x a<b fc with trio< b px
+                 ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) a<b (fcup fc (o<→≤ (ordtrans a<b b<px) )) 
+                 ... | tri≈ ¬a b=px ¬c = ZChain.order zc (o≤-refl0 b=px) a<b (fcup fc (o<→≤ (subst (λ k → a o< k) b=px a<b )))
+                 ... | tri> ¬a ¬b px<b with trio< a px
+                 ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px fc) sfpx≤sp1  --   supf1 a ≡ supf0 a
+                 ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (case2 (subst (λ k → FClosure A f (supf0 k) w) a=px fc ))  
+                 ... | tri> ¬a ¬b px<a = ⊥-elim (¬p<x<op ⟪ px<a , zc22 ⟫ ) where  --   supf1 a ≡ sp1
+                     zc22 : a o< osuc px
+                     zc22 = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
 
           zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ZChain.asupf zc ; supf-mono = ZChain.supf-mono zc ; order = ?
-              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs    }  where
+              ; supfmax = ? ; sup=u = ? ; is-minsup = ? ; cfcs = cfcs    }  where
 
                  --  supf0 px not is included by the chain
                  --     supf1 x ≡ supf0 px because of supfmax
@@ -1172,6 +1153,10 @@
                      ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ?  } where
                           zc37 : MinSUP A (UnionCF A f ay supf0 z)
                           zc37 = record { sup = ? ; asm = ? ; x≤sup = ? ; minsup = ? }
+
+                 is-minsup :  {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf0 z) (supf0 z)
+                 is-minsup = ?
+
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsMinSUP A (UnionCF A f ay supf0 b) b ∧ (¬ HasPrev A (UnionCF A f ay supf0 b) f b ) → supf0 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
@@ -1189,9 +1174,10 @@
                      
      ... | no lim with trio< x o∅
      ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 
-     ... | tri≈ ¬a b ¬c = record { supf = ? }
+     ... | tri≈ ¬a b ¬c = record { supf = ? ; sup=u = ? ; asupf = ? ; supf-mono = ? ; order = ?
+              ; supfmax = ? ; is-minsup = ? ; cfcs = ?    }  
      ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
-              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs    }  where
+              ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
 
           pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z
           pzc {z} z<x = prev z z<x
@@ -1227,14 +1213,14 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 with trio< (IChain.i ia)  (IChain.i ib)
                ... | tri< ia<ib ¬b ¬c with 
-                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ia<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))) ? ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (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 ¬b ib<ia  with
-                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ia))) ib<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))) ? ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (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)
@@ -1287,6 +1273,9 @@
           ... | tri≈ ¬a b ¬c = ?
           ... | tri> ¬a ¬b c = ?
 
+          is-minsup :  {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
+          is-minsup = ?
+
           cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
                  → a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
           cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x
@@ -1379,7 +1368,7 @@
                ... | case1 eq = ⊥-elim ( ne eq )
                ... | case2 lt = lt
                z19 : IsSUP A (UnionCF A f ay (ZChain.supf zc) sp) sp
-               z19 = record {   x≤sup = z20 }  where
+               z19 = record { ax = ? ;   x≤sup = z20 }  where
                    z20 : {y : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
                    z20 {y} zy with MinSUP.x≤sup sp1
                        (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22)  zy ))