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

changeset 458:882c24efdc3f

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 Fri, 18 Mar 2022 20:36:42 +0900
parents 5f8243d1d41b
children 3d84389cc43f
files src/filter.agda
diffstat 1 files changed, 46 insertions(+), 43 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Thu Mar 17 16:40:54 2022 +0900
+++ b/src/filter.agda	Fri Mar 18 20:36:42 2022 +0900
@@ -38,7 +38,7 @@
 open Bool
 
 -- Kunen p.76 and p.53, we use ⊆
-record Filter  ( L : HOD  ) : Set (suc n) where
+record Filter  { L P : HOD  } (LP : L ⊆ Power P) : Set (suc n) where
    field
        filter  : HOD   
        f⊆L     : filter ⊆ L
@@ -47,21 +47,23 @@
 
 open Filter
 
-record prime-filter { L : HOD } (F : Filter L) : Set (suc (suc n)) where
+record prime-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter LP) : Set (suc (suc n)) where
    field
        proper  : ¬ (filter F ∋ od∅)
-       prime   : {p q : HOD } →  filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
+       prime   : {p q : HOD } → L ∋ p → L ∋ q  →  filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
 
-record ultra-filter { L : HOD } (P : HOD ) (F : Filter L) : Set (suc (suc n)) where
+record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter LP) : Set (suc (suc n)) where
    field
-       L⊆PP :  L ⊆ Power P
        proper  : ¬ (filter F ∋ od∅)
        ultra   : {p : HOD } → L ∋ p →  ( filter F ∋ p ) ∨ (  filter F ∋ ( P ＼ p) )
 
 open _⊆_
 
-∈-filter : {L p : HOD} → (F : Filter L ) → filter F ∋ p → L ∋ p 
-∈-filter {L} {p} F lt = incl ( f⊆L F) lt 
+∈-filter : {L P p : HOD} →  {LP : L ⊆ Power P}  → (F : Filter LP ) → filter F ∋ p → L ∋ p 
+∈-filter {L} {p} {LP} F lt = incl ( f⊆L F) lt 
+
+⊆-filter : {L P p q : HOD } →  {LP : L ⊆ Power P } → (F : Filter LP) →  L ∋ q → q ⊆ P
+⊆-filter {L} {P} {p} {q} {LP} F lt = power→⊆ P q ( incl LP lt )
 
 ∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
@@ -69,12 +71,6 @@
 ∪-lemma2 : {L p q : HOD } → (p ∪ q)  ⊆ L → q ⊆ L
 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
 
-∪-lemma3 : {L P p q : HOD } → L ⊆ Power P → L ∋ (p ∪ q)  → L ∋ p
-∪-lemma3 = {!!}
-
-∪-lemma4 : {L P p q : HOD } →  L ⊆ Power P →  L ∋ (p ∪ q)  → L ∋ q
-∪-lemma4 = {!!}
-
 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
 q∩q⊆q = record { incl = λ lt → proj1 lt } 
 
@@ -85,28 +81,28 @@
 --  ultra filter is prime
 --
 
-filter-lemma1 :  {P L : HOD} → (F : Filter L)  → ∀ {p q : HOD } → ultra-filter P F  → prime-filter F 
-filter-lemma1 {P} {L} F u = record {
+filter-lemma1 :  {P L : HOD} → (LP : L ⊆ Power P)  → (F : Filter LP)  → ∀ {p q : HOD } → ultra-filter F  → prime-filter F 
+filter-lemma1 {P} {L} LP F u = record {
          proper = ultra-filter.proper u
        ; prime = lemma3
     } where
-  lemma3 : {p q : HOD} → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
-  lemma3 {p} {q} lt with ultra-filter.ultra u (∈-filter F lt) 
-  ... | case1 p∈P  = case1 {!!} -- (∪-lemma3 (ultra-filter.L⊆PP u) ? ) --  : OD.def (od (filter F)) (& p)
-  ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (L ＼ p)} {!!} lemma7 lemma8) where
-    lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h=  (q ∩ (L ＼ p))
+  lemma3 : {p q : HOD} → L ∋ p → L ∋ q  → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
+  lemma3 {p} {q} Lp Lq lt with ultra-filter.ultra u Lp
+  ... | case1 p∈P  = case1 p∈P 
+  ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (P ＼ p)} Lq lemma7 lemma8) where
+    lemma5 : ((p ∪ q ) ∩ (P ＼ p)) =h=  (q ∩ (P ＼ p))
     lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt  ⟫
        ;  eq← = λ {x} lt → ⟪  case2 (proj1 lt) , proj2 lt ⟫
       } where
-         lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x
+         lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (P ＼ p)) x → odef q x
          lemma4 x lt with proj1 lt
          lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
          lemma4 x lt | case2 qx = qx
     lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p))
-    lemma6 = {!!} -- filter2 F lt ¬p∈P
-    lemma7 : filter F ∋ (q ∩ (L ＼ p))
-    lemma7 =  subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) {!!}
-    lemma8 : (q ∩ (L ＼ p)) ⊆ q
+    lemma6 = filter2 F lt ¬p∈P
+    lemma7 : filter F ∋ (q ∩ (P ＼ p))
+    lemma7 =  subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) lemma6
+    lemma8 : (q ∩ (P ＼ p)) ⊆ q
     lemma8 = q∩q⊆q
 
 -----
@@ -114,23 +110,30 @@
 --  if Filter contains L, prime filter is ultra
 --
 
-filter-lemma2 :  {P L : HOD} → (F : Filter L)  → filter F ∋ L → prime-filter F → ultra-filter P F
-filter-lemma2 {P} {L} F f∋L prime = record {
-         L⊆PP = {!!}
-       ; proper = prime-filter.proper prime
-       ; ultra = λ {p}  p⊆L → prime-filter.prime prime {!!} -- (lemma p  p⊆L)
+filter-lemma2 :  {P L : HOD} → (LP : L ⊆ Power P) → (F : Filter LP)  → filter F ∋ L → prime-filter F → ultra-filter F
+filter-lemma2 {P} {L} LP F f∋L prime = record {
+         proper = prime-filter.proper prime
+       ; ultra = λ {p}  p⊆L → prime-filter.prime prime {!!} {!!} {!!} -- (lemma p  p⊆L)
    } where
         open _==_
-        p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) 
+        p+1-p=1 : {p : HOD} → p ⊆ P → P =h= (p ∪ (P ＼ p)) 
         eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
         eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
         eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫
-        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) &iso (incl p⊆L ( subst (λ k → odef p k) (sym &iso) p∋x  )) 
+        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef P k ) &iso (incl p⊆L ( subst (λ k → odef p k) (sym &iso) p∋x  )) 
         eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p  ) = proj1 ¬p
-        lemma : (p : HOD) → p ⊆ L   →  filter F ∋ (p ∪ (P ＼ p))
-        lemma p p⊆L = {!!} -- subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
+        lemma : (p : HOD) → p ⊆ P   →  filter F ∋ (p ∪ (P ＼ p))
+        lemma p p⊆L = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) {!!} -- f∋L
 
-record Dense  (L : HOD )  : Set (suc n) where
+-----
+--
+--  if there is a filter , there is a ultra filter under the axiom of choise
+--
+
+filter→ultra :  {P L : HOD} → (LP : L ⊆ Power P) → (F : Filter LP)  → ultra-filter F
+filter→ultra {P} {L} LP F = ?
+
+record Dense  {L P : HOD } (LP : L ⊆ Power P)  : Set (suc n) where
    field
        dense : HOD
        d⊆P :  dense ⊆ L
@@ -138,7 +141,7 @@
        dense-d :  { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt
        dense-p :  { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p  
 
-record Ideal  ( L : HOD  ) : Set (suc n) where
+record Ideal   {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where
    field
        ideal : HOD   
        i⊆L :  ideal ⊆ L 
@@ -147,15 +150,15 @@
 
 open Ideal
 
-proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n
-proper-ideal {L} P {p} = ideal P ∋ od∅
+proper-ideal : {L P : HOD} → (LP : L ⊆ Power P) → (P : Ideal LP ) → {p : HOD} → Set n
+proper-ideal {L} {P} LP I = ideal I ∋ od∅
 
-prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
-prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
+prime-ideal : {L P : HOD} → (LP : L ⊆ Power P) → Ideal LP → ∀ {p q : HOD } → Set n
+prime-ideal {L} {P} LP I {p} {q} =  ideal I ∋ ( p ∩ q) → ( ideal I ∋ p ) ∨ ( ideal I ∋ q )
 
 
-record GenericFilter (L : HOD) : Set (suc n) where
+record GenericFilter {L P : HOD} (LP : L ⊆ Power P) : Set (suc n) where
     field
-       genf : Filter L
-       generic : (D : Dense L ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
+       genf : Filter LP
+       generic : (D : Dense LP ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )