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

changeset 1251:a6416ea475bf

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 Wed, 15 Mar 2023 21:44:42 +0900
parents 6c467705e6e4
children c99c37121d47
files src/generic-filter.agda
diffstat 1 files changed, 24 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Wed Mar 15 19:44:38 2023 +0900
+++ b/src/generic-filter.agda	Wed Mar 15 21:44:42 2023 +0900
@@ -359,7 +359,18 @@
        (trans (cong (*) x=ψz) *iso) px
     ... | ⟪ Px , npz ⟫ = Px
     L∋gpr : {p : HOD } → GPR ∋ p → L ∋ (P ＼ p)
-    L∋gpr {p} record { z = z ; az = az ; x=ψz = x=ψz }  = ?
+    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
+        fd41 : * z ⊆ P
+        fd41 {x} lt = L⊆PP ( PDN.x∈PP az ) _ lt
+        fd40 : z ≡ & p
+        fd40 = begin
+           z ≡⟨ sym &iso ⟩ 
+           & (* z) ≡⟨ cong (&) (sym (L＼Lx=x fd41 )) ⟩ 
+           & (P ＼ ( P ＼ * z ) )  ≡⟨ cong (λ k →  & (P ＼ k)) (sym *iso) ⟩ 
+           & (P ＼ * (& ( P ＼ * z )))  ≡⟨ cong (λ k → & (P ＼  * k )) (sym x=ψzp)  ⟩ 
+           & (P ＼ * zp)  ≡⟨ sym x=ψz ⟩ 
+           & p  ∎ where open ≡-Reasoning
     gpr→gp : {p : HOD} → GPR ∋ p → GP ∋ (P ＼ p ) 
     gpr→gp {p} record { z = zp ; az = azp ; x=ψz = x=ψzp } = gfp where
         open ≡-Reasoning
@@ -372,8 +383,19 @@
     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
         gp =  record { z = np ; az = record { z = z ; az = pdz ; x=ψz = x=ψznp } ; x=ψz = x=ψz } 
+        open ≡-Reasoning
+        fd41 : * z ⊆ P
+        fd41 {x} lt = L⊆PP ( PDN.x∈PP pdz ) _ lt
+        p=*z : p ≡ * z
+        p=*z = trans (sym *iso) ( cong (*) (sym ( begin
+           z ≡⟨ sym &iso ⟩ 
+           & (* z) ≡⟨ cong (&) (sym (L＼Lx=x fd41 )) ⟩ 
+           & (P ＼ ( P ＼ * z ) )  ≡⟨ cong (λ k →  & (P ＼ k)) (sym *iso) ⟩ 
+           & (P ＼ * (& ( P ＼ * z )))  ≡⟨ cong (λ k → & (P ＼  * k )) (sym x=ψznp)  ⟩ 
+           & (P ＼ * np)  ≡⟨ sym x=ψz ⟩ 
+           & p ∎ ))) 
         q⊆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))
         gf32 : (P ＼ p) ⊆ (P ＼ q)
         gf32 = proj1 (＼-⊆ {P} {q} {p} q⊆P ) q⊆p 
         gf30 : GP ∋ (P ＼ q )