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

changeset 1255:afecaee48825

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 Thu, 16 Mar 2023 17:46:36 +0900
parents abd86d493c61
children 0b7e4eb68afc
files src/filter.agda src/generic-filter.agda
diffstat 2 files changed, 37 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Thu Mar 16 11:56:17 2023 +0900
+++ b/src/filter.agda	Thu Mar 16 17:46:36 2023 +0900
@@ -156,7 +156,7 @@
        ideal : HOD   
        i⊆L :  ideal ⊆ L 
        ideal1 : { p q : HOD } →  L ∋ q  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
-       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)
+       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → L ∋ (p ∩ q) → ideal ∋ (p ∪ q)
 
 open Ideal
 
--- a/src/generic-filter.agda	Thu Mar 16 11:56:17 2023 +0900
+++ b/src/generic-filter.agda	Thu Mar 16 17:46:36 2023 +0900
@@ -179,6 +179,23 @@
        d⊆P :  dense ⊆ L
        has-expansion : {p : HOD} → (Lp : L ∋ p) → Expansion L dense Lp
 
+record GenericFilter1 {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (Level.suc n) where
+    field
+       genf : Ideal {L} {P} LP
+       generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Ideal.ideal genf ) ≡ od∅ )
+
+P-GenericFilter1 : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0
+      → (C : CountableModel ) → GenericFilter1 {L} {P} LP ( ctl-M C )
+P-GenericFilter1 P L p0 L⊆PP Lp0 C = record {
+      genf = record { ideal = PDHOD L p0 C ; i⊆L = x∈PP ; ideal1 = ideal1 ; ideal2 =  ? }
+    ; generic = ?
+   } where
+       ideal1 : {p q : HOD} → L ∋ q → PDHOD L p0 C ∋ p → q ⊆ p → PDHOD L p0 C ∋ q
+       ideal1 {p} {q} Lq record { gr = gr ; pn<gr = pn<gr ; x∈PP = x∈PP } q⊆p = 
+                 record { gr = gr ; pn<gr = λ y qy → pn<gr y ? ; x∈PP = ? }  where
+            gf00 : {y : Ordinal } →  odef (* (& q)) y → odef (* (& q)) y  
+            gf00 {y} qy = subst (λ k → odef k y ) ? (q⊆p (subst (λ k → odef k y) ? qy ))
+
 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (Level.suc n) where
     field
        genf : Filter {L} {P} LP
@@ -190,11 +207,8 @@
        gideal2 : {p q : HOD} → (rgen ∋ p ) ∧ (rgen ∋ q) → rgen ∋ (p ∪ q)
 
 P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0
-      → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q ))  -- L is a Boolean Algebra
-      → (UNI : {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 CAP UNI NEG C = record {
+P-GenericFilter P L p0 L⊆PP Lp0 C = record {
       genf = record { filter = Replace (PDHOD L p0 C) (λ x → P ＼ x)  ; f⊆L =  gf01 ; filter1 = f1 ; filter2 = f2 }
     ; generic = λ D cd → subst (λ k → ¬ (Dense.dense D ∩ k) ≡ od∅ ) (sym gf00) (fdense D cd )
     ; gideal1 = gideal1
@@ -205,7 +219,7 @@
     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)) )
+    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)) )
     gf141 : {xp xq : Ordinal } → (Pp : PDN L p0 C xp) (Pq : PDN L p0 C xq) →  (* xp ∪ * xq) ⊆ P
     gf141 Pp Pq {x} (case1 xpx) = L⊆PP (PDN.x∈PP Pp)  _ xpx
     gf141 Pp Pq {x} (case2 xqx) = L⊆PP (PDN.x∈PP Pq)  _ xqx
@@ -226,7 +240,7 @@
 
     f1 : {p q : HOD} → L ∋ q → Replace (PDHOD L p0 C) (λ x → P ＼ x) ∋ p → p ⊆ q → Replace (PDHOD L p0 C) (λ x → P ＼ x) ∋ q
     f1 {p} {q} L∋q record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = _ 
-       ; az = record { gr = gr az ;  pn<gr = f04 ; x∈PP = NEG L∋q } ; x=ψz = f05 } where
+       ; az = record { gr = gr az ;  pn<gr = f04 ; x∈PP = ? } ; x=ψz = f05 } where
        open ≡-Reasoning
        f04 : (y : Ordinal) → odef (* (& (P ＼ q))) y → odef (* (find-p L C (gr az ) (& p0))) y
        f04 y qy = PDN.pn<gr az  _ (subst (λ k → odef k y ) f06 (f03 qy ))  where
@@ -253,24 +267,24 @@
           gp = record { z = xp ; az = Pp ; x=ψz = peq }
           gq = record { z = xq ; az = Pq ; x=ψz = qeq }
           gf10 : odef (PDHOD L p0 C) (& (* xp ∪ * xq))
-          gf10 = record { gr = PDN.gr Pq ; pn<gr = gf15 ; x∈PP = subst (λ k → odef L k) (cong (&) (gf131 gp gq)) ( NEG L∋pq ) } where
+          gf10 = record { gr = PDN.gr Pq ; pn<gr = gf15 ; x∈PP = subst (λ k → odef L k) (cong (&) (gf131 gp gq)) ? } where
              gf16 : gr Pp ≤ gr Pq
              gf16 = <to≤ a
              gf15 :  (y : Ordinal) → odef (* (& (* xp ∪ * xq))) y → odef (* (find-p L C (gr Pq) (& p0))) y
              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 eq ¬c = record { z = & (* xp ∪ * xq) ; az = record { gr = gr Pp ; pn<gr = gf21 ; x∈PP = gf22 } ; x=ψz = gf23 } where
+    ... | tri≈ ¬a eq ¬c = record { z = & (* xp ∪ * xq) ; az = record { gr = gr Pp ; pn<gr = gf21 ; x∈PP = ? } ; x=ψz = gf23 } where
           gp = record { z = xp ; az = Pp ; x=ψz = peq }
           gq = record { z = xq ; az = Pq ; x=ψz = qeq }
           gf22 : odef L (& (* xp ∪ * xq))
-          gf22 = UNI (subst (λ k → odef L k ) (sym &iso) (PDN.x∈PP Pp)) (subst (λ k → odef L k ) (sym &iso) (PDN.x∈PP Pq))
+          gf22 = ?
           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
           ... | case1 xpy = PDN.pn<gr Pp _ xpy
           ... | case2 xqy = subst (λ k → odef (* (find-p L C k (& p0))) y ) (sym eq) ( PDN.pn<gr Pq _ xqy )
           gf25 : odef L (& p)
-          gf25 = subst (λ k → odef L k ) (sym peq) ( NEG (subst (λ k → odef L k) (sym &iso) (PDN.x∈PP Pp) ))
+          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
           -- gf02 : {P a b : HOD } → (P ＼ a) ∩ (P ＼ b) ≡ ( P ＼ (a ∪ b) )
@@ -280,7 +294,7 @@
           gp = record { z = xp ; az = Pp ; x=ψz = peq }
           gq = record { z = xq ; az = Pq ; x=ψz = qeq }
           gf10 : odef (PDHOD L p0 C) (& (* xp ∪ * xq))
-          gf10 = record { gr = PDN.gr Pp ; pn<gr = gf15 ; x∈PP = subst (λ k → odef L k) (cong (&) (gf131 gp gq)) ( NEG L∋pq ) } where
+          gf10 = record { gr = PDN.gr Pp ; pn<gr = gf15 ; x∈PP = subst (λ k → odef L k) (cong (&) (gf131 gp gq)) ?  } where
              gf16 : gr Pq ≤ gr Pp
              gf16 = <to≤ c
              gf15 :  (y : Ordinal) → odef (* (& (* xp ∪ * xq))) y → odef (* (find-p L C (gr Pp) (& p0))) y
@@ -366,7 +380,7 @@
     ... | ⟪ Px , npz ⟫ = Px
     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 } 
-      = ⟪ subst (λ k → odef L k) fd40 (PDN.x∈PP az) , NEG (subst (λ k → odef L k) fd40 (PDN.x∈PP az)) ⟫ where
+      = ⟪ 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
@@ -414,7 +428,7 @@
        = 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 (proj2 (L∋gpr gp)) (proj2 (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 )
@@ -435,19 +449,16 @@
       Lr : L ∋ r
       p⊆q : p ⊆ q  
       p⊆r : p ⊆ r  
-      ¬compat : (s : HOD) → ¬ ( (q ⊆ s) ∧ (r ⊆ s) )
+      ¬compat : (s : HOD) → L ∋ s → ¬ ( (q ⊆ s) ∧ (r ⊆ s) )
 
 lemma232 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
-      → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q ))  -- L is a Boolean Algebra
-      → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q ))
-      → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)))
       → (C : CountableModel ) 
       → ctl-M C ∋ L
       → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp )
-      →  ¬ ( ctl-M C ∋  rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG  C ))
-lemma232 P L p0 LPP Lp0 CAP UNI NEG C ML NC MF = ¬rgf∩D=0 record { eq→ = λ {x} rgf∩D → ⊥-elim( proj2 (proj1 rgf∩D) (proj2 rgf∩D)) 
+      →  ¬ ( ctl-M C ∋  rgen ( P-GenericFilter P L p0 LPP Lp0 C ))
+lemma232 P L p0 LPP Lp0 C ML NC MF = ¬rgf∩D=0 record { eq→ = λ {x} rgf∩D → ⊥-elim( proj2 (proj1 rgf∩D) (proj2 rgf∩D)) 
         ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where
-    PG = P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG  C 
+    PG = P-GenericFilter P L p0 LPP Lp0 C 
     GF =  genf PG
     rgf =  rgen PG
     M = ctl-M C
@@ -469,6 +480,8 @@
             q = NotCompatible.q (NC Lp)
             r : HOD
             r = NotCompatible.r (NC Lp)
+            Lq : L ∋ q
+            Lq = NotCompatible.Lq (NC Lp)
             exp1 : Expansion L D Lp
             exp1  with ODC.p∨¬p O (rgf ∋ q)
             ... | case2 ngq = record { expansion = q  ; dense∋exp = ? ; p⊆exp = ? }  
@@ -476,7 +489,9 @@
             ... | case2 ngr = record { expansion = q  ; dense∋exp = ? ; p⊆exp = ? }  
             ... | case1 gr = ⊥-elim ( ll02 ⟪ ? , ? ⟫ ) where
                 ll02 : ¬ ( (q ⊆ p) ∧ (r ⊆ p) )
-                ll02 = NotCompatible.¬compat (NC Lp) p 
+                ll02 = NotCompatible.¬compat (NC Lp) p ? 
+                ll05 : ¬ ( (q ⊆ (q ∪ r) ∧ (r ⊆ (q ∪ r)) ))
+                ll05 = NotCompatible.¬compat (NC Lp )  (q ∪ r) ?
                 ll03 : rgf ∋ p → rgf ∋ q → rgf ∋ (p ∪ q)
                 ll03 rp rq = gideal2 PG ⟪ rp , rq ⟫ 
                 ll04 : rgf ∋ p → q ⊆ p → rgf ∋ q