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

changeset 1241:5f1572d1f19a

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 Mon, 13 Mar 2023 01:30:55 +0900
parents fbe072447243
children e843ace90b31
files src/BAlgebra.agda src/generic-filter.agda
diffstat 2 files changed, 21 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/BAlgebra.agda	Sun Mar 12 13:02:09 2023 +0900
+++ b/src/BAlgebra.agda	Mon Mar 13 01:30:55 2023 +0900
@@ -63,6 +63,12 @@
 ... | yes y = case1 ( subst (λ k → odef X k ) &iso y  )
 ... | no  n = case2 ⟪ Lx , subst (λ k → ¬ odef X k) &iso n ⟫
 
+＼-⊆ : { P A B : HOD } →  A ⊆ P → ( A ⊆ B → ( P ＼ B ) ⊆ ( P ＼ A )) ∧ (( P ＼ B ) ⊆ ( P ＼ A ) → A ⊆ B ) 
+＼-⊆ {P} {A} {B} A⊆P = ⟪ ( λ a<b {x} pbx → ⟪ proj1 pbx  , (λ ax → proj2 pbx (a<b ax))   ⟫ )  , lem07 ⟫ where
+    lem07 : (P ＼ B) ⊆ (P ＼ A) → A ⊆ B
+    lem07 pba {x} ax with ODC.p∨¬p O (odef B x)
+    ... | case1 bx = bx
+    ... | case2 ¬bx = ⊥-elim ( proj2 ( pba ⟪ A⊆P ax  , ¬bx ⟫ ) ax )
 
 [a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅
 [a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
--- a/src/generic-filter.agda	Sun Mar 12 13:02:09 2023 +0900
+++ b/src/generic-filter.agda	Mon Mar 13 01:30:55 2023 +0900
@@ -159,17 +159,24 @@
     rgen : HOD
     rgen = Replace (Filter.filter genf) (λ x → P ＼ x )
 
-P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C )
-P-GenericFilter P L p0 L⊆PP Lp0 C = record {
-      genf = record { filter = Replace (PDHOD L p0 C) (λ x → P ＼ x)  ; f⊆L =  ? ; filter1 = ? ; filter2 = ? }
+-- ＼-⊆
+
+P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 → ({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 {
+      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
+        GP =  Replace (PDHOD L p0 C) (λ x → P ＼ x) 
         f⊆PL :  PDHOD L p0 C ⊆ L 
         f⊆PL lt = x∈PP lt  
+        gf01 : Replace (PDHOD L p0 C) (λ x → P ＼ x) ⊆ L
+        gf01 {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef L k) (sym x=ψz) ( NEG (subst (λ k → odef L k) (sym &iso) (f⊆PL az)) )
         f1 : {p q : HOD} → L ∋  q → PDHOD L p0 C ∋ p → p ⊆ q → PDHOD L p0 C ∋ q
         f1 {p} {q} L∋q PD∋p p⊆q =  ?
-        f2 : {p q : HOD} → ? ∋ p → ? ∋ q → L ∋ (p ∩ q) → ? ∋ (p ∩ q)
-        f2 {p} {q} PD∋p PD∋q L∋pq with <-cmp (gr PD∋q) (gr PD∋p)
+        f2 : {p q : HOD} → GP ∋ p → GP ∋ q → L ∋ (p ∩ q) → GP ∋ (p ∩ q)
+        f2 {p} {q} record { z = xp ; az = Pp ; x=ψz = peq } 
+                   record { z = xq ; az = Pq ; x=ψz = qeq } L∋pq with <-cmp (gr Pp) (gr Pq) 
         ... | tri< a ¬b ¬c = ?
         ... | tri≈ ¬a eq ¬c = ?
         ... | tri> ¬a ¬b c = ? 
@@ -189,10 +196,10 @@
       b<a : b ⊆ a
 
 lemma232 : (P L p : HOD ) (C : CountableModel ) 
-    →  (LP : L ⊆ Power P ) →  (Lp0 : L ∋ p  )
+    →  (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  C )) 
-lemma232 P L p C LP Lp0 NA MG = {!!} where
+    →  ¬ ( (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 = ?