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

changeset 1243:50fcf7f047d1

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, 14 Mar 2023 06:19:42 +0900
parents e843ace90b31
children a7dfcbbd07ff
files src/generic-filter.agda
diffstat 1 files changed, 39 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Mon Mar 13 13:32:22 2023 +0900
+++ b/src/generic-filter.agda	Tue Mar 14 06:19:42 2023 +0900
@@ -172,9 +172,11 @@
 
 -- ＼-⊆
 
-P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) 
+P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 
+      → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q ))
+      → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)))
       → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C )
-P-GenericFilter P L p0 L⊆PP Lp0 NEG C = record {
+P-GenericFilter P L p0 L⊆PP Lp0 CAP NEG C = record {
       genf = record { filter = Replace (PDHOD L p0 C) (λ x → P ＼ x)  ; f⊆L =  gf01 ; filter1 = ? ; filter2 = ? }
     ; generic = λ D cd → subst (λ k → ¬ (Dense.dense D ∩ k) ≡ od∅ ) (sym gf00) (fdense D cd )
    } where
@@ -217,9 +219,42 @@
                  gf15 y gpqy with subst (λ k → odef k y ) *iso gpqy 
                  ... | case1 xpy = p-monotonic L p0 C gf16 (PDN.pn<gr Pp y xpy )
                  ... | case2 xqy = PDN.pn<gr Pq _ xqy
-        ... | tri≈ ¬a refl ¬c =  record { z = xp ; az = Pp  ; x=ψz = trans (cong (&) gf17) peq } where
+        ... | tri≈ ¬a eq ¬c = record { z = & (* xp ∩ * xq) ; az = record { gr = gr Pp ; pn<gr = gf21 ; x∈PP = gf22 } ; x=ψz = gf23 } where
+              gf22 : odef L (& (* xp ∩ * xq))
+              gf22 = CAP (subst (λ k → odef L k ) (sym &iso) (PDN.x∈PP Pp)) (subst (λ k → odef L k ) (sym &iso) (PDN.x∈PP Pq)) 
+              gf21 : (y : Ordinal) → odef (* (& (* xp ∩ * xq))) y → odef (* (find-p L C (gr Pp) (& p0))) y
+              gf21 y xpqy with subst (λ k → odef k y) *iso xpqy
+              ... | ⟪ xpy , xqy ⟫ = PDN.pn<gr Pp _ xpy
+              gf25 : odef L (& p)
+              gf25 = subst (λ k → odef L k ) (sym peq) ( NEG (subst (λ k → odef L k) (sym &iso) (PDN.x∈PP Pp) ))
+              gf27 : {x : Ordinal} → odef p x → odef (P ＼ * xp) x
+              gf27 {x} px = subst (λ k → odef k x) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) peq)) px
+              gf23 : & (p ∩ q) ≡ & (P ＼ * (& (* xp ∩ * xq)))    --  != P ＼ (xp ∪ xq)
+              gf23 = cong (&) ( ==→o≡ record { eq→ = gf24 ; eq← = gf30 } ) where
+                  gf24 : {x : Ordinal} → odef (p ∩ q) x → odef (P ＼ * (& (* xp ∩ * xq))) x
+                  gf24 {x} ⟪ px , qx ⟫ = subst (λ k → odef (P ＼ k) x) (sym *iso)  ⟪ L⊆PP gf25 _ (subst (λ k → odef k x) (sym *iso) px) , gf26  ⟫ where
+                     gf26 : ¬ odef (* xp ∩ * xq) x
+                     gf26 npx = proj2 (gf27 px) (proj1 npx)
+                  gf30 : {x : Ordinal} → odef (P ＼ * (& (* xp ∩ * xq))) x → odef (p ∩ q) x
+                  gf30 {x} pxp with subst (λ k → odef (P ＼ k) x) *iso pxp
+                  ... | ⟪ Px , ¬xpqx ⟫ = ⟪ ? , gf28 ⟪ Px , (λ xqx → ¬xpqx ⟪ ? , xqx ⟫ )  ⟫ ⟫ where
+                      gf28 : {x : Ordinal} → odef (P ＼ * xq) x → odef q x 
+                      gf28 {x} qx = subst (λ k → odef k x) (sym (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) qeq))) qx
+              pn : HOD
+              pn = * (find-p L C (gr Pp) (& p0))
+              qn : HOD
+              qn = * (find-p L C (gr Pq) (& p0))
+              gf20 : pn ≡ qn
+              gf20 = cong ( λ k → * (find-p L C k (& p0))) eq
+              gf19 : * xp ⊆ pn
+              gf19 = PDN.pn<gr Pp _
+              gf18 : PDN L p0 C xp → PDN L p0 C xq → Replaced (PDHOD L p0 C) (λ z → & (P ＼ * z)) (& (p ∩ q))
+              gf18 record { gr = gr₁ ; pn<gr = pn<gr₁ ; x∈PP = x∈PP₁ } record { gr = gr ; pn<gr = pn<gr ; x∈PP = x∈PP } = ?
+              -- record { z = xp ; az = Pp  ; x=ψz = trans (cong (&) gf17) peq } where
               gf17 : p ∩ q ≡ p
               gf17 = ==→o≡ record { eq→ = proj1 ; eq← = λ {y} px → ⟪ px , ? ⟫   }
+              f4 : (y : Ordinal) → odef (* (find-p L C (gr Pp ) (& p0))) y → odef (p ∩ q) y
+              f4 y lt = ⟪ subst (λ k → odef k y) *iso ?  , subst (λ k → odef k y) *iso (pn<gr ? ? lt) ⟫ 
         ... | tri> ¬a ¬b c = record { z = & ( (* xp) ∪ (* xq) ) ; az = gf10  ; x=ψz = cong (&) (gf121 gp gq ) } where 
               gp = record { z = xp ; az = Pp ; x=ψz = peq } 
               gq = record { z = xq ; az = Pq ; x=ψz = qeq } 
@@ -270,7 +305,7 @@
 lemma232 : (P L p : HOD ) (C : CountableModel ) 
     →  (LP : L ⊆ Power P ) →  (Lp0 : L ∋ p  ) ( NEG : {p : HOD} → L ∋ p → L ∋ ( P ＼ p))
     →  ( {q : HOD} → (Lq : L ∋ q ) → NonAtomic L q Lq )
-    →  ¬ ( (ctl-M C) ∋  rgen ( P-GenericFilter P L p LP Lp0 NEG  C )) 
+    →  ¬ ( (ctl-M C) ∋  rgen ( P-GenericFilter P L p LP Lp0 ? NEG  C )) 
 lemma232 P L p C LP Lp0 NEG NA MG = {!!} where
     D : HOD  -- P - G
     D = ?