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

changeset 1260:8a8052df5254

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generic filter modification
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 18 Mar 2023 11:30:42 +0900
parents 4993a95d3fc8
children 2fccbe475cf7
files src/filter.agda src/generic-filter.agda
diffstat 2 files changed, 61 insertions(+), 54 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Fri Mar 17 11:33:20 2023 +0900
+++ b/src/filter.agda	Sat Mar 18 11:30:42 2023 +0900
@@ -160,6 +160,7 @@
 
 open Ideal
 
+
 proper-ideal : {L P : HOD} → (LP : L ⊆ Power P) → (P : Ideal {L} {P} LP ) → {p : HOD} → Set n
 proper-ideal {L} {P} LP I = ideal I ∋ od∅
 
--- a/src/generic-filter.agda	Fri Mar 17 11:33:20 2023 +0900
+++ b/src/generic-filter.agda	Sat Mar 18 11:30:42 2023 +0900
@@ -3,7 +3,7 @@
 open import Ordinals
 module generic-filter {n : Level.Level } (O : Ordinals {n})   where
 
-import filter
+-- import filter
 open import zf
 open import logic
 -- open import partfunc {n} O
@@ -35,7 +35,7 @@
 
 import ODC
 
-open filter O
+-- open filter O
 
 open _∧_
 open _∨_
@@ -150,27 +150,41 @@
 ... | 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
+record Expansion  (p : HOD) (dense : HOD)  : Set (Level.suc n) where
    field
        exp : HOD
        D∋exp : dense ∋ exp 
        p⊆exp : p ⊆ exp 
 
-record Dense  {L P : HOD } (LP : L ⊆ Power P)  : Set (Level.suc n) where
+record Dense  (L : HOD ) : Set (Level.suc n) where
    field
        dense : HOD
        d⊆P :  dense ⊆ L
-       has-exp : {p : HOD} → (Lp : L ∋ p) → Expansion L dense Lp
+       has-exp : {p : HOD} → (Lp : L ∋ p) → Expansion p dense 
+
+record Exp2 (I : HOD)  ( p q : HOD ) : Set (Level.suc n) where
+   field 
+       exp : HOD
+       I∋exp : I ∋ exp 
+       p⊆exp : p ⊆ exp 
+       q⊆exp : q ⊆ exp 
+
+record ⊆-Ideal {L P : HOD } (LP : L ⊆ Power P) : Set (Level.suc n) where
+   field
+       ideal : HOD   
+       i⊆L :  ideal ⊆ L 
+       ideal1 : { p q : HOD } →  L ∋ q  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
+       exp : { p q : HOD } → ideal ∋ p → ideal ∋ q → Exp2 ideal p q
 
 record GenericFilter {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∅ )
+       genf : ⊆-Ideal {L} {P} LP
+       generic : (D : Dense L ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ ⊆-Ideal.ideal genf ) ≡ od∅ )
 
 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 { ideal = PDHOD L p0 C ; i⊆L = x∈PP ; ideal1 = ideal1 ; ideal2 =  ideal2 }
+      genf = record { ideal = PDHOD L p0 C ; i⊆L = x∈PP ; ideal1 = ideal1 ; exp = λ ip iq → exp1 ip iq }
     ; generic = fdense
    } where
        ideal1 : {p q : HOD} → L ∋ q → PDHOD L p0 C ∋ p → q ⊆ p → PDHOD L p0 C ∋ q
@@ -178,41 +192,37 @@
                  record { gr = gr ; pn<gr = λ y qy → pn<gr y (gf00 qy) ; x∈PP = Lq }  where
             gf00 : {y : Ordinal } →  odef (* (& q)) y → odef (* (& p)) y  
             gf00 {y} qy = subst (λ k → odef k y ) (sym *iso) (q⊆p (subst (λ k → odef k y) *iso qy ))
-       ideal2 : {p q : HOD} → PDHOD L p0 C ∋ p → PDHOD L p0 C ∋ q → L ∋ (p ∪ q) → PDHOD L p0 C ∋ (p ∪ q)
-       ideal2 {p} {q} record { gr = pgr ; pn<gr = ppn ; x∈PP = PPp } 
-                      record { gr = qgr ; pn<gr = qpn ; x∈PP = PPq } Lpq = gf01 where
+       Lfp : (i : ℕ ) →  odef L (find-p L C i (& p0))
+       Lfp zero = Lp0
+       Lfp (suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) )
+       ... | yes y  = Lfp i
+       ... | no not  = proj1 ( ODC.x∋minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))) 
+       exp1 : {p q : HOD} → (ip : PDHOD L p0 C ∋ p) → (ip : PDHOD L p0 C ∋ q) → Exp2 (PDHOD L p0 C) p q
+       exp1 {p} {q} record { gr = pgr ; pn<gr = ppn ; x∈PP = PPp } 
+                      record { gr = qgr ; pn<gr = qpn ; x∈PP = PPq } = gf01 where
             Pp = record { gr = pgr ; pn<gr = ppn ; x∈PP = PPp } 
             Pq = record { gr = qgr ; pn<gr = qpn ; x∈PP = PPq } 
-            gf01 : PDHOD L p0 C ∋ (p ∪ q)
+            gf17 : {q : HOD} → (Pq : PDHOD L p0 C ∋ q ) → PDHOD L p0 C ∋ * (find-p L C (gr Pq) (& p0))
+            gf17 {q} Pq = record { gr = PDN.gr Pq  ; pn<gr = λ y qq → subst (λ k → odef (* k) y) &iso qq  
+                 ; x∈PP = subst (λ k → odef L k ) (sym &iso) (Lfp (PDN.gr Pq))  } 
+            gf01 : Exp2 (PDHOD L p0 C) p q
             gf01 with <-cmp pgr qgr
-            ... | tri< a ¬b ¬c = record { gr = qgr ; pn<gr = gf03 ; x∈PP = Lpq } where
-               gf03 : (y : Ordinal) → odef (* (& (p ∪ q))) y → odef (* (find-p L C qgr (& p0))) y
-               gf03 y pqy = gf15 y pqy where
+            ... | tri< a ¬b ¬c = record { exp = * (find-p L C (gr Pq) (& p0))  ; I∋exp = gf17 Pq ; p⊆exp = λ px → gf15 _ px 
+                    ; q⊆exp = λ {x} qx → qpn _ (subst (λ k → odef k x) (sym *iso) qx)  } where
                  gf16 : gr Pp ≤ gr Pq
                  gf16 = <to≤ a
-                 gf15 :  (y : Ordinal) → odef (* (& (p ∪ q))) 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 (subst (λ k → odef k y) (sym *iso) xpy) )
-                 ... | case2 xqy = PDN.pn<gr Pq _ (subst (λ k → odef k y) (sym *iso) xqy)
-            ... | tri≈ ¬a refl ¬c = record { gr = qgr ; pn<gr = gf03 ; x∈PP = Lpq } where
-               gf03 : (y : Ordinal) → odef (* (& (p ∪ q))) y → odef (* (find-p L C qgr (& p0))) y
-               gf03 y pqy = gf15 y pqy where
-                 gf16 : gr Pp ≤ gr Pq
-                 gf16 = ≤-refl
-                 gf15 :  (y : Ordinal) → odef (* (& (p ∪ q))) 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 (subst (λ k → odef k y) (sym *iso) xpy) )
-                 ... | case2 xqy = PDN.pn<gr Pq _ (subst (λ k → odef k y) (sym *iso) xqy)
-            ... | tri> ¬a ¬b c = record { gr = pgr ; pn<gr = gf03 ; x∈PP = Lpq } where
-               gf03 : (y : Ordinal) → odef (* (& (p ∪ q))) y → odef (* (find-p L C pgr (& p0))) y
-               gf03 y ppy = gf15 y ppy where
+                 gf15 :  (y : Ordinal) → odef p y → odef (* (find-p L C (gr Pq) (& p0))) y
+                 gf15 y xpy = p-monotonic L p0 C gf16 (PDN.pn<gr Pp y (subst (λ k → odef k y) (sym *iso) xpy) )
+            ... | tri≈ ¬a refl ¬c = record { exp = * (find-p L C (gr Pq) (& p0))  ; I∋exp = gf17 Pq
+                    ; p⊆exp = λ {x} px → ppn _ (subst (λ k → odef k x) (sym *iso) px)   
+                    ; q⊆exp = λ {x} qx → qpn _ (subst (λ k → odef k x) (sym *iso) qx)  } 
+            ... | tri> ¬a ¬b c = record { exp = * (find-p L C (gr Pp) (& p0))  ; I∋exp = gf17 Pp ; q⊆exp = λ qx → gf15 _ qx 
+                    ; p⊆exp = λ {x} px → ppn _ (subst (λ k → odef k x) (sym *iso) px)  } where
                  gf16 : gr Pq ≤ gr Pp
                  gf16 = <to≤ c
-                 gf15 :  (y : Ordinal) → odef (* (& (p ∪ q))) y → odef (* (find-p L C (gr Pp) (& p0))) y
-                 gf15 y gppy with subst (λ k → odef k y ) *iso gppy
-                 ... | case2 xqy = p-monotonic L p0 C gf16 (PDN.pn<gr Pq y (subst (λ k → odef k y) (sym *iso) xqy) )
-                 ... | case1 xpy = PDN.pn<gr Pp _ (subst (λ k → odef k y) (sym *iso) xpy)
-       fdense : (D : Dense {L} {P} L⊆PP ) → (ctl-M C ) ∋ Dense.dense D  → ¬ (Dense.dense D ∩ (PDHOD L p0 C)) ≡ od∅
+                 gf15 :  (y : Ordinal) → odef q y → odef (* (find-p L C (gr Pp) (& p0))) y
+                 gf15 y xqy = p-monotonic L p0 C gf16 (PDN.pn<gr Pq y (subst (λ k → odef k y) (sym *iso) xqy) )
+       fdense : (D : Dense L ) → (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
@@ -264,7 +274,7 @@
            fd01 = ⟪ subst (λ k → odef (dense D)  k ) (sym &iso) fd07 , subst (λ k → odef  (PDHOD L p0 C) k) (sym &iso) fd03 ⟫  
 
 open GenericFilter
-open Filter
+-- open Filter
 
 record NotCompatible  (L p : HOD ) (L∋a : L ∋ p ) : Set (Level.suc (Level.suc n)) where
    field
@@ -279,26 +289,26 @@
       → (C : CountableModel ) 
       → ctl-M C ∋ L
       → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp )
-      →  ¬ ( ctl-M C ∋  Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C )))
+      →  ¬ ( ctl-M C ∋  ⊆-Ideal.ideal (genf ( 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 C 
     GF =  genf PG
-    rgf =  Ideal.ideal (genf PG)
+    rgf =  ⊆-Ideal.ideal (genf PG)
     M = ctl-M C
     D : HOD  
     D = L ＼ rgf
     M∋DM : M ∋ (D ∩ M )
     M∋DM = is-model C D ?
+    -- M∋G : M ∋ rgf
+    -- M∋G = MF
     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
+    DD : Dense L 
     DD = record { dense = D ; d⊆P = proj1 ; has-exp = exp } where
-        exp : {p : HOD} → (Lp : L ∋ p) → Expansion L D Lp
+        exp : {p : HOD} → (Lp : L ∋ p) → Expansion p D 
         exp {p} Lp = exp1 where
             q : HOD
             q = NotCompatible.q (NC Lp)
@@ -308,20 +318,16 @@
             Lq = NotCompatible.Lq (NC Lp)
             Lr : L ∋ r
             Lr = NotCompatible.Lr (NC Lp)
-            exp1 : Expansion L D Lp
+            exp1 : Expansion p D 
             exp1  with ODC.p∨¬p O (rgf ∋ q)
             ... | case2 ngq = record { exp = q  ; D∋exp = ⟪ Lq , ngq ⟫ ; p⊆exp = NotCompatible.p⊆q (NC Lp)}  
             ... | case1 gq with ODC.p∨¬p O (rgf ∋ r)
             ... | case2 ngr = record { exp = r  ; D∋exp = ⟪ Lr , ngr ⟫ ; p⊆exp = NotCompatible.p⊆r (NC Lp)}  
-            ... | case1 gr = ⊥-elim ( ll02 ⟪ ? , ? ⟫ ) where
-                ll02 : ¬ ( (q ⊆ p) ∧ (r ⊆ 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 = Ideal.ideal2 GF rp rq ? -- ⟪ rp , rq ⟫ 
-                ll04 : rgf ∋ p → q ⊆ p → rgf ∋ q
-                ll04 rp q⊆p = Ideal.ideal1 GF Lq rp q⊆p 
+            ... | case1 gr = ⊥-elim ( NotCompatible.¬compat (NC Lp) ex2 Le ⟪  q⊆ex2 , r⊆ex2 ⟫ ) where
+                ex2 = Exp2.exp (⊆-Ideal.exp GF gq gr)
+                Le =  ⊆-Ideal.i⊆L GF (Exp2.I∋exp (⊆-Ideal.exp GF gq gr))
+                q⊆ex2 = Exp2.p⊆exp (⊆-Ideal.exp GF gq gr) 
+                r⊆ex2 = Exp2.q⊆exp (⊆-Ideal.exp GF gq gr) 
     ¬rgf∩D=0 : ¬ ( (D ∩ rgf ) =h= od∅ )
     ¬rgf∩D=0 eq =  generic PG DD M∋D (==→o≡ eq)
 
@@ -352,5 +358,5 @@
     →  HOD
 val x G = TransFinite {λ x → HOD } ind (& x) where
   ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
-  ind x valy = record { od = record { def = λ y → valS x y (& (Ideal.ideal (genf G))) } ; odmax = {!!} ; <odmax = {!!} }
+  ind x valy = record { od = record { def = λ y → valS x y (& (⊆-Ideal.ideal (genf G))) } ; odmax = {!!} ; <odmax = {!!} }