Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate generic-filter.agda @ 391:e98b5774d180
generic filter defined
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 25 Jul 2020 16:45:22 +0900 |
parents | d58edc4133b0 |
children | 55f44ec2a0c6 |
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 |
190 | 26 |
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
27 import ODC |
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
28 |
387 | 29 open filter O |
30 | |
236 | 31 open _∧_ |
32 open _∨_ | |
33 open Bool | |
34 | |
265 | 35 |
331 | 36 open HOD |
37 | |
379 | 38 ------- |
39 -- the set of finite partial functions from ω to 2 | |
40 -- | |
41 -- | |
42 | |
387 | 43 open import Data.List |
44 open import Data.Maybe | |
379 | 45 |
46 import OPair | |
47 open OPair O | |
48 | |
49 open PFunc | |
50 | |
387 | 51 _f∩_ : (f g : PFunc (Lift n Nat) (Lift n Two) ) → PFunc (Lift n Nat) (Lift n Two) |
52 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) | |
53 ; pmap = λ x p → pmap f x (proj1 p) ; meq = meq f } | |
381 | 54 |
387 | 55 _↑_ : (Nat → Two) → Nat → PFunc (Lift n Nat) (Lift n Two) |
56 _↑_ f i = record { dom = λ x → Lift n (lower x ≤ i) ; pmap = λ x _ → lift (f (lower x)) ; meq = λ {x} {p} {q} → refl } | |
381 | 57 |
387 | 58 record _f⊆_ (f g : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where |
59 field | |
60 extend : {x : Nat} → (fr : dom f (lift x) ) → dom g (lift x ) | |
61 feq : {x : Nat} → {fr : dom f (lift x) } → pmap f (lift x) fr ≡ pmap g (lift x) (extend fr) | |
381 | 62 |
387 | 63 record FiniteF (p : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where |
379 | 64 field |
65 f-max : Nat | |
66 f-func : Nat → Two | |
67 f-p⊆f : p f⊆ (f-func ↑ f-max) | |
68 f-f⊆p : (f-func ↑ f-max) f⊆ p | |
69 | |
70 open FiniteF | |
71 | |
387 | 72 |
381 | 73 -- Dense-Gf : {n : Level} → F-Dense (PFunc {n}) (λ x → Lift (suc n) (One {n})) _f⊆_ _f∩_ |
74 -- Dense-Gf = record { | |
75 -- dense = λ x → FiniteF x | |
76 -- ; d⊆P = lift OneObj | |
387 | 77 -- ; dense-f = λ x → record { dom = {!!} ; pmap = {!!} } |
381 | 78 -- ; dense-d = λ {p} d → {!!} |
79 -- ; dense-p = λ {p} d → {!!} | |
80 -- } | |
379 | 81 |
387 | 82 open _f⊆_ |
83 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
|
84 |
370 | 85 |
363 | 86 ODSuc : (y : HOD) → infinite ∋ y → HOD |
87 ODSuc y lt = Union (y , (y , y)) | |
88 | |
366 | 89 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where |
90 hφ : Hω2 0 o∅ | |
91 h0 : {i : Nat} {x : Ordinal } → Hω2 i x → | |
92 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) , ord→od x ))) | |
93 h1 : {i : Nat} {x : Ordinal } → Hω2 i x → | |
94 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) , ord→od x ))) | |
95 he : {i : Nat} {x : Ordinal } → Hω2 i x → | |
96 Hω2 (Suc i) x | |
97 | |
98 record Hω2r (x : Ordinal) : Set n where | |
99 field | |
100 count : Nat | |
101 hω2 : Hω2 count x | |
102 | |
103 open Hω2r | |
363 | 104 |
105 HODω2 : HOD | |
366 | 106 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where |
365 | 107 ω<next : {y : Ordinal} → infinite-d y → y o< next o∅ |
108 ω<next = ω<next-o∅ ho< | |
366 | 109 lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x |
110 lemma = {!!} | |
111 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅ | |
112 odmax0 {y} r with hω2 r | |
113 ... | hφ = x<nx | |
114 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x}) | |
115 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x}) | |
116 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx | |
363 | 117 |
387 | 118 3→Hω2 : List (Maybe Two) → HOD |
385 | 119 3→Hω2 t = list→hod t 0 where |
387 | 120 list→hod : List (Maybe Two) → Nat → HOD |
385 | 121 list→hod [] _ = od∅ |
387 | 122 list→hod (just i0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) |
123 list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) | |
124 list→hod (nothing ∷ t) i = list→hod t (Suc i ) | |
385 | 125 |
387 | 126 Hω2→3 : (x : HOD) → HODω2 ∋ x → List (Maybe Two) |
385 | 127 Hω2→3 x = lemma where |
387 | 128 lemma : { y : Ordinal } → Hω2r y → List (Maybe Two) |
385 | 129 lemma record { count = 0 ; hω2 = hφ } = [] |
387 | 130 lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 } |
131 lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 = hω3 } | |
132 lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 = hω3 } | |
385 | 133 |
370 | 134 ω→2 : HOD |
379 | 135 ω→2 = Replace (Power infinite) (λ p → Replace infinite (λ x → < x , repl p x > )) where |
370 | 136 repl : HOD → HOD → HOD |
137 repl p x with ODC.∋-p O p x | |
138 ... | yes _ = nat→ω 1 | |
139 ... | no _ = nat→ω 0 | |
368 | 140 |
385 | 141 ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two |
142 ω→2f x = {!!} | |
143 | |
144 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD | |
145 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) )) | |
146 | |
363 | 147 -- the set of finite partial functions from ω to 2 |
148 | |
149 Hω2f : Set (suc n) | |
150 Hω2f = (Nat → Set n) → Two | |
151 | |
152 Hω2f→Hω2 : Hω2f → HOD | |
381 | 153 Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} } |
363 | 154 |
155 | |
386 | 156 record CountableOrdinal : Set (suc (suc n)) where |
157 field | |
158 ctl→ : Nat → Ordinal | |
159 ctl← : Ordinal → Nat | |
160 ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x | |
161 ctl-iso← : { x : Nat } → ctl← (ctl→ x ) ≡ x | |
388 | 162 |
163 record CountableHOD : Set (suc (suc n)) where | |
164 field | |
390 | 165 mhod : HOD |
166 mtl→ : Nat → Ordinal | |
167 mtl→∈P : (i : Nat) → odef mhod (mtl→ i) | |
168 mtl← : (x : Ordinal) → odef mhod x → Nat | |
169 mtl-iso→ : { x : Ordinal } → (lt : odef mhod x ) → mtl→ (mtl← x lt ) ≡ x | |
170 mtl-iso← : { x : Nat } → mtl← (mtl→ x ) (mtl→∈P x) ≡ x | |
388 | 171 |
386 | 172 |
387 | 173 open CountableOrdinal |
388 | 174 open CountableHOD |
387 | 175 |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
176 PGHOD : (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
177 PGHOD i C P p = record { od = record { def = λ x → odef P x ∧ odef (ord→od (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (ord→od p) y → odef (ord→od x) y ) } |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
178 ; odmax = odmax P ; <odmax = λ {y} lt → <odmax P (proj1 lt) } |
388 | 179 |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
180 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
|
181 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
|
182 next-p C P i p | yes y = p |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
183 next-p C P i p | no not = od→ord (ODC.minimal O (PGHOD i C P p ) not) |
387 | 184 |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
185 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
|
186 find-p C P Zero x = x |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
187 find-p C P (Suc i) x = find-p C P i ( next-p C P i x ) |
388 | 188 |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
189 record PDN (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where |
388 | 190 field |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
191 gr : Nat |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
192 pn<gr : (y : Ordinal) → odef (ord→od x) y → odef (ord→od (find-p C P gr o∅)) y |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
193 px∈ω : odef P x |
388 | 194 |
195 open PDN | |
386 | 196 |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
197 PDHOD : (C : CountableOrdinal) → (P : HOD ) → HOD |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
198 PDHOD C P = record { od = record { def = λ x → PDN C P x } |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
199 ; odmax = odmax (Power P) ; <odmax = {!!} } where |
388 | 200 |
201 -- | |
202 -- p 0 ≡ ∅ | |
203 -- p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q | |
204 --- else p n | |
386 | 205 |
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
206 P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
207 P-GenericFilter C P = record { |
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
208 genf = record { filter = PDHOD C P ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } |
386 | 209 ; generic = λ D → {!!} |
210 } |