Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate filter.agda @ 403:ce2ce3f62023
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 28 Jul 2020 10:51:08 +0900 |
| parents | 19687f3304c9 |
| children | 44a484f17f26 |
| rev | line source |
|---|---|
| 190 | 1 open import Level |
| 236 | 2 open import Ordinals |
| 3 module filter {n : Level } (O : Ordinals {n}) where | |
| 4 | |
| 190 | 5 open import zf |
| 236 | 6 open import logic |
| 7 import OD | |
| 193 | 8 |
| 363 | 9 open import Relation.Nullary |
| 10 open import Data.Empty | |
| 190 | 11 open import Relation.Binary.Core |
| 363 | 12 open import Relation.Binary.PropositionalEquality |
| 13 import BAlgbra | |
| 293 | 14 |
| 15 open BAlgbra O | |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
16 |
| 236 | 17 open inOrdinal O |
| 18 open OD O | |
| 19 open OD.OD | |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
20 open ODAxiom odAxiom |
| 190 | 21 |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
22 import ODC |
| 388 | 23 open ODC O |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
24 |
| 236 | 25 open _∧_ |
| 26 open _∨_ | |
| 27 open Bool | |
| 28 | |
| 295 | 29 -- Kunen p.76 and p.53, we use ⊆ |
| 329 | 30 record Filter ( L : HOD ) : Set (suc n) where |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
31 field |
| 329 | 32 filter : HOD |
| 290 | 33 f⊆PL : filter ⊆ Power L |
| 329 | 34 filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q |
| 35 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) | |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
36 |
| 292 | 37 open Filter |
| 38 | |
| 329 | 39 record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where |
| 295 | 40 field |
| 41 proper : ¬ (filter P ∋ od∅) | |
| 329 | 42 prime : {p q : HOD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) |
| 292 | 43 |
| 329 | 44 record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where |
| 295 | 45 field |
| 46 proper : ¬ (filter P ∋ od∅) | |
| 329 | 47 ultra : {p : HOD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) ) |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
48 |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
49 open _⊆_ |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
50 |
| 329 | 51 ∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
52 ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt ) |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
53 |
| 329 | 54 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
55 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) } |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
56 |
| 329 | 57 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
58 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) } |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
59 |
| 329 | 60 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
61 q∩q⊆q = record { incl = λ lt → proj1 lt } |
| 265 | 62 |
| 331 | 63 open HOD |
| 64 | |
| 295 | 65 ----- |
| 66 -- | |
| 67 -- ultra filter is prime | |
| 68 -- | |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
69 |
| 329 | 70 filter-lemma1 : {L : HOD} → (P : Filter L) → ∀ {p q : HOD } → ultra-filter P → prime-filter P |
| 295 | 71 filter-lemma1 {L} P u = record { |
| 72 proper = ultra-filter.proper u | |
| 73 ; prime = lemma3 | |
| 74 } where | |
| 329 | 75 lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) |
| 295 | 76 lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) |
| 77 ... | case1 p∈P = case1 p∈P | |
| 78 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where | |
| 331 | 79 lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h= (q ∩ (L ＼ p)) |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
80 lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt } |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
81 ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt } |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
82 } where |
| 331 | 83 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
84 lemma4 x lt with proj1 lt |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
85 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
86 lemma4 x lt | case2 qx = qx |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
87 lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p)) |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
88 lemma6 = filter2 P lt ¬p∈P |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
89 lemma7 : filter P ∋ (q ∩ (L ＼ p)) |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
90 lemma7 = subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6 |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
91 lemma8 : (q ∩ (L ＼ p)) ⊆ q |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
92 lemma8 = q∩q⊆q |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
93 |
| 295 | 94 ----- |
| 95 -- | |
| 96 -- if Filter contains L, prime filter is ultra | |
| 97 -- | |
| 98 | |
| 329 | 99 filter-lemma2 : {L : HOD} → (P : Filter L) → filter P ∋ L → prime-filter P → ultra-filter P |
|
296
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
100 filter-lemma2 {L} P f∋L prime = record { |
|
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
101 proper = prime-filter.proper prime |
|
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
102 ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L) |
|
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
103 } where |
|
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
104 open _==_ |
| 331 | 105 p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) |
| 106 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x) | |
|
296
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
107 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x |
|
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
108 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p }) |
| 331 | 109 eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x )) |
|
296
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
110 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p |
| 329 | 111 lemma : (p : HOD) → p ⊆ L → filter P ∋ (p ∪ (L ＼ p)) |
|
296
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
112 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L |
| 293 | 113 |
| 329 | 114 record Dense (P : HOD ) : Set (suc n) where |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
115 field |
| 329 | 116 dense : HOD |
| 379 | 117 d⊆P : dense ⊆ Power P |
| 329 | 118 dense-f : HOD → HOD |
| 368 | 119 dense-d : { p : HOD} → p ⊆ P → dense ∋ dense-f p |
| 120 dense-p : { p : HOD} → p ⊆ P → p ⊆ (dense-f p) | |
| 266 | 121 |
| 329 | 122 record Ideal ( L : HOD ) : Set (suc n) where |
| 293 | 123 field |
| 329 | 124 ideal : HOD |
| 293 | 125 i⊆PL : ideal ⊆ Power L |
| 329 | 126 ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q |
| 127 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) | |
| 293 | 128 |
| 129 open Ideal | |
| 130 | |
| 329 | 131 proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n |
| 293 | 132 proper-ideal {L} P {p} = ideal P ∋ od∅ |
| 133 | |
| 329 | 134 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n |
| 293 | 135 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) |
| 136 | |
| 374 | 137 record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where |
| 370 | 138 field |
| 374 | 139 filter : L → Set n |
| 371 | 140 f⊆P : PL filter |
| 374 | 141 filter1 : { p q : L } → PL (λ x → q ⊆ x ) → filter p → p ⊆ q → filter q |
| 371 | 142 filter2 : { p q : L } → filter p → filter q → filter (p ∩ q) |
| 143 | |
| 374 | 144 Filter-is-F : {L : HOD} → (f : Filter L ) → F-Filter HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_ |
| 145 Filter-is-F {L} f = record { | |
| 146 filter = λ x → Lift (suc n) ((filter f) ∋ x) | |
| 147 ; f⊆P = λ x f∋x → power→⊆ _ _ (incl ( f⊆PL f ) (lower f∋x )) | |
| 148 ; filter1 = λ {p} {q} q⊆L f∋p p⊆q → lift ( filter1 f (q⊆L q refl-⊆) (lower f∋p) p⊆q) | |
| 149 ; filter2 = λ {p} {q} f∋p f∋q → lift ( filter2 f (lower f∋p) (lower f∋q)) | |
| 150 } | |
| 151 | |
| 379 | 152 record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where |
| 153 field | |
| 154 dense : L → Set n | |
| 155 d⊆P : PL dense | |
| 156 dense-f : L → L | |
| 157 dense-d : { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p ) | |
| 158 dense-p : { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p) | |
| 159 | |
| 160 Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_ | |
| 161 Dense-is-F {L} f = record { | |
| 162 dense = λ x → Lift (suc n) ((dense f) ∋ x) | |
| 163 ; d⊆P = λ x f∋x → power→⊆ _ _ (incl ( d⊆P f ) (lower f∋x )) | |
| 164 ; dense-f = λ x → dense-f f x | |
| 165 ; dense-d = λ {p} d → lift ( dense-d f (d p refl-⊆ ) ) | |
| 166 ; dense-p = λ {p} d → dense-p f (d p refl-⊆) | |
| 167 } where open Dense | |
| 168 | |
| 386 | 169 |
| 170 record GenericFilter (P : HOD) : Set (suc n) where | |
| 171 field | |
| 172 genf : Filter P | |
| 173 generic : (D : Dense P ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ ) | |
| 174 | |
| 175 record F-GenericFilter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where | |
| 176 field | |
| 177 GFilter : F-Filter L PL _⊆_ _∩_ | |
| 178 Intersection : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → F-Dense.dense D x → L | |
| 179 Generic : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → ( y : F-Dense.dense D x) → F-Filter.filter GFilter (Intersection D y ) | |
| 180 |