Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate filter.agda @ 364:67580311cc8e
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 18 Jul 2020 11:38:33 +0900 |
| parents | aad9249d1e8f |
| children | 7f919d6b045b |
| 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 Relation.Binary | |
| 11 open import Data.Empty | |
| 190 | 12 open import Relation.Binary |
| 13 open import Relation.Binary.Core | |
| 363 | 14 open import Relation.Binary.PropositionalEquality |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
| 363 | 16 import BAlgbra |
| 293 | 17 |
| 18 open BAlgbra O | |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
19 |
| 236 | 20 open inOrdinal O |
| 21 open OD O | |
| 22 open OD.OD | |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
23 open ODAxiom odAxiom |
| 190 | 24 |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
25 import ODC |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
26 |
| 236 | 27 open _∧_ |
| 28 open _∨_ | |
| 29 open Bool | |
| 30 | |
| 295 | 31 -- Kunen p.76 and p.53, we use ⊆ |
| 329 | 32 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
|
33 field |
| 329 | 34 filter : HOD |
| 290 | 35 f⊆PL : filter ⊆ Power L |
| 329 | 36 filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q |
| 37 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
|
38 |
| 292 | 39 open Filter |
| 40 | |
| 329 | 41 record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where |
| 295 | 42 field |
| 43 proper : ¬ (filter P ∋ od∅) | |
| 329 | 44 prime : {p q : HOD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) |
| 292 | 45 |
| 329 | 46 record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where |
| 295 | 47 field |
| 48 proper : ¬ (filter P ∋ od∅) | |
| 329 | 49 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
|
50 |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
51 open _⊆_ |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
52 |
| 329 | 53 trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
54 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) } |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
55 |
| 329 | 56 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A |
| 331 | 57 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where |
| 329 | 58 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
59 t1 = zf.IsZF.power→ isZF A t PA∋t |
| 292 | 60 |
| 329 | 61 ∈-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
|
62 ∈-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
|
63 |
| 329 | 64 ∪-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
|
65 ∪-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
|
66 |
| 329 | 67 ∪-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
|
68 ∪-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
|
69 |
| 329 | 70 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
|
71 q∩q⊆q = record { incl = λ lt → proj1 lt } |
| 265 | 72 |
| 331 | 73 open HOD |
| 74 _=h=_ : (x y : HOD) → Set n | |
| 75 x =h= y = od x == od y | |
| 76 | |
| 295 | 77 ----- |
| 78 -- | |
| 79 -- ultra filter is prime | |
| 80 -- | |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
81 |
| 329 | 82 filter-lemma1 : {L : HOD} → (P : Filter L) → ∀ {p q : HOD } → ultra-filter P → prime-filter P |
| 295 | 83 filter-lemma1 {L} P u = record { |
| 84 proper = ultra-filter.proper u | |
| 85 ; prime = lemma3 | |
| 86 } where | |
| 329 | 87 lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) |
| 295 | 88 lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) |
| 89 ... | case1 p∈P = case1 p∈P | |
| 90 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where | |
| 331 | 91 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
|
92 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
|
93 ; 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
|
94 } where |
| 331 | 95 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
|
96 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
|
97 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
|
98 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
|
99 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
|
100 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
|
101 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
|
102 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
|
103 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
|
104 lemma8 = q∩q⊆q |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
105 |
| 295 | 106 ----- |
| 107 -- | |
| 108 -- if Filter contains L, prime filter is ultra | |
| 109 -- | |
| 110 | |
| 329 | 111 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
|
112 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
|
113 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
|
114 ; 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
|
115 } where |
|
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
116 open _==_ |
| 331 | 117 p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) |
| 118 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
|
119 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
|
120 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p }) |
| 331 | 121 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
|
122 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p |
| 329 | 123 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
|
124 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L |
| 293 | 125 |
| 329 | 126 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
|
127 field |
| 329 | 128 dense : HOD |
| 271 | 129 incl : dense ⊆ P |
| 329 | 130 dense-f : HOD → HOD |
| 131 dense-d : { p : HOD} → P ∋ p → dense ∋ dense-f p | |
| 132 dense-p : { p : HOD} → P ∋ p → p ⊆ (dense-f p) | |
| 266 | 133 |
| 329 | 134 record Ideal ( L : HOD ) : Set (suc n) where |
| 293 | 135 field |
| 329 | 136 ideal : HOD |
| 293 | 137 i⊆PL : ideal ⊆ Power L |
| 329 | 138 ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q |
| 139 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) | |
| 293 | 140 |
| 141 open Ideal | |
| 142 | |
| 329 | 143 proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n |
| 293 | 144 proper-ideal {L} P {p} = ideal P ∋ od∅ |
| 145 | |
| 329 | 146 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n |
| 293 | 147 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) |
| 148 | |
| 364 | 149 ------- |
| 363 | 150 -- the set of finite partial functions from ω to 2 |
| 151 -- | |
| 152 -- | |
| 153 | |
| 154 import OPair | |
| 155 open OPair O | |
| 156 | |
| 157 ODSuc : (y : HOD) → infinite ∋ y → HOD | |
| 158 ODSuc y lt = Union (y , (y , y)) | |
| 159 | |
| 160 nat→ω : Nat → HOD | |
| 161 nat→ω Zero = od∅ | |
| 162 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) | |
| 163 | |
| 364 | 164 postulate -- we have proved in other module |
| 165 ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n)) | |
| 166 ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅ | |
| 167 | |
| 168 postulate | |
| 169 ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) | |
| 170 | |
| 363 | 171 data Hω2 : ( x : Ordinal ) → Set n where |
| 172 hφ : Hω2 o∅ | |
| 173 h0 : {x : Ordinal } → Hω2 x → | |
| 174 Hω2 (od→ord < nat→ω 0 , ord→od x >) | |
| 175 h1 : {x : Ordinal } → Hω2 x → | |
| 176 Hω2 (od→ord < nat→ω 1 , ord→od x >) | |
| 177 h2 : {x : Ordinal } → Hω2 x → | |
| 178 Hω2 (od→ord < nat→ω 2 , ord→od x >) | |
| 179 | |
| 180 HODω2 : HOD | |
| 364 | 181 HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where |
| 182 lemma0 : {n y : Ordinal} → Hω2 y → odef infinite n → od→ord < ord→od n , ord→od y > o< next y | |
| 183 lemma0 {n} {y} hw2 inf = nexto=n {!!} | |
| 184 odmax0 : {y : Ordinal} → Hω2 y → y o< next o∅ | |
| 185 odmax0 {o∅} hφ = x<nx | |
| 186 odmax0 (h0 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {0} ))) | |
| 187 odmax0 (h1 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {1} ))) | |
| 188 odmax0 (h2 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {2} ))) | |
| 363 | 189 |
| 190 -- the set of finite partial functions from ω to 2 | |
| 191 | |
| 192 data Two : Set n where | |
| 193 i0 : Two | |
| 194 i1 : Two | |
| 195 | |
| 196 Hω2f : Set (suc n) | |
| 197 Hω2f = (Nat → Set n) → Two | |
| 198 | |
| 199 Hω2f→Hω2 : Hω2f → HOD | |
| 200 Hω2f→Hω2 p = record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} } | |
| 201 | |
| 202 |