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

changeset 1129:5053fd12134a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use different filter
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 10 Jan 2023 18:12:05 +0900
parents 7d4966f2f74d
children 4a4ac5141b95
files src/filter.agda
diffstat 1 files changed, 13 insertions(+), 105 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Tue Jan 10 17:16:16 2023 +0900
+++ b/src/filter.agda	Tue Jan 10 18:12:05 2023 +0900
@@ -181,7 +181,7 @@
     field 
        y : Ordinal 
        mfy : odef (filter (MaximumFilter.mf mx)) y
-       x=y∪p : x ≡ & ( * y ∪ * p )
+       y-p⊂x : ( * y ＼ * p ) ⊂ * x
 
 max→ultra : {L P : HOD} (LP : L ⊆ Power P) 
        → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ＼ q)) 
@@ -191,115 +191,23 @@
 max→ultra {L} {P} LP NEG CAP CUP mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
     mf = MaximumFilter.mf mx
     ultra : {p : HOD} → L ∋ p → L ∋ (P ＼ p) → (filter mf ∋ p) ∨ (filter mf ∋ (P ＼ p))
-    ultra {p} Lp lnp with ∋-p (filter mf) p
+    ultra {p} Lp lnp with ODC.∋-p O (filter mf) p 
     ... | yes y = case1 y
-    ... | no np with ∋-p (filter mf) (P ＼ p) 
-    ... | yes y = case2 y
-    ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter FisProper  ⟪ F< , FisGreater ⟫  ) where
-         F⊆L : {x : Ordinal } →  Fp {L} {P} LP mx (& p) x ∨ odef (filter mf) x → odef L x
-         F⊆L (case2 mfx) = f⊆L mf mfx
-         F⊆L {x} (case1 pmf) = mu04 pmf where
-             mu05 : (fp : Fp LP mx (& p) x ) → odef L (Fp.y fp )
-             mu05 fp = f⊆L mf ( Fp.mfy fp )
-             mu04 :  Fp LP mx (& p) x → odef L x
-             mu04 fp = subst (λ k → odef L k ) (sym (trans (Fp.x=y∪p fp ) mu06  )) 
-              ( CUP (subst (λ k → odef L k ) (sym &iso) (mu05 fp)) Lp ) where
-                 mu06 :  & (* (Fp.y fp) ∪ * (& p)) ≡ & (* (Fp.y fp) ∪ p) 
-                 mu06 = cong (λ k → & (* (Fp.y fp) ∪ k))  *iso
-         F : HOD  -- Replace (filter mf) (λ y → y ∪ p ) ∪ filter mf
-         F = record { od = record { def = λ x →  Fp {L} {P} LP mx (& p) x ∨ odef (filter mf) x  } 
-            ; odmax = & L ; <odmax = λ lt → odef< (F⊆L lt) } 
+    ... | no np = ? where
+         F : HOD  
+         F = record { od = record { def = λ x →  odef L x ∧ Fp {L} {P} LP mx (& p) x } 
+            ; odmax = & L ; <odmax = λ lt → odef< (proj1 lt) } 
          mu01 :  {r : HOD} {q : HOD} → L ∋ q → F ∋ r → r ⊆ q → F ∋ q
-         mu01 {r} {q} Lq (case1 record { y = y ; mfy = mfy ; x=y∪p = x=y∪p }) r⊆q = mu03 where
-             y+q-r : HOD
-             y+q-r = * y ∪ ( q ＼ r )
-             Ly : L ∋ * y
-             Ly = subst (λ k → odef L k) (sym &iso) (f⊆L mf mfy)
-             mu08 : L ∋ y+q-r
-             mu08 = CUP Ly (NEG Lq (subst (λ k → odef L k) 
-               (trans (cong (λ k → & (* y ∪ k)) (sym *iso)) (sym x=y∪p) ) (CUP Ly Lp )) ) 
-             mu09 : * y ⊆ y+q-r
-             mu09 {x} yx = case1 yx
-             mu07 : filter mf  ∋ y+q-r
-             mu07 = filter1 mf {_} {y+q-r} mu08 (subst (λ k → odef (filter mf) k) (sym &iso) mfy) mu09
-             mu03 : odef F (& q) -- y+q-r + p  ≡ y+q-(y+p)+ p = q  so it is in F
-             mu03 = case1 record { y = _  ; mfy = mu07 ; x=y∪p = cong (&) (==→o≡ record { eq→ = mu10 ; eq← = mu11 } ) } where
-                mu12 : r ≡ (* y ∪ p)
-                mu12 = subst₂ (λ j k → j ≡ k ) *iso (trans *iso (cong (λ k → (* y ∪ k)) *iso)) (cong (*) x=y∪p )
-                mu10 : {x : Ordinal} → odef q x → odef (* (& y+q-r) ∪ * (& p)) x
-                mu10 {x} qx with ODC.∋-p O r (* x)
-                ... | no nrx = case1 (subst (λ k → odef k x) (sym *iso) mu13) where
-                      mu13 : odef (* y ∪ (q ＼ r)) x 
-                      mu13 = case2 ⟪ qx , (λ rx → nrx (subst (λ k → odef r k ) (sym &iso) rx))  ⟫ 
-                ... | yes rx with subst₂ (λ j k → odef j k ) mu12 (sym &iso) rx
-                ... | case1 yx = case1 (subst (λ k → odef k x) (sym *iso) (case1 (subst (λ k → odef (* y) k) (trans &iso &iso) yx) ) )
-                ... | case2 px = case2 (subst₂ (λ j k → odef j k ) (sym *iso) (trans &iso &iso) px )
-                mu11 : {x : Ordinal} → odef (* (& y+q-r) ∪ * (& p)) x → odef q x
-                mu11 {x} (case2 px) = r⊆q (subst (λ k → odef k x) (sym mu12) (case2 (subst (λ k → odef k x) *iso px) )) 
-                mu11 {x} (case1 m06x) with subst (λ k → odef k x) *iso m06x
-                ... | case1 yx = r⊆q (subst (λ k → odef k x) (sym mu12) (case1 yx))
-                ... | case2 q-rx = proj1 q-rx
-         mu01 {r} {q} Lq (case2 mfr) r⊆q = case2 ( filter1 mf Lq mfr r⊆q)  
+         mu01 {r} {q} Lq ⟪ Lr , record { y = y ; mfy = mfy ; y-p⊂x = y-p⊂x } ⟫ r⊆q = ⟪ Lq , record { y = y ; mfy = mfy ; y-p⊂x = ? } ⟫ 
          mu02 : {r : HOD} {q : HOD} → F ∋ r → F ∋ q → L ∋ (r ∩ q) → F ∋ (r ∩ q)
-         mu02 {r} {q} (case1 record { y = ry ; mfy = mfry ; x=y∪p = x=ry∪p }) (case1 record { y = qy ; mfy = mfqy ; x=y∪p = x=qy∪p }) Lrq = mu20 where
-              mu21 : r ≡ * ry ∪ p
-              mu21 = subst₂ (λ j k → j ≡ k ) *iso (trans *iso (cong (λ k → (* ry ∪ k)) *iso)) (cong (*) x=ry∪p )
-              mu22 : q ≡ * qy ∪ p
-              mu22 = subst₂ (λ j k → j ≡ k ) *iso (trans *iso (cong (λ k → (* qy ∪ k)) *iso)) (cong (*) x=qy∪p )
-              mu23 : odef (filter mf) (& (* ry ∩ * qy))
-              mu23 = filter2 mf (subst (λ k → odef (filter mf) k) (sym &iso) mfry) (subst (λ k → odef (filter mf) k) (sym &iso) mfqy) 
-                (CAP (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfry)) (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfqy)))
-              mu25 : (r ∩ q) =h= ((* ry ∩ * qy) ∪ * (& p))
-              mu25 = record { eq→ = mu27 ; eq← = mu28 } where
-                 mu27 : {x : Ordinal } → odef (r ∩ q) x → odef ((* ry ∩ * qy) ∪ * (& p)) x
-                 mu27 {x} rqx with subst₂ (λ j k → odef ( j  ∩ k ) x ) mu21 mu22 rqx
-                 ... | ⟪ case1 ryx , case1 qyx ⟫ = case1 ⟪ ryx , qyx ⟫
-                 ... | ⟪ case1 ryx , case2 px ⟫ = case2 (subst (λ k → odef k x) (sym *iso) px)
-                 ... | ⟪ case2 px , case1 qyx ⟫ = case2 (subst (λ k → odef k x) (sym *iso) px)
-                 ... | ⟪ case2 px , case2 px₂ ⟫ = case2 (subst (λ k → odef k x) (sym *iso) px)
-                 mu28 : {x : Ordinal } → odef ((* ry ∩ * qy) ∪ * (& p)) x → odef (r ∩ q) x
-                 mu28 {x} (case1 ryqy) = subst₂ (λ j k → odef (j ∩ k ) x ) (sym mu21) (sym mu22) ⟪ case1 (proj1 ryqy) , case1 (proj2 ryqy) ⟫ 
-                 mu28 {x} (case2 px) = subst₂ (λ j k → odef (j ∩ k ) x ) (sym mu21) (sym mu22) 
-                    ⟪ case2 (subst (λ k → odef k x) *iso px) , case2 (subst (λ k → odef k x) *iso px) ⟫
-              mu26 : ((* ry ∩ * qy) ∪ * (& p)) ≡ (* (& (* ry ∩ * qy)) ∪ * (& p))
-              mu26 = cong (λ k → (k ∪ * (& p))) (sym *iso)
-              mu24 : & (r ∩ q) ≡ & (* (& (* ry ∩ * qy)) ∪ * (& p))
-              mu24 = subst (λ k → & (r ∩ q) ≡ k ) (cong (&) mu26) (cong (&) (==→o≡ mu25) ) 
-              mu20 : F ∋ (r ∩ q)
-              mu20 = case1 record { y = & ( * ry ∩ * qy ) ; mfy = mu23 ; x=y∪p = mu24 }
-         mu02 {r} {q} (case1 record { y = ry ; mfy = mfry ; x=y∪p = x=ry∪p }) (case2 mfq) Lrq = case2 mu24 where
-              mu21 : r ≡ * ry ∪ p
-              mu21 = subst₂ (λ j k → j ≡ k ) *iso (trans *iso (cong (λ k → (* ry ∪ k)) *iso)) (cong (*) x=ry∪p )
-              mu23 : odef (filter mf) (& (* ry ∩ q))
-              mu23 = filter2 mf (subst (λ k → odef (filter mf) k) (sym &iso) mfry) mfq
-                (CAP (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfry)) (f⊆L mf mfq) )
-              mu26 : (p ∩ q) =h= od∅
-              mu26 = record { eq→ = λ lt → ⊥-elim ( mu29 lt)  ; eq← = λ lt → ⊥-elim ( ¬x<0 lt  ) } where
-                  q-p : HOD
-                  q-p = q ＼ p
-                  [q-p]⊆q : ?
-                  [q-p]⊆q = ?
-                  mu30 : odef (filter mf ) (& ( q ∩ ( q ＼ p )))
-                  mu30 = filter2 mf ? ? ?
-                  mu31 : odef (filter mf ) (& p )
-                  mu31 = filter1 mf ? ? ?
-                  mu29 : {x : Ordinal} → ¬ ( odef (p ∩ q) x )
-                  mu29 {x} pqx = ?
-              mu25 : od (r ∩ q) == od (* (& (* ry ∩ q)))
-              mu25 = subst (λ k → od (k ∩ q)== od (* (& (* ry ∩ q)) )) (sym mu21) record { eq→ = mu27 ; eq← = mu28 } where
-                  mu27 : {x : Ordinal} → odef (* ry ∪ p) x ∧ odef q x → odef (* (& (* ry ∩ q))) x 
-                  mu27 {x} ⟪ case1 ryx , qx ⟫ = subst (λ k → odef k x) (sym *iso) ⟪ ryx , qx ⟫ 
-                  mu27 {x} ⟪ case2 px , qx ⟫ = ?
-                  mu28 : {x : Ordinal} → odef (* (& (* ry ∩ q))) x → odef (* ry ∪ p) x ∧ odef q x
-                  mu28 {x} ryq = ?
-              mu24 :   odef (filter mf) (& (r ∩ q))
-              mu24 = ?                             
-         mu02 {r} {q} (case2 mfr) (case1 record { y = y ; mfy = mfp ; x=y∪p = x=y∪p }) Lrq = ?
-         mu02 {r} {q} (case2 mfr) (case2 mfq ) Lrq = case2 (filter2 mf mfr mfq Lrq )
+         mu02 {r} {q} ⟪ Lr , record { y = ry ; mfy = mfry ; y-p⊂x = ry-p⊂x } ⟫ 
+          ⟪ Lq , record { y = qy ; mfy = mfqy ; y-p⊂x = qy-p⊂x } ⟫  Lrq = ⟪ Lrq , record { y = & (* qy  ∩ * ry) ; mfy = ? ; y-p⊂x = ? } ⟫   
          FisFilter : Filter {L} {P} LP
-         FisFilter = record { filter = F ; f⊆L = F⊆L ; filter1 = mu01 ; filter2 = mu02 }
+         FisFilter = record { filter = F ; f⊆L = ? ; filter1 = mu01 ; filter2 = mu02 }
          FisGreater : {x : Ordinal } → odef (filter (MaximumFilter.mf mx))  x → odef (filter FisFilter ) x
-         FisGreater {x} mfx = case2 mfx
+         FisGreater {x} mfx = ⟪ f⊆L mf mfx , record { y = x ; mfy = mfx ; y-p⊂x = mu03 }  ⟫ where
+             mu03 : (* x ＼ * (& p)) ⊂ * x
+             mu03 =  ⟪ ? , ?  ⟫
          F< : & (filter (MaximumFilter.mf mx)) o< & F
          F< = ?
          FisProper : ¬ (filter FisFilter ∋ od∅)