comparison filter.agda @ 295:822b50091a26

fix prime
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 15 Jun 2020 09:53:18 +0900
parents 4340ffcfa83d
children 42f89e5efb00
comparison
equal deleted inserted replaced
294:4340ffcfa83d 295:822b50091a26
26 26
27 open _∧_ 27 open _∧_
28 open _∨_ 28 open _∨_
29 open Bool 29 open Bool
30 30
31 -- Kunen p.76 and p.53 31 -- Kunen p.76 and p.53, we use ⊆
32 record Filter ( L : OD ) : Set (suc n) where 32 record Filter ( L : OD ) : Set (suc n) where
33 field 33 field
34 filter : OD 34 filter : OD
35 f⊆PL : filter ⊆ Power L 35 f⊆PL : filter ⊆ Power L
36 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q 36 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
37 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) 37 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
38 38
39 open Filter 39 open Filter
40 40
41 -- should use inhabit? 41 record prime-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
42 proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n 42 field
43 proper-filter {L} P {p} = ¬ (filter P ∋ od∅) 43 proper : ¬ (filter P ∋ od∅)
44 prime : {p q : OD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
44 45
45 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n 46 record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
46 prime-filter {L} P {p} {q} = filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) 47 field
48 proper : ¬ (filter P ∋ od∅)
49 ultra : {p : OD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L \ p) )
47 50
48 open _⊆_ 51 open _⊆_
49 52
50 trans-⊆ : { A B C : OD} → A ⊆ B → B ⊆ C → A ⊆ C 53 trans-⊆ : { A B C : OD} → A ⊆ B → B ⊆ C → A ⊆ C
51 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) } 54 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
65 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) } 68 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
66 69
67 q∩q⊆q : {p q : OD } → (q ∩ p) ⊆ q 70 q∩q⊆q : {p q : OD } → (q ∩ p) ⊆ q
68 q∩q⊆q = record { incl = λ lt → proj1 lt } 71 q∩q⊆q = record { incl = λ lt → proj1 lt }
69 72
70 -- is-∅ : ( x : OD ) → Dec ( x ≡ od∅ ) 73 -----
71 -- is-∅ x with is-o∅ (od→ord x) 74 --
72 -- ... | yes eq = yes {!!} 75 -- ultra filter is prime
73 -- ... | no ne = no {!!} 76 --
74 77
75 record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where 78 filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ultra-filter P → prime-filter P
76 field 79 filter-lemma1 {L} P u = record {
77 proper : ¬ (filter P ∋ od∅) 80 proper = ultra-filter.proper u
78 ultra : {p : OD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L \ p) ) 81 ; prime = lemma3
79 82 } where
80 filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ultra-filter P → prime-filter {L} P {p} {q} 83 lemma3 : {p q : OD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
81 filter-lemma1 {L} P {p} {q} u lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) 84 lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
82 ... | case1 p∈P = case1 p∈P 85 ... | case1 p∈P = case1 p∈P
83 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L \ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where 86 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L \ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
84 lemma5 : ((p ∪ q ) ∩ (L \ p)) == (q ∩ (L \ p)) 87 lemma5 : ((p ∪ q ) ∩ (L \ p)) == (q ∩ (L \ p))
85 lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt } 88 lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt }
86 ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt } 89 ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt }
87 } where 90 } where
88 lemma4 : (x : Ordinal ) → def ((p ∪ q) ∩ (L \ p)) x → def q x 91 lemma4 : (x : Ordinal ) → def ((p ∪ q) ∩ (L \ p)) x → def q x
94 lemma7 : filter P ∋ (q ∩ (L \ p)) 97 lemma7 : filter P ∋ (q ∩ (L \ p))
95 lemma7 = subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6 98 lemma7 = subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
96 lemma8 : (q ∩ (L \ p)) ⊆ q 99 lemma8 : (q ∩ (L \ p)) ⊆ q
97 lemma8 = q∩q⊆q 100 lemma8 = q∩q⊆q
98 101
99 filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter P 102 -----
100 filter-lemma2 {L} P prime p = {!!} 103 --
104 -- if Filter contains L, prime filter is ultra
105 --
106
107 filter-lemma2 : {L : OD} → (P : Filter L) → prime-filter P → ultra-filter P
108 filter-lemma2 {L} P prime = {!!}
101 109
102 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) 110 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
103 generated-filter {L} P p = {!!} 111 generated-filter {L} P p = {!!}
104 112
105 record Dense (P : OD ) : Set (suc n) where 113 record Dense (P : OD ) : Set (suc n) where