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

changeset 1127:c4f4868a8cdd

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 09:29:58 +0900
parents 3091ac71a999
children 7d4966f2f74d
files src/filter.agda
diffstat 1 files changed, 44 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Tue Jan 10 03:00:04 2023 +0900
+++ b/src/filter.agda	Tue Jan 10 09:29:58 2023 +0900
@@ -185,9 +185,10 @@
 
 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))
        → ({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
+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
@@ -240,10 +241,49 @@
                 ... | 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} (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 = 
+           case1 record { y = & ( * ry ∩ q ) ; mfy = mu23 ; x=y∪p = cong (&) (==→o≡ mu25) } 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) )
+              mu25 : od (r ∩ q) == od (* (& (* ry ∩ q)) ∪ * (& p))
+              mu25 = subst (λ k → od (k ∩ q)== od (* (& (* ry ∩ q)) ∪ * (& p))) (sym mu21) record { eq→ = mu27 ; eq← = mu28 } where
+                  mu27 : {x : Ordinal} → odef (* ry ∪ p) x ∧ odef q x → odef (* (& (* ry ∩ q))) x ∨ odef (* (& p)) x
+                  mu27 {x} ⟪ case1 ryx , qx ⟫ = case1 (subst (λ k → odef k x) (sym *iso) ⟪ ryx , qx ⟫ )
+                  mu27 {x} ⟪ case2 px , qx ⟫ = case2 (subst (λ k → odef k x) (sym *iso) px )
+                  mu28 : {x : Ordinal} → odef (* (& (* ry ∩ q))) x ∨ odef (* (& p)) x → odef (* ry ∪ p) x ∧ odef q x
+                  mu28 {x} (case1 ryq) = ?
+                  mu28 {x} (case2 px) = ⟪  case2 (subst (λ k → odef k x) *iso px ) , ? ⟫
          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 = ?
+         mu02 {r} {q} (case2 mfr) (case2 mfq ) Lrq = case2 (filter2 mf mfr mfq Lrq )
          FisFilter : Filter {L} {P} LP
          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