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

changeset 1125:edef8810a023

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, 10 Jan 2023 02:19:08 +0900
parents d122d0c1b094
children 3091ac71a999
files src/filter.agda
diffstat 1 files changed, 59 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Mon Jan 09 13:09:30 2023 +0900
+++ b/src/filter.agda	Tue Jan 10 02:19:08 2023 +0900
@@ -177,29 +177,75 @@
        proper  : ¬ (filter mf ∋ od∅)
        is-maximum : ( f : Filter {L} {P} LP ) →  ¬ (filter f ∋ od∅)  →  ¬ ( filter mf  ⊂ filter f  )
 
-max→ultra : {L P : HOD} (LP : L ⊆ Power P) → (mx : MaximumFilter {L} {P} LP ) → ultra-filter ( MaximumFilter.mf mx )
-max→ultra {L} {P} LP mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
+record Fp {L P : HOD} (LP : L ⊆ Power P)  (mx : MaximumFilter {L} {P} LP ) (p x : Ordinal ) : Set n where
+    field 
+       y : Ordinal 
+       mfy : odef (filter (MaximumFilter.mf mx)) y
+       x=y∪p : x ≡ & ( * y ∪ * p )
+
+max→ultra : {L P : HOD} (LP : L ⊆ Power P) 
+       → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ＼ q)) 
+       → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q))
+       → (mx : MaximumFilter {L} {P} LP ) → ultra-filter ( MaximumFilter.mf mx )
+max→ultra {L} {P} LP NEG 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 ∋-p (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 : {y : Ordinal } → (y ≡ & p) ∨ odef (filter mf) y → odef L y
-         F⊆L (case1 refl) = lp
+         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 : HOD
-         F = record { od = record { def = λ x → (x ≡ & p) ∨ odef (filter mf) x  } ; odmax = & L ; <odmax = λ lt → odef< (F⊆L lt) } where
+         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) } 
          mu01 :  {r : HOD} {q : HOD} → L ∋ q → F ∋ r → r ⊆ q → F ∋ q
-         mu01 {r} {q} Lq (case1 eq) r⊆q = mu03 where
-             r=p : r ≡ p
-             r=p = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
-             mu03 : odef F (& q)
-             mu03 = ?
+         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 )) ) where
+             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)  
+         mu02 : {r : HOD} {q : HOD} → F ∋ r → F ∋ q → L ∋ (r ∩ q) → F ∋ (r ∩ q)
+         mu02 {r} {q} (case1 record { y = y₁ ; mfy = mfy₁ ; x=y∪p = x=y∪p₁ }) (case1 record { y = y ; mfy = mfy ; x=y∪p = x=y∪p }) Lrq = ?
+         mu02 {r} {q} (case1 record { y = y ; mfy = mfy ; x=y∪p = x=y∪p }) (case2 mfq) Lrq = ?
+         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 = ?
          FisFilter : Filter {L} {P} LP
-         FisFilter = record { filter = F ; f⊆L = F⊆L ; filter1 = mu01 ; filter2 = {!!} }
+         FisFilter = record { filter = F ; f⊆L = F⊆L ; filter1 = mu01 ; filter2 = mu02 }
          FisGreater : {x : Ordinal } → odef (filter (MaximumFilter.mf mx))  x → odef (filter FisFilter ) x
          FisGreater {x} mfx = case2 mfx
          F< : & (filter (MaximumFilter.mf mx)) o< & F