Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/filter.agda @ 574:9084a26445a7
ZC data won't work
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 05 Jun 2022 12:49:48 +0900 |
parents | 286016848403 |
children | 55ab5de1ae02 |
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 | |
15 import BAlgbra | |
16 | |
17 open BAlgbra O | |
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 ⊆ | |
458 | 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 | |
458 | 50 record prime-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter 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 |
458 | 55 record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter 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 |
60 open _⊆_ | |
61 | |
458 | 62 ∈-filter : {L P p : HOD} → {LP : L ⊆ Power P} → (F : Filter LP ) → filter F ∋ p → L ∋ p |
63 ∈-filter {L} {p} {LP} F lt = incl ( f⊆L F) lt | |
64 | |
65 ⊆-filter : {L P p q : HOD } → {LP : L ⊆ Power P } → (F : Filter LP) → L ∋ q → q ⊆ P | |
66 ⊆-filter {L} {P} {p} {q} {LP} F lt = power→⊆ P q ( incl LP lt ) | |
431 | 67 |
68 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L | |
69 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) } | |
70 | |
71 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L | |
72 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) } | |
73 | |
74 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q | |
75 q∩q⊆q = record { incl = λ lt → proj1 lt } | |
76 | |
77 open HOD | |
78 | |
79 ----- | |
80 -- | |
81 -- ultra filter is prime | |
82 -- | |
83 | |
461 | 84 filter-lemma1 : {P L : HOD} → (LP : L ⊆ Power P) |
85 → ({p : HOD} → L ∋ p → L ∋ (P \ p)) | |
86 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) | |
87 → (F : Filter LP) → ultra-filter F → prime-filter F | |
88 filter-lemma1 {P} {L} LP NG IN F u = record { | |
431 | 89 proper = ultra-filter.proper u |
90 ; prime = lemma3 | |
91 } where | |
461 | 92 lemma3 : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q) → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) |
93 lemma3 {p} {q} Lp Lq _ lt with ultra-filter.ultra u Lp (NG Lp) | |
458 | 94 ... | case1 p∈P = case1 p∈P |
95 ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (P \ p)} Lq lemma7 lemma8) where | |
96 lemma5 : ((p ∪ q ) ∩ (P \ p)) =h= (q ∩ (P \ p)) | |
431 | 97 lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫ |
98 ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫ | |
99 } where | |
458 | 100 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (P \ p)) x → odef q x |
431 | 101 lemma4 x lt with proj1 lt |
102 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) | |
103 lemma4 x lt | case2 qx = qx | |
461 | 104 lemma9 : L ∋ ((p ∪ q ) ∩ (P \ p)) |
105 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
|
106 lemma6 : filter F ∋ ((p ∪ q ) ∩ (P \ p)) |
461 | 107 lemma6 = filter2 F lt ¬p∈P lemma9 |
458 | 108 lemma7 : filter F ∋ (q ∩ (P \ p)) |
109 lemma7 = subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) lemma6 | |
110 lemma8 : (q ∩ (P \ p)) ⊆ q | |
431 | 111 lemma8 = q∩q⊆q |
112 | |
113 ----- | |
114 -- | |
115 -- if Filter contains L, prime filter is ultra | |
116 -- | |
117 | |
461 | 118 filter-lemma2 : {P L : HOD} → (LP : L ⊆ Power P) |
119 → ({p : HOD} → L ∋ p → L ∋ ( P \ p)) | |
120 → (F : Filter LP) → filter F ∋ P → prime-filter F → ultra-filter F | |
459 | 121 filter-lemma2 {P} {L} LP Lm F f∋P prime = record { |
458 | 122 proper = prime-filter.proper prime |
461 | 123 ; ultra = λ {p} L∋p _ → prime-filter.prime prime L∋p (Lm L∋p) (lemma10 L∋p (incl (f⊆L F) f∋P) ) (lemma p (p⊆L L∋p )) |
431 | 124 } where |
125 open _==_ | |
459 | 126 p⊆L : {p : HOD} → L ∋ p → p ⊆ P |
127 p⊆L {p} lt = power→⊆ P p ( incl LP lt ) | |
128 p+1-p=1 : {p : HOD} → p ⊆ P → P =h= (p ∪ (P \ p)) | |
129 eq→ (p+1-p=1 {p} p⊆P) {x} lt with ODC.decp O (odef p x) | |
130 eq→ (p+1-p=1 {p} p⊆P) {x} lt | yes p∋x = case1 p∋x | |
131 eq→ (p+1-p=1 {p} p⊆P) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫ | |
132 eq← (p+1-p=1 {p} p⊆P) {x} ( case1 p∋x ) = subst (λ k → odef P k ) &iso (incl p⊆P ( subst (λ k → odef p k) (sym &iso) p∋x )) | |
133 eq← (p+1-p=1 {p} p⊆P) {x} ( case2 ¬p ) = proj1 ¬p | |
458 | 134 lemma : (p : HOD) → p ⊆ P → filter F ∋ (p ∪ (P \ p)) |
459 | 135 lemma p p⊆P = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P |
461 | 136 lemma10 : {p : HOD} → L ∋ p → L ∋ P → L ∋ (p ∪ (P \ p)) |
137 lemma10 {p} L∋p lt = subst (λ k → L ∋ k ) (==→o≡ (p+1-p=1 {p} (p⊆L L∋p))) lt | |
431 | 138 |
458 | 139 ----- |
140 -- | |
141 -- if there is a filter , there is a ultra filter under the axiom of choise | |
461 | 142 -- Zorn Lemma |
458 | 143 |
459 | 144 -- filter→ultra : {P L : HOD} → (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P \ p)) → (F : Filter LP) → ultra-filter F |
145 -- filter→ultra {P} {L} LP Lm F = {!!} | |
458 | 146 |
147 record Dense {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where | |
431 | 148 field |
149 dense : HOD | |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
150 d⊆P : dense ⊆ L |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
151 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
|
152 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
|
153 dense-p : { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p |
431 | 154 |
458 | 155 record Ideal {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where |
431 | 156 field |
157 ideal : HOD | |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
158 i⊆L : ideal ⊆ L |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
159 ideal1 : { p q : HOD } → L ∋ q → ideal ∋ p → q ⊆ p → ideal ∋ q |
431 | 160 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) |
161 | |
162 open Ideal | |
163 | |
458 | 164 proper-ideal : {L P : HOD} → (LP : L ⊆ Power P) → (P : Ideal LP ) → {p : HOD} → Set n |
165 proper-ideal {L} {P} LP I = ideal I ∋ od∅ | |
431 | 166 |
458 | 167 prime-ideal : {L P : HOD} → (LP : L ⊆ Power P) → Ideal LP → ∀ {p q : HOD } → Set n |
168 prime-ideal {L} {P} LP I {p} {q} = ideal I ∋ ( p ∩ q) → ( ideal I ∋ p ) ∨ ( ideal I ∋ q ) | |
431 | 169 |
170 | |
461 | 171 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
|
172 field |
458 | 173 genf : Filter LP |
461 | 174 generic : (D : Dense LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ ) |
431 | 175 |
478 | 176 record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) : Set (suc n) where |
177 field | |
178 mf : Filter LP | |
179 proper : ¬ (filter mf ∋ od∅) | |
481 | 180 is-maximum : ( f : Filter LP ) → ¬ (filter f ∋ od∅) → ¬ filter mf ≡ filter f → ¬ ( filter mf ⊆ filter f ) |
478 | 181 |
182 max→ultra : {L P : HOD} (LP : L ⊆ Power P) → (mx : MaximumFilter LP ) → ultra-filter ( MaximumFilter.mf mx ) | |
479 | 183 max→ultra {L} {P} LP mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where |
184 mf = MaximumFilter.mf mx | |
185 ultra : {p : HOD} → L ∋ p → L ∋ (P \ p) → (filter mf ∋ p) ∨ (filter mf ∋ (P \ p)) | |
186 ultra {p} lp lnp with ∋-p (filter mf) p | |
187 ... | yes y = case1 y | |
188 ... | no np with ∋-p (filter mf) (P \ p) | |
189 ... | yes y = case2 y | |
481 | 190 ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter FisProper {!!} record { incl = FisGreater } ) where |
479 | 191 Y : (y : Ordinal) → (my : odef (filter mf) y ) → HOD |
192 Y y my = record { od = record { def = λ x → (x ≡ y) ∨ (x ≡ & p) } ; odmax = & L ; <odmax = {!!} } | |
193 F : HOD | |
194 F = record { od = record { def = λ x → (x ≡ & p) ∨ ((y : Ordinal) → (my : odef (filter mf) y ) → x ≡ & (Y y my) ) } ; odmax = & L ; <odmax = {!!} } | |
195 FisFilter : Filter LP | |
196 FisFilter = record { filter = F ; f⊆L = {!!} ; filter1 = {!!} ; filter2 = {!!} } | |
480 | 197 FisGreater : {x : HOD} → filter (MaximumFilter.mf mx) ∋ x → filter FisFilter ∋ x |
198 FisGreater = {!!} | |
199 FisProper : ¬ (filter FisFilter ∋ od∅) | |
200 FisProper = {!!} | |
478 | 201 |
480 | 202 open _==_ |
203 | |
204 open import Relation.Binary.Definitions | |
205 | |
206 ultra→max : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P \ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) | |
481 | 207 → (U : Filter LP) → ultra-filter U → MaximumFilter LP |
208 ultra→max {L} {P} LP NG CAP U u = record { mf = U ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where | |
209 is-maximum : (F : Filter LP) → (¬ (filter F ∋ od∅)) → ( U≠F : ¬ filter U ≡ filter F ) → (U⊆F : filter U ⊆ filter F ) → ⊥ | |
210 is-maximum F Prop U≠F U⊆F = Prop f0 where | |
480 | 211 GT : HOD |
212 GT = record { od = record { def = λ x → odef (filter F) x ∧ (¬ odef (filter U) x) } ; odmax = {!!} ; <odmax = {!!} } | |
213 GT≠∅ : ¬ (GT =h= od∅) | |
214 GT≠∅ eq = ⊥-elim (U≠F ( ==→o≡ (⊆→= U⊆F (U-F=∅→F⊆U gt01)))) where | |
215 gt01 : (x : Ordinal) → ¬ odef (filter F) x ∧ (¬ odef (filter U) x) | |
216 gt01 x not = ¬x<0 ( eq→ eq not ) | |
217 p : HOD | |
218 p = ODC.minimal O GT GT≠∅ | |
219 ¬U∋p : ¬ ( filter U ∋ p ) | |
220 ¬U∋p = proj2 (ODC.x∋minimal O GT GT≠∅) | |
221 U∋-p : filter U ∋ ( P \ p ) | |
222 U∋-p with ultra-filter.ultra u {p} {!!} {!!} | |
223 ... | case1 ux = ⊥-elim ( ¬U∋p ux ) | |
224 ... | case2 u-x = u-x | |
225 F∋p : filter F ∋ p | |
226 F∋p = proj1 (ODC.x∋minimal O GT GT≠∅) | |
227 F∋-p : filter F ∋ ( P \ p ) | |
228 F∋-p = incl U⊆F U∋-p | |
229 f0 : filter F ∋ od∅ | |
230 f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP {!!} {!!}) ) | |
516 | 231 |
232 _⊆'_ : ( A B : HOD ) → Set n | |
574 | 233 _⊆'_ A B = {x : Ordinal } → odef A x → odef B x |
516 | 234 |
235 import zorn | |
574 | 236 open zorn O _⊆'_ hiding ( _⊆'_ ) |
237 | |
238 open import Relation.Binary.Structures | |
481 | 239 |
516 | 240 MaximumSubset : {L P : HOD} |
574 | 241 → o∅ o< & L → o∅ o< & P → P ⊆' L |
242 → (PO : IsStrictPartialOrder _≡_ _⊆'_ ) | |
243 → ( (B : HOD) → B ⊆ P → IsTotalOrderSet PO B → SUP PO P B ) | |
244 → Maximal PO P | |
245 MaximumSubset {L} {P} 0<L 0<P P⊆L PO C = Zorn-lemma PO 0<P {!!} | |
503 | 246 |
516 | 247 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)) |
248 → (F : Filter LP) → o∅ o< & L → o∅ o< & (filter F) → (¬ (filter F ∋ od∅)) → MaximumFilter LP | |
249 MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = {!!} ; proper = {!!} ; is-maximum = {!!} } where | |
574 | 250 mf01 : Maximal {!!} {!!} |
251 mf01 = MaximumSubset 0<L {!!} {!!} {!!} {!!} | |
481 | 252 |
253 |