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

changeset 1254:abd86d493c61

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 11:56:17 +0900
parents 507f443c97ce
children afecaee48825
files src/generic-filter.agda
diffstat 1 files changed, 51 insertions(+), 30 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Wed Mar 15 22:45:05 2023 +0900
+++ b/src/generic-filter.agda	Thu Mar 16 11:56:17 2023 +0900
@@ -167,13 +167,17 @@
 ... | tri≈ ¬a refl ¬c = λ x → x
 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
 
+record Expansion  (L : HOD) {p : HOD } (dense : HOD) (Lp : L ∋ p) : Set (Level.suc n) where
+   field
+       expansion : HOD
+       dense∋exp : dense ∋ expansion 
+       p⊆exp : p ⊆ expansion 
+
 record Dense  {L P : HOD } (LP : L ⊆ Power P)  : Set (Level.suc n) where
    field
        dense : HOD
        d⊆P :  dense ⊆ L
-       dense-f : {p : HOD} → L ∋ p  → HOD
-       dense-d :  { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt
-       dense-p :  { p : HOD} → (lt : L ∋ p) → p ⊆ dense-f lt
+       has-expansion : {p : HOD} → (Lp : L ∋ p) → Expansion L dense Lp
 
 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (Level.suc n) where
     field
@@ -181,9 +185,9 @@
     rgen : HOD
     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  → L ∋ ( P ＼ q) → rgen ∋ q
-       gfilter2 : {p q : HOD} → (rgen ∋ p ) ∧ (rgen ∋ q) → rgen ∋ (p ∪ q)
+       generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ rgen ) ≡ od∅ )
+       gideal1 : {p q : HOD} → rgen ∋ p → q ⊆ p  → L ∋ ( P ＼ q) → rgen ∋ q
+       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
@@ -193,8 +197,8 @@
 P-GenericFilter P L p0 L⊆PP Lp0 CAP UNI NEG 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 )
-    ; gfilter1 = gfilter1
-    ; gfilter2 = gfilter2
+    ; gideal1 = gideal1
+    ; gideal2 = gideal2
    } where
     GP =  Replace (PDHOD L p0 C) (λ x → P ＼ x)
     GPR = Replace GP (_＼_ P) 
@@ -309,6 +313,7 @@
     fdense : (D : Dense {L} {P} L⊆PP ) → (ctl-M C ) ∋ Dense.dense D  → ¬ (Dense.dense D ∩ (PDHOD L p0 C)) ≡ od∅
     fdense D MD eq0  = ⊥-elim (  ∅< {Dense.dense D ∩ PDHOD L p0 C} fd01 (≡od∅→=od∅ eq0 )) where
        open Dense
+       open Expansion
        fd09 : (i : ℕ ) → odef L (find-p L C i (& p0))
        fd09 zero = Lp0
        fd09 (suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) )
@@ -334,13 +339,14 @@
        ... | yes y = ⊥-elim ( ¬x<0 ( _==_.eq→ fd10 fd21 ) ) where
           L∋pn : L ∋ * (find-p L C an (& p0))
           L∋pn = subst (λ k → odef L k) (sym &iso) (fd09 an )
-          L∋df : L ∋ ( dense-f D L∋pn )
-          L∋df = (d⊆P D) (  dense-d D L∋pn )
-          pn∋df : (* (ctl→ C an)) ∋ ( dense-f D L∋pn )
-          pn∋df = subst (λ k → odef k (& ( dense-f D L∋pn ) )) d=an (  dense-d D L∋pn ) 
-          pn⊆df : (y : Ordinal) → odef (* (find-p L C an (& p0))) y → odef (* (& (dense-f D L∋pn))) y
-          pn⊆df y py = subst (λ k → odef k y ) (sym *iso) (dense-p D L∋pn py)
-          fd21 : odef (PGHOD an L C (find-p L C an (& p0)) ) (& (dense-f D L∋pn))
+          exp = has-expansion D L∋pn
+          L∋df : L ∋ ( expansion exp )
+          L∋df = (d⊆P D) (dense∋exp exp)
+          pn∋df : (* (ctl→ C an)) ∋ ( expansion exp)
+          pn∋df = subst (λ k → odef k (& ( expansion exp))) d=an (dense∋exp exp )
+          pn⊆df : (y : Ordinal) → odef (* (find-p L C an (& p0))) y → odef (* (& (expansion exp))) y
+          pn⊆df y py = subst (λ k → odef k y ) (sym *iso) (p⊆exp exp py)
+          fd21 : odef (PGHOD an L C (find-p L C an (& p0)) ) (& (expansion exp))
           fd21 = ⟪ L∋df , ⟪ pn∋df , pn⊆df ⟫ ⟫
           fd10 :  PGHOD an L C (find-p L C an (& p0)) =h= od∅
           fd10 = ≡o∅→=od∅ y
@@ -380,8 +386,8 @@
            & (* 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 → 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 
+    gideal1 : {p q : HOD} → GPR ∋ p → q ⊆ p → L ∋  ( P ＼ q) → GPR ∋ q
+    gideal1 {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
@@ -403,8 +409,8 @@
         gf32 = proj1 (＼-⊆ {P} {q} {p} q⊆P ) q⊆p 
         gf30 : GP ∋ (P ＼ q )
         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 ⟫ 
+    gideal2 : {p q : HOD} → (GPR ∋ p) ∧ (GPR ∋ q) → Replace GP (_＼_ P) ∋ (p ∪ q)
+    gideal2 {p} {q} ⟪ gp , gq ⟫ 
        = record { z = _ ; az = gf31 ; x=ψz = cong (&) gf32  } where
         open ≡-Reasoning
         gf31 : GP ∋ ( (P ＼ p ) ∩ (P ＼ q ) )
@@ -439,7 +445,7 @@
       → 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 (proj2 rgf∩D) (proj1 rgf∩D)) 
+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)) 
         ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where
     PG = P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG  C 
     GF =  genf PG
@@ -449,19 +455,34 @@
     D = L ＼ rgf
     M∋DM : M ∋ (D ∩ M )
     M∋DM = is-model C D ?
+    M∋D : M ∋ D 
+    M∋D = ?
+    M∋G : M ∋ rgf
+    M∋G = MF
     D⊆PP : D ⊆ Power P
     D⊆PP {x} ⟪ Lx , ngx ⟫  = LPP Lx 
     DD : Dense {L} {P} LPP
-    Dense.dense DD = D
-    Dense.d⊆P DD ⟪ Lx , _ ⟫ = Lx
-    Dense.dense-f DD Lp = ll00 where
-        ll00 : HOD
-        ll00 with NotCompatible.¬compat (NC Lp)
-        ... | nc = ? 
-    Dense.dense-d DD = ?
-    Dense.dense-p DD = ?
-    ¬rgf∩D=0 : ¬ ( (rgf ∩ D) =h= od∅ )
-    ¬rgf∩D=0 = ?
+    DD = record { dense = D ; d⊆P = proj1 ; has-expansion = exp } where
+        exp : {p : HOD} → (Lp : L ∋ p) → Expansion L D Lp
+        exp {p} Lp = exp1 where
+            q : HOD
+            q = NotCompatible.q (NC Lp)
+            r : HOD
+            r = NotCompatible.r (NC Lp)
+            exp1 : Expansion L D Lp
+            exp1  with ODC.p∨¬p O (rgf ∋ q)
+            ... | case2 ngq = record { expansion = q  ; dense∋exp = ? ; p⊆exp = ? }  
+            ... | case1 gq with ODC.p∨¬p O (rgf ∋ r)
+            ... | 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 
+                ll03 : rgf ∋ p → rgf ∋ q → rgf ∋ (p ∪ q)
+                ll03 rp rq = gideal2 PG ⟪ rp , rq ⟫ 
+                ll04 : rgf ∋ p → q ⊆ p → rgf ∋ q
+                ll04 rp q⊆p = gideal1 PG rp q⊆p ?
+    ¬rgf∩D=0 : ¬ ( (D ∩ rgf ) =h= od∅ )
+    ¬rgf∩D=0 eq =  generic PG DD M∋D (==→o≡ eq)
 
 --
 -- P-Generic Filter defines a countable model D ⊂ C from P