# HG changeset patch # User Shinji KONO # Date 1592182398 -32400 # Node ID 822b50091a2665078fe320ae7299a5fd50c976a9 # Parent 4340ffcfa83d2e77957090e082c011f73c6c332f fix prime diff -r 4340ffcfa83d -r 822b50091a26 filter.agda --- a/filter.agda Sun Jun 14 19:11:38 2020 +0900 +++ b/filter.agda Mon Jun 15 09:53:18 2020 +0900 @@ -28,7 +28,7 @@ open _∨_ open Bool --- Kunen p.76 and p.53 +-- Kunen p.76 and p.53, we use ⊆ record Filter ( L : OD ) : Set (suc n) where field filter : OD @@ -38,12 +38,15 @@ open Filter --- should use inhabit? -proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n -proper-filter {L} P {p} = ¬ (filter P ∋ od∅) +record prime-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where + field + proper : ¬ (filter P ∋ od∅) + prime : {p q : OD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) -prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n -prime-filter {L} P {p} {q} = filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) +record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where + field + proper : ¬ (filter P ∋ od∅) + ultra : {p : OD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) ) open _⊆_ @@ -67,20 +70,20 @@ q∩q⊆q : {p q : OD } → (q ∩ p) ⊆ q q∩q⊆q = record { incl = λ lt → proj1 lt } --- is-∅ : ( x : OD ) → Dec ( x ≡ od∅ ) --- is-∅ x with is-o∅ (od→ord x) --- ... | yes eq = yes {!!} --- ... | no ne = no {!!} +----- +-- +-- ultra filter is prime +-- -record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where - field - proper : ¬ (filter P ∋ od∅) - ultra : {p : OD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) ) - -filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ultra-filter P → prime-filter {L} P {p} {q} -filter-lemma1 {L} P {p} {q} u lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) -... | case1 p∈P = case1 p∈P -... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where +filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ultra-filter P → prime-filter P +filter-lemma1 {L} P u = record { + proper = ultra-filter.proper u + ; prime = lemma3 + } where + lemma3 : {p q : OD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) + lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) + ... | case1 p∈P = case1 p∈P + ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where lemma5 : ((p ∪ q ) ∩ (L ＼ p)) == (q ∩ (L ＼ p)) lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt } ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt } @@ -96,8 +99,13 @@ lemma8 : (q ∩ (L ＼ p)) ⊆ q lemma8 = q∩q⊆q -filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter P -filter-lemma2 {L} P prime p = {!!} +----- +-- +-- if Filter contains L, prime filter is ultra +-- + +filter-lemma2 : {L : OD} → (P : Filter L) → prime-filter P → ultra-filter P +filter-lemma2 {L} P prime = {!!} generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) generated-filter {L} P p = {!!}