Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate generic-filter.agda @ 424:cc7909f86841
remvoe TransFinifte1
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 01 Aug 2020 23:37:10 +0900 |
parents | 44a484f17f26 |
children | 9b0630f03c4b |
rev | line source |
---|---|
190 | 1 open import Level |
236 | 2 open import Ordinals |
387 | 3 module generic-filter {n : Level } (O : Ordinals {n}) where |
236 | 4 |
387 | 5 import filter |
190 | 6 open import zf |
236 | 7 open import logic |
387 | 8 open import partfunc {n} O |
236 | 9 import OD |
193 | 10 |
363 | 11 open import Relation.Nullary |
12 open import Relation.Binary | |
13 open import Data.Empty | |
190 | 14 open import Relation.Binary |
15 open import Relation.Binary.Core | |
363 | 16 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
|
17 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
363 | 18 import BAlgbra |
293 | 19 |
20 open BAlgbra O | |
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
21 |
236 | 22 open inOrdinal O |
23 open OD O | |
24 open OD.OD | |
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
25 open ODAxiom odAxiom |
424 | 26 import OrdUtil |
27 import ODUtil | |
28 open Ordinals.Ordinals O | |
29 open Ordinals.IsOrdinals isOrdinal | |
30 open Ordinals.IsNext isNext | |
31 open OrdUtil O | |
32 open ODUtil O | |
33 | |
190 | 34 |
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
35 import ODC |
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
36 |
387 | 37 open filter O |
38 | |
236 | 39 open _∧_ |
40 open _∨_ | |
41 open Bool | |
42 | |
265 | 43 |
331 | 44 open HOD |
45 | |
379 | 46 ------- |
47 -- the set of finite partial functions from ω to 2 | |
48 -- | |
49 -- | |
50 | |
392 | 51 open import Data.List hiding (filter) |
387 | 52 open import Data.Maybe |
379 | 53 |
54 import OPair | |
55 open OPair O | |
56 | |
57 open PFunc | |
58 | |
387 | 59 _f∩_ : (f g : PFunc (Lift n Nat) (Lift n Two) ) → PFunc (Lift n Nat) (Lift n Two) |
60 f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → pmap f x fr ≡ pmap g x gr) | |
61 ; pmap = λ x p → pmap f x (proj1 p) ; meq = meq f } | |
381 | 62 |
387 | 63 _↑_ : (Nat → Two) → Nat → PFunc (Lift n Nat) (Lift n Two) |
64 _↑_ f i = record { dom = λ x → Lift n (lower x ≤ i) ; pmap = λ x _ → lift (f (lower x)) ; meq = λ {x} {p} {q} → refl } | |
381 | 65 |
387 | 66 record _f⊆_ (f g : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where |
67 field | |
68 extend : {x : Nat} → (fr : dom f (lift x) ) → dom g (lift x ) | |
69 feq : {x : Nat} → {fr : dom f (lift x) } → pmap f (lift x) fr ≡ pmap g (lift x) (extend fr) | |
381 | 70 |
387 | 71 open _f⊆_ |
72 open import Data.Nat.Properties | |
375
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
73 |
363 | 74 ODSuc : (y : HOD) → infinite ∋ y → HOD |
75 ODSuc y lt = Union (y , (y , y)) | |
76 | |
366 | 77 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where |
78 hφ : Hω2 0 o∅ | |
79 h0 : {i : Nat} {x : Ordinal } → Hω2 i x → | |
422 | 80 Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 0 >) , * x ))) |
366 | 81 h1 : {i : Nat} {x : Ordinal } → Hω2 i x → |
422 | 82 Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 1 >) , * x ))) |
366 | 83 he : {i : Nat} {x : Ordinal } → Hω2 i x → |
84 Hω2 (Suc i) x | |
85 | |
86 record Hω2r (x : Ordinal) : Set n where | |
87 field | |
88 count : Nat | |
89 hω2 : Hω2 count x | |
90 | |
91 open Hω2r | |
363 | 92 |
93 HODω2 : HOD | |
366 | 94 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where |
393 | 95 P : (i j : Nat) (x : Ordinal ) → HOD |
422 | 96 P i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , * x |
97 nat1 : (i : Nat) (x : Ordinal) → & (nat→ω i) o< next x | |
394 | 98 nat1 i x = next< nexto∅ ( <odmax infinite (ω∋nat→ω {i})) |
422 | 99 lemma1 : (i j : Nat) (x : Ordinal ) → osuc (& (P i j x)) o< next x |
394 | 100 lemma1 i j x = osuc<nx (pair-<xy (pair-<xy (pair-<xy (nat1 i x) (nat1 i x) ) (pair-<xy (nat1 i x) (nat1 j x) ) ) |
422 | 101 (subst (λ k → k o< next x) (sym &iso) x<nx )) |
102 lemma : (i j : Nat) (x : Ordinal ) → & (Union (P i j x)) o< next x | |
393 | 103 lemma i j x = next< (lemma1 i j x ) ho< |
366 | 104 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅ |
105 odmax0 {y} r with hω2 r | |
106 ... | hφ = x<nx | |
393 | 107 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 0 x) |
108 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 1 x) | |
366 | 109 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx |
363 | 110 |
387 | 111 3→Hω2 : List (Maybe Two) → HOD |
385 | 112 3→Hω2 t = list→hod t 0 where |
387 | 113 list→hod : List (Maybe Two) → Nat → HOD |
385 | 114 list→hod [] _ = od∅ |
387 | 115 list→hod (just i0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) |
116 list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) | |
117 list→hod (nothing ∷ t) i = list→hod t (Suc i ) | |
385 | 118 |
387 | 119 Hω2→3 : (x : HOD) → HODω2 ∋ x → List (Maybe Two) |
385 | 120 Hω2→3 x = lemma where |
387 | 121 lemma : { y : Ordinal } → Hω2r y → List (Maybe Two) |
385 | 122 lemma record { count = 0 ; hω2 = hφ } = [] |
387 | 123 lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 } |
124 lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 = hω3 } | |
125 lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 = hω3 } | |
385 | 126 |
370 | 127 ω→2 : HOD |
394 | 128 ω→2 = Power infinite |
368 | 129 |
385 | 130 ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two |
394 | 131 ω→2f x lt n with ODC.∋-p O x (nat→ω n) |
132 ω→2f x lt n | yes p = i1 | |
133 ω→2f x lt n | no ¬p = i0 | |
385 | 134 |
395 | 135 fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n |
422 | 136 fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (& x) ) → f (ω→nat x lt) ≡ i1 ) |
395 | 137 |
138 fω→2 : (Nat → Two) → HOD | |
139 fω→2 f = Select infinite (fω→2-sel f) | |
140 | |
141 open _==_ | |
142 | |
143 postulate f-extensionality : { n m : Level} → Relation.Binary.PropositionalEquality.Extensionality n m | |
144 | |
396 | 145 ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f |
146 ω2∋f f = power← infinite (fω→2 f) (λ {x} lt → proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt)) | |
147 | |
411 | 148 ω→2f≡i1 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω) ≡ i1 → X ∋ i |
149 ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω)) | |
150 ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p | |
151 | |
152 open _⊆_ | |
396 | 153 |
412 | 154 -- someday ... |
155 postulate | |
156 ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt ) =h= X | |
157 fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f | |
395 | 158 |
385 | 159 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD |
160 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) )) | |
161 | |
386 | 162 record CountableOrdinal : Set (suc (suc n)) where |
163 field | |
164 ctl→ : Nat → Ordinal | |
165 ctl← : Ordinal → Nat | |
166 ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x | |
167 ctl-iso← : { x : Nat } → ctl← (ctl→ x ) ≡ x | |
388 | 168 |
169 record CountableHOD : Set (suc (suc n)) where | |
170 field | |
390 | 171 mhod : HOD |
172 mtl→ : Nat → Ordinal | |
173 mtl→∈P : (i : Nat) → odef mhod (mtl→ i) | |
174 mtl← : (x : Ordinal) → odef mhod x → Nat | |
175 mtl-iso→ : { x : Ordinal } → (lt : odef mhod x ) → mtl→ (mtl← x lt ) ≡ x | |
176 mtl-iso← : { x : Nat } → mtl← (mtl→ x ) (mtl→∈P x) ≡ x | |
388 | 177 |
386 | 178 |
387 | 179 open CountableOrdinal |
388 | 180 open CountableHOD |
387 | 181 |
412 | 182 ---- |
183 -- a(n) ∈ M | |
184 -- ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q | |
185 -- | |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
186 PGHOD : (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD |
412 | 187 PGHOD i C P p = record { od = record { def = λ x → |
422 | 188 odef P x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) } |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
189 ; odmax = odmax P ; <odmax = λ {y} lt → <odmax P (proj1 lt) } |
388 | 190 |
412 | 191 --- |
192 -- p(n+1) = if PGHOD n qn otherwise p(n) | |
193 -- | |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
194 next-p : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (p : Ordinal) → Ordinal |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
195 next-p C P i p with ODC.decp O ( PGHOD i C P p =h= od∅ ) |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
196 next-p C P i p | yes y = p |
422 | 197 next-p C P i p | no not = & (ODC.minimal O (PGHOD i C P p ) not) |
387 | 198 |
412 | 199 --- |
200 -- ascendant search on p(n) | |
201 -- | |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
202 find-p : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
203 find-p C P Zero x = x |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
204 find-p C P (Suc i) x = find-p C P i ( next-p C P i x ) |
388 | 205 |
412 | 206 --- |
207 -- G = { r ∈ Power P | ∃ n → r ⊆ p(n) } | |
208 -- | |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
209 record PDN (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where |
388 | 210 field |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
211 gr : Nat |
422 | 212 pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y |
412 | 213 px∈ω : odef (Power P) x |
388 | 214 |
215 open PDN | |
386 | 216 |
412 | 217 --- |
413
b00d58b3dc57
generic filter on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
412
diff
changeset
|
218 -- G as a HOD |
412 | 219 -- |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
220 PDHOD : (C : CountableOrdinal) → (P : HOD ) → HOD |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
221 PDHOD C P = record { od = record { def = λ x → PDN C P x } |
412 | 222 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.px∈ω lt) } where |
388 | 223 |
412 | 224 open PDN |
225 | |
226 ---- | |
413
b00d58b3dc57
generic filter on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
412
diff
changeset
|
227 -- Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set ) |
412 | 228 -- |
413
b00d58b3dc57
generic filter on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
412
diff
changeset
|
229 -- p 0 ≡ ∅ |
422 | 230 -- p (suc n) = if ∃ q ∈ * ( ctl→ n ) ∧ p n ⊆ q → q (axiom of choice) |
413
b00d58b3dc57
generic filter on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
412
diff
changeset
|
231 --- else p n |
b00d58b3dc57
generic filter on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
412
diff
changeset
|
232 |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
233 P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
234 P-GenericFilter C P = record { |
412 | 235 genf = record { filter = PDHOD C P ; f⊆PL = f⊆PL ; filter1 = {!!} ; filter2 = {!!} } |
386 | 236 ; generic = λ D → {!!} |
412 | 237 } where |
413
b00d58b3dc57
generic filter on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
412
diff
changeset
|
238 P∅ : {P : HOD} → odef (Power P) o∅ |
b00d58b3dc57
generic filter on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
412
diff
changeset
|
239 P∅ {P} = subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅ o∅≡od∅) where |
422 | 240 lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅) |
413
b00d58b3dc57
generic filter on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
412
diff
changeset
|
241 lemma x eq = power← P od∅ (λ {x} lt → ⊥-elim (¬x<0 lt )) |
422 | 242 x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y |
243 x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt | |
244 find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal) → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y | |
245 find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) &iso | |
246 ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P) Px)) (x<y→∋ Py)) | |
413
b00d58b3dc57
generic filter on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
412
diff
changeset
|
247 find-p-⊆P C P (Suc i) x y Px Py = find-p-⊆P C P i (next-p C P i x) y {!!} {!!} |
412 | 248 f⊆PL : PDHOD C P ⊆ Power P |
249 f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x → | |
422 | 250 find-p-⊆P C P (gr lt) o∅ (& y) P∅ (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) } |
412 | 251 |
392 | 252 |
253 open GenericFilter | |
254 open Filter | |
255 | |
256 record Incompatible (P : HOD ) : Set (suc (suc n)) where | |
257 field | |
258 except : HOD → ( HOD ∧ HOD ) | |
412 | 259 incompatible : { p : HOD } → Power P ∋ p → Power P ∋ proj1 (except p ) → Power P ∋ proj2 (except p ) |
392 | 260 → ( p ⊆ proj1 (except p) ) ∧ ( p ⊆ proj2 (except p) ) |
412 | 261 → ∀ ( r : HOD ) → Power P ∋ r → ¬ (( proj1 (except p) ⊆ r ) ∧ ( proj2 (except p) ⊆ r )) |
392 | 262 |
412 | 263 lemma725 : (M : CountableHOD ) (C : CountableOrdinal) (P : HOD ) → mhod M ∋ Power P |
392 | 264 → Incompatible P → ¬ ( mhod M ∋ filter ( genf ( P-GenericFilter C P ))) |
265 lemma725 = {!!} | |
266 | |
267 lemma725-1 : Incompatible HODω2 | |
268 lemma725-1 = {!!} | |
269 | |
270 lemma726 : (C : CountableOrdinal) (P : HOD ) | |
271 → Union ( filter ( genf ( P-GenericFilter C HODω2 ))) =h= ω→2 | |
272 lemma726 = {!!} | |
273 | |
274 -- | |
275 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > } | |
276 -- | |
277 | |
278 | |
279 | |
280 |