Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/filter.agda @ 1129:5053fd12134a
use different filter
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 10 Jan 2023 18:12:05 +0900 |
parents | 7d4966f2f74d |
children | 4a4ac5141b95 |
rev | line source |
---|---|
457 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
2 | |
431 | 3 open import Level |
4 open import Ordinals | |
5 module filter {n : Level } (O : Ordinals {n}) where | |
6 | |
7 open import zf | |
8 open import logic | |
9 import OD | |
10 | |
11 open import Relation.Nullary | |
12 open import Data.Empty | |
13 open import Relation.Binary.Core | |
14 open import Relation.Binary.PropositionalEquality | |
1124 | 15 import BAlgebra |
431 | 16 |
1124 | 17 open BAlgebra O |
431 | 18 |
19 open inOrdinal O | |
20 open OD O | |
21 open OD.OD | |
22 open ODAxiom odAxiom | |
23 | |
24 import OrdUtil | |
25 import ODUtil | |
26 open Ordinals.Ordinals O | |
27 open Ordinals.IsOrdinals isOrdinal | |
28 open Ordinals.IsNext isNext | |
29 open OrdUtil O | |
30 open ODUtil O | |
31 | |
32 | |
33 import ODC | |
34 open ODC O | |
35 | |
36 open _∧_ | |
37 open _∨_ | |
38 open Bool | |
39 | |
40 -- Kunen p.76 and p.53, we use ⊆ | |
1124 | 41 record Filter { L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where |
431 | 42 field |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
43 filter : HOD |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
44 f⊆L : filter ⊆ L |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
45 filter1 : { p q : HOD } → L ∋ q → filter ∋ p → p ⊆ q → filter ∋ q |
461 | 46 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → L ∋ (p ∩ q) → filter ∋ (p ∩ q) |
431 | 47 |
48 open Filter | |
49 | |
1124 | 50 record prime-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter {L} {P} LP) : Set (suc (suc n)) where |
431 | 51 field |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
52 proper : ¬ (filter F ∋ od∅) |
461 | 53 prime : {p q : HOD } → L ∋ p → L ∋ q → L ∋ (p ∪ q) → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) |
431 | 54 |
1124 | 55 record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter {L} {P} LP) : Set (suc (suc n)) where |
431 | 56 field |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
57 proper : ¬ (filter F ∋ od∅) |
461 | 58 ultra : {p : HOD } → L ∋ p → L ∋ ( P \ p) → ( filter F ∋ p ) ∨ ( filter F ∋ ( P \ p) ) |
431 | 59 |
1124 | 60 ∈-filter : {L P p : HOD} → {LP : L ⊆ Power P} → (F : Filter {L} {P} LP ) → filter F ∋ p → L ∋ p |
1096 | 61 ∈-filter {L} {p} {LP} F lt = ( f⊆L F) lt |
458 | 62 |
1124 | 63 ⊆-filter : {L P p q : HOD } → {LP : L ⊆ Power P } → (F : Filter {L} {P} LP) → L ∋ q → q ⊆ P |
1096 | 64 ⊆-filter {L} {P} {p} {q} {LP} F lt = power→⊆ P q ( LP lt ) |
431 | 65 |
66 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L | |
1096 | 67 ∪-lemma1 {L} {p} {q} lt p∋x = lt (case1 p∋x) |
431 | 68 |
69 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L | |
1096 | 70 ∪-lemma2 {L} {p} {q} lt p∋x = lt (case2 p∋x) |
431 | 71 |
72 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q | |
1096 | 73 q∩q⊆q lt = proj1 lt |
431 | 74 |
75 open HOD | |
76 | |
77 ----- | |
78 -- | |
79 -- ultra filter is prime | |
80 -- | |
81 | |
461 | 82 filter-lemma1 : {P L : HOD} → (LP : L ⊆ Power P) |
83 → ({p : HOD} → L ∋ p → L ∋ (P \ p)) | |
84 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) | |
1124 | 85 → (F : Filter {L} {P} LP) → ultra-filter F → prime-filter F |
461 | 86 filter-lemma1 {P} {L} LP NG IN F u = record { |
431 | 87 proper = ultra-filter.proper u |
88 ; prime = lemma3 | |
89 } where | |
461 | 90 lemma3 : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q) → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) |
91 lemma3 {p} {q} Lp Lq _ lt with ultra-filter.ultra u Lp (NG Lp) | |
458 | 92 ... | case1 p∈P = case1 p∈P |
93 ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (P \ p)} Lq lemma7 lemma8) where | |
94 lemma5 : ((p ∪ q ) ∩ (P \ p)) =h= (q ∩ (P \ p)) | |
431 | 95 lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫ |
96 ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫ | |
97 } where | |
458 | 98 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (P \ p)) x → odef q x |
431 | 99 lemma4 x lt with proj1 lt |
100 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) | |
101 lemma4 x lt | case2 qx = qx | |
461 | 102 lemma9 : L ∋ ((p ∪ q ) ∩ (P \ p)) |
103 lemma9 = subst (λ k → L ∋ k ) (sym (==→o≡ lemma5)) (IN Lq (NG Lp)) | |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
104 lemma6 : filter F ∋ ((p ∪ q ) ∩ (P \ p)) |
461 | 105 lemma6 = filter2 F lt ¬p∈P lemma9 |
458 | 106 lemma7 : filter F ∋ (q ∩ (P \ p)) |
107 lemma7 = subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) lemma6 | |
108 lemma8 : (q ∩ (P \ p)) ⊆ q | |
1124 | 109 lemma8 lt = proj1 lt |
431 | 110 |
111 ----- | |
112 -- | |
1124 | 113 -- if Filter {L} {P} contains L, prime filter is ultra |
431 | 114 -- |
115 | |
461 | 116 filter-lemma2 : {P L : HOD} → (LP : L ⊆ Power P) |
117 → ({p : HOD} → L ∋ p → L ∋ ( P \ p)) | |
1124 | 118 → (F : Filter {L} {P} LP) → filter F ∋ P → prime-filter F → ultra-filter F |
459 | 119 filter-lemma2 {P} {L} LP Lm F f∋P prime = record { |
458 | 120 proper = prime-filter.proper prime |
1096 | 121 ; ultra = λ {p} L∋p _ → prime-filter.prime prime L∋p (Lm L∋p) (lemma10 L∋p ((f⊆L F) f∋P) ) (lemma p (p⊆L L∋p )) |
431 | 122 } where |
123 open _==_ | |
459 | 124 p⊆L : {p : HOD} → L ∋ p → p ⊆ P |
1096 | 125 p⊆L {p} lt = power→⊆ P p ( LP lt ) |
459 | 126 p+1-p=1 : {p : HOD} → p ⊆ P → P =h= (p ∪ (P \ p)) |
127 eq→ (p+1-p=1 {p} p⊆P) {x} lt with ODC.decp O (odef p x) | |
128 eq→ (p+1-p=1 {p} p⊆P) {x} lt | yes p∋x = case1 p∋x | |
129 eq→ (p+1-p=1 {p} p⊆P) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫ | |
1096 | 130 eq← (p+1-p=1 {p} p⊆P) {x} ( case1 p∋x ) = subst (λ k → odef P k ) &iso (p⊆P ( subst (λ k → odef p k) (sym &iso) p∋x )) |
459 | 131 eq← (p+1-p=1 {p} p⊆P) {x} ( case2 ¬p ) = proj1 ¬p |
458 | 132 lemma : (p : HOD) → p ⊆ P → filter F ∋ (p ∪ (P \ p)) |
459 | 133 lemma p p⊆P = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P |
461 | 134 lemma10 : {p : HOD} → L ∋ p → L ∋ P → L ∋ (p ∪ (P \ p)) |
135 lemma10 {p} L∋p lt = subst (λ k → L ∋ k ) (==→o≡ (p+1-p=1 {p} (p⊆L L∋p))) lt | |
431 | 136 |
458 | 137 ----- |
138 -- | |
139 -- if there is a filter , there is a ultra filter under the axiom of choise | |
461 | 140 -- Zorn Lemma |
458 | 141 |
1124 | 142 -- filter→ultra : {P L : HOD} → (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P \ p)) → (F : Filter {L} {P} LP) → ultra-filter F |
459 | 143 -- filter→ultra {P} {L} LP Lm F = {!!} |
458 | 144 |
145 record Dense {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where | |
431 | 146 field |
147 dense : HOD | |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
148 d⊆P : dense ⊆ L |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
149 dense-f : {p : HOD} → L ∋ p → HOD |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
150 dense-d : { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
151 dense-p : { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p |
431 | 152 |
458 | 153 record Ideal {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where |
431 | 154 field |
155 ideal : HOD | |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
156 i⊆L : ideal ⊆ L |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
157 ideal1 : { p q : HOD } → L ∋ q → ideal ∋ p → q ⊆ p → ideal ∋ q |
431 | 158 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) |
159 | |
160 open Ideal | |
161 | |
1124 | 162 proper-ideal : {L P : HOD} → (LP : L ⊆ Power P) → (P : Ideal {L} {P} LP ) → {p : HOD} → Set n |
458 | 163 proper-ideal {L} {P} LP I = ideal I ∋ od∅ |
431 | 164 |
1124 | 165 prime-ideal : {L P : HOD} → (LP : L ⊆ Power P) → Ideal {L} {P} LP → ∀ {p q : HOD } → Set n |
458 | 166 prime-ideal {L} {P} LP I {p} {q} = ideal I ∋ ( p ∩ q) → ( ideal I ∋ p ) ∨ ( ideal I ∋ q ) |
431 | 167 |
168 | |
461 | 169 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (suc n) where |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
170 field |
1124 | 171 genf : Filter {L} {P} LP |
172 generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ ) | |
431 | 173 |
478 | 174 record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) : Set (suc n) where |
175 field | |
1124 | 176 mf : Filter {L} {P} LP |
478 | 177 proper : ¬ (filter mf ∋ od∅) |
1124 | 178 is-maximum : ( f : Filter {L} {P} LP ) → ¬ (filter f ∋ od∅) → ¬ ( filter mf ⊂ filter f ) |
478 | 179 |
1125 | 180 record Fp {L P : HOD} (LP : L ⊆ Power P) (mx : MaximumFilter {L} {P} LP ) (p x : Ordinal ) : Set n where |
181 field | |
182 y : Ordinal | |
183 mfy : odef (filter (MaximumFilter.mf mx)) y | |
1129 | 184 y-p⊂x : ( * y \ * p ) ⊂ * x |
1125 | 185 |
186 max→ultra : {L P : HOD} (LP : L ⊆ Power P) | |
187 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p \ q)) | |
1127 | 188 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) |
1125 | 189 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q)) |
190 → (mx : MaximumFilter {L} {P} LP ) → ultra-filter ( MaximumFilter.mf mx ) | |
1127 | 191 max→ultra {L} {P} LP NEG CAP CUP mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where |
479 | 192 mf = MaximumFilter.mf mx |
193 ultra : {p : HOD} → L ∋ p → L ∋ (P \ p) → (filter mf ∋ p) ∨ (filter mf ∋ (P \ p)) | |
1129 | 194 ultra {p} Lp lnp with ODC.∋-p O (filter mf) p |
479 | 195 ... | yes y = case1 y |
1129 | 196 ... | no np = ? where |
197 F : HOD | |
198 F = record { od = record { def = λ x → odef L x ∧ Fp {L} {P} LP mx (& p) x } | |
199 ; odmax = & L ; <odmax = λ lt → odef< (proj1 lt) } | |
1124 | 200 mu01 : {r : HOD} {q : HOD} → L ∋ q → F ∋ r → r ⊆ q → F ∋ q |
1129 | 201 mu01 {r} {q} Lq ⟪ Lr , record { y = y ; mfy = mfy ; y-p⊂x = y-p⊂x } ⟫ r⊆q = ⟪ Lq , record { y = y ; mfy = mfy ; y-p⊂x = ? } ⟫ |
1125 | 202 mu02 : {r : HOD} {q : HOD} → F ∋ r → F ∋ q → L ∋ (r ∩ q) → F ∋ (r ∩ q) |
1129 | 203 mu02 {r} {q} ⟪ Lr , record { y = ry ; mfy = mfry ; y-p⊂x = ry-p⊂x } ⟫ |
204 ⟪ Lq , record { y = qy ; mfy = mfqy ; y-p⊂x = qy-p⊂x } ⟫ Lrq = ⟪ Lrq , record { y = & (* qy ∩ * ry) ; mfy = ? ; y-p⊂x = ? } ⟫ | |
1124 | 205 FisFilter : Filter {L} {P} LP |
1129 | 206 FisFilter = record { filter = F ; f⊆L = ? ; filter1 = mu01 ; filter2 = mu02 } |
1124 | 207 FisGreater : {x : Ordinal } → odef (filter (MaximumFilter.mf mx)) x → odef (filter FisFilter ) x |
1129 | 208 FisGreater {x} mfx = ⟪ f⊆L mf mfx , record { y = x ; mfy = mfx ; y-p⊂x = mu03 } ⟫ where |
209 mu03 : (* x \ * (& p)) ⊂ * x | |
210 mu03 = ⟪ ? , ? ⟫ | |
1124 | 211 F< : & (filter (MaximumFilter.mf mx)) o< & F |
212 F< = ? | |
480 | 213 FisProper : ¬ (filter FisFilter ∋ od∅) |
214 FisProper = {!!} | |
478 | 215 |
480 | 216 open _==_ |
217 | |
1124 | 218 -- open import Relation.Binary.Definitions |
480 | 219 |
1124 | 220 ultra→max : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} |
221 → L ∋ p → L ∋ ( P \ p)) | |
222 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) | |
223 → (U : Filter {L} {P} LP) → ultra-filter U → MaximumFilter LP | |
481 | 224 ultra→max {L} {P} LP NG CAP U u = record { mf = U ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where |
1124 | 225 is-maximum : (F : Filter {L} {P} LP) → (¬ (filter F ∋ od∅)) → (U⊂F : filter U ⊂ filter F ) → ⊥ |
226 is-maximum F Prop ⟪ U<F , U⊆F ⟫ = Prop f0 where | |
480 | 227 GT : HOD |
1124 | 228 GT = record { od = record { def = λ x → odef (filter F) x ∧ (¬ odef (filter U) x) } ; odmax = & L ; <odmax = um02 } where |
229 um02 : {y : Ordinal } → odef (filter F) y ∧ (¬ odef (filter U) y) → y o< & L | |
230 um02 {y} Fy = odef< ( f⊆L F (proj1 Fy ) ) | |
480 | 231 GT≠∅ : ¬ (GT =h= od∅) |
1124 | 232 GT≠∅ eq = ⊥-elim (U≠F ( ==→o≡ ((⊆→= {filter U} {filter F}) U⊆F (U-F=∅→F⊆U {filter F} {filter U} gt01)))) where |
233 U≠F : ¬ ( filter U ≡ filter F ) | |
234 U≠F eq = o<¬≡ (cong (&) eq) U<F | |
235 gt01 : (x : Ordinal) → ¬ ( odef (filter F) x ∧ (¬ odef (filter U) x)) | |
480 | 236 gt01 x not = ¬x<0 ( eq→ eq not ) |
237 p : HOD | |
238 p = ODC.minimal O GT GT≠∅ | |
239 ¬U∋p : ¬ ( filter U ∋ p ) | |
240 ¬U∋p = proj2 (ODC.x∋minimal O GT GT≠∅) | |
1124 | 241 L∋p : L ∋ p |
242 L∋p = f⊆L F ( proj1 (ODC.x∋minimal O GT GT≠∅)) | |
243 um00 : ¬ odef (filter U) (& p) | |
244 um00 = proj2 (ODC.x∋minimal O GT GT≠∅) | |
245 L∋-p : L ∋ ( P \ p ) | |
246 L∋-p = NG L∋p | |
480 | 247 U∋-p : filter U ∋ ( P \ p ) |
1124 | 248 U∋-p with ultra-filter.ultra u {p} L∋p L∋-p |
480 | 249 ... | case1 ux = ⊥-elim ( ¬U∋p ux ) |
250 ... | case2 u-x = u-x | |
251 F∋p : filter F ∋ p | |
252 F∋p = proj1 (ODC.x∋minimal O GT GT≠∅) | |
253 F∋-p : filter F ∋ ( P \ p ) | |
1096 | 254 F∋-p = U⊆F U∋-p |
480 | 255 f0 : filter F ∋ od∅ |
1124 | 256 f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP L∋p L∋-p) ) |
516 | 257 |
258 import zorn | |
1126 | 259 |
260 open import Relation.Binary | |
261 | |
262 PO : IsStrictPartialOrder _≡_ _⊂_ | |
263 PO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans } | |
264 ; trans = λ {a} {b} {c} → trans-⊂ {a} {b} {c} | |
265 ; irrefl = λ x=y x<y → ? | |
266 ; <-resp-≈ = record { fst = λ {x} {y} {y1} y=y1 xy1 → ? ; snd = λ {x} {x1} {y} x=x1 x1y → ? } } | |
267 | |
268 open zorn O _⊂_ PO | |
574 | 269 |
270 open import Relation.Binary.Structures | |
481 | 271 |
1126 | 272 SUP⊆ : (P B : HOD) → B ⊆ P → IsTotalOrderSet B → SUP P B |
273 SUP⊆ P B B⊆P OB = record { sup = Union B ; isSUP = record { ax = ? ; x≤sup = ? } } | |
274 | |
516 | 275 MaximumSubset : {L P : HOD} |
1096 | 276 → o∅ o< & L → o∅ o< & P → P ⊆ L |
1126 | 277 → Maximal P |
278 MaximumSubset {L} {P} 0<L 0<P P⊆L = Zorn-lemma 0<P (SUP⊆ P) | |
503 | 279 |
516 | 280 MaximumFilterExist : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P \ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) |
1124 | 281 → (F : Filter {L} {P} LP) → o∅ o< & L → o∅ o< & (filter F) → (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP |
516 | 282 MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = {!!} ; proper = {!!} ; is-maximum = {!!} } where |
1126 | 283 mf01 : Maximal {!!} |
284 mf01 = MaximumSubset 0<L {!!} {!!} | |
481 | 285 |
286 |