# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678886760 -32400
# Node ID c99c37121d473cf2dbcfc79821518f442e153b60
# Parent  a6416ea475bfeb7451d5277b7c1ae4f741d5410d
generic filter done

diff -r a6416ea475bf -r c99c37121d47 src/generic-filter.agda
--- a/src/generic-filter.agda	Wed Mar 15 21:44:42 2023 +0900
+++ b/src/generic-filter.agda	Wed Mar 15 22:26:00 2023 +0900
@@ -182,7 +182,7 @@
     rgen = Replace (Filter.filter genf) (λ x → P ＼ x )
     field
        generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Replace (Filter.filter genf) (λ x → P ＼ x )) ≡ od∅ )
-       gfilter1 : {p q : HOD} → rgen ∋ p → q ⊆ p  → rgen ∋ q
+       gfilter1 : {p q : HOD} → rgen ∋ p → q ⊆ p  → L ∋ ( P ＼ q) → rgen ∋ q
        gfilter2 : {p q : HOD} → (rgen ∋ p ) ∧ (rgen ∋ q) → rgen ∋ (p ∪ q)
 
 P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0
@@ -358,9 +358,9 @@
     gpx→⊆P {p} record { z = z ; az = az ; x=ψz = x=ψz } {x} px with subst (λ k → odef k x ) 
        (trans (cong (*) x=ψz) *iso) px
     ... | ⟪ Px , npz ⟫ = Px
-    L∋gpr : {p : HOD } → GPR ∋ p → L ∋ (P ＼ p)
+    L∋gpr : {p : HOD } → GPR ∋ p → (L ∋ p) ∧ ( L ∋ (P ＼ p))
     L∋gpr {p} record { z = zp ; az = record { z = z ; az = az ; x=ψz = x=ψzp } ; x=ψz = x=ψz } 
-      = NEG (subst (λ k → odef L k) fd40 (PDN.x∈PP az)) where
+      = ⟪ subst (λ k → odef L k) fd40 (PDN.x∈PP az) , NEG (subst (λ k → odef L k) fd40 (PDN.x∈PP az)) ⟫ where
         fd41 : * z ⊆ P
         fd41 {x} lt = L⊆PP ( PDN.x∈PP az ) _ lt
         fd40 : z ≡ & p
@@ -380,8 +380,9 @@
            & (* zp) ≡⟨ cong (&) (sym (L＼Lx=x (gpx→⊆P azp) )) ⟩
            & (P ＼ (P ＼ (* zp) )) ≡⟨ cong (λ k → & ( P ＼ k)) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (sym x=ψzp)))  ⟩
            & (P ＼ p) ∎ ) azp
-    gfilter1 : {p q : HOD} → GPR ∋ p → q ⊆ p → GPR ∋ q
-    gfilter1 {p} {q} record { z = np ; az = record { z = z ; az = pdz ; x=ψz = x=ψznp } ; x=ψz = x=ψz } q⊆p = record { z = _ ; az = gf30 ; x=ψz = ? } where
+    gfilter1 : {p q : HOD} → GPR ∋ p → q ⊆ p → L ∋  ( P ＼ q) → GPR ∋ q
+    gfilter1 {p} {q} record { z = np ; az = record { z = z ; az = pdz ; x=ψz = x=ψznp } ; x=ψz = x=ψz } q⊆p Lpq 
+      = record { z = _ ; az = gf30 ; x=ψz = cong (&) fd42 } where
         gp =  record { z = np ; az = record { z = z ; az = pdz ; x=ψz = x=ψznp } ; x=ψz = x=ψz } 
         open ≡-Reasoning
         fd41 : * z ⊆ P
@@ -396,16 +397,27 @@
            & p ∎ ))) 
         q⊆P : q ⊆ P
         q⊆P {x} lt = L⊆PP ( PDN.x∈PP pdz ) _ (subst (λ k → odef k x) p=*z (q⊆p lt))
+        fd42 : q ≡  P ＼ * (& (P ＼ q))
+        fd42 = trans (sym (L＼Lx=x  q⊆P )) (cong (λ k → P ＼ k) (sym *iso) )
         gf32 : (P ＼ p) ⊆ (P ＼ q)
         gf32 = proj1 (＼-⊆ {P} {q} {p} q⊆P ) q⊆p 
         gf30 : GP ∋ (P ＼ q )
-        gf30 = f1 ? (gpr→gp gp) gf32
+        gf30 = f1 Lpq (gpr→gp gp) gf32
     gfilter2 : {p q : HOD} → (GPR ∋ p) ∧ (GPR ∋ q) → Replace GP (_＼_ P) ∋ (p ∪ q)
     gfilter2 {p} {q} ⟪ gp , gq ⟫ 
-       = record { z = _ ; az = gf31 ; x=ψz = cong (&) ?  } where
+       = record { z = _ ; az = gf31 ; x=ψz = cong (&) gf32  } where
         open ≡-Reasoning
         gf31 : GP ∋ ( (P ＼ p ) ∩ (P ＼ q ) )
-        gf31 = f2 (gpr→gp gp) (gpr→gp gq) (CAP (L∋gpr gp) (L∋gpr gq)  ) 
+        gf31 = f2 (gpr→gp gp) (gpr→gp gq) (CAP (proj2 (L∋gpr gp)) (proj2 (L∋gpr gq))  ) 
+        gf33 : (p ∪ q) ⊆ P
+        gf33 {x} (case1 px) = L⊆PP (proj1 (L∋gpr gp)) _ (subst (λ k → odef k x) (sym *iso) px )
+        gf33 {x} (case2 qx) = L⊆PP (proj1 (L∋gpr gq)) _ (subst (λ k → odef k x) (sym *iso) qx )
+        gf32 :  (p ∪ q) ≡ (P ＼ * (& ((P ＼ p) ∩ (P ＼ q))))
+        gf32 = begin
+          p ∪ q ≡⟨ sym ( L＼Lx=x gf33 ) ⟩ 
+          P ＼ (P ＼ (p ∪ q)) ≡⟨ cong (λ k → P ＼ k) (sym (gf02 {P} {p}{q} ) ) ⟩ 
+          P ＼ ((P ＼ p) ∩ (P ＼ q)) ≡⟨ cong (λ k → P ＼ k) (sym *iso) ⟩ 
+          P ＼ * (& ((P ＼ p) ∩ (P ＼ q))) ∎
 
 open GenericFilter
 open Filter