Mercurial > hg > Members > kono > Proof > ZF-in-agda
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 |