Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate generic-filter.agda @ 403:ce2ce3f62023
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 28 Jul 2020 10:51:08 +0900 |
| parents | 48ea49494fd1 |
| children | 6dcea4c7cba1 |
| 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 | |
| 392 | 43 open import Data.List hiding (filter) |
| 387 | 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 open _f⊆_ |
| 64 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
|
65 |
| 363 | 66 ODSuc : (y : HOD) → infinite ∋ y → HOD |
| 67 ODSuc y lt = Union (y , (y , y)) | |
| 68 | |
| 366 | 69 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where |
| 70 hφ : Hω2 0 o∅ | |
| 71 h0 : {i : Nat} {x : Ordinal } → Hω2 i x → | |
| 72 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) , ord→od x ))) | |
| 73 h1 : {i : Nat} {x : Ordinal } → Hω2 i x → | |
| 74 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) , ord→od x ))) | |
| 75 he : {i : Nat} {x : Ordinal } → Hω2 i x → | |
| 76 Hω2 (Suc i) x | |
| 77 | |
| 78 record Hω2r (x : Ordinal) : Set n where | |
| 79 field | |
| 80 count : Nat | |
| 81 hω2 : Hω2 count x | |
| 82 | |
| 83 open Hω2r | |
| 363 | 84 |
| 85 HODω2 : HOD | |
| 366 | 86 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where |
| 393 | 87 P : (i j : Nat) (x : Ordinal ) → HOD |
| 88 P i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x | |
| 394 | 89 nat1 : (i : Nat) (x : Ordinal) → od→ord (nat→ω i) o< next x |
| 90 nat1 i x = next< nexto∅ ( <odmax infinite (ω∋nat→ω {i})) | |
| 393 | 91 lemma1 : (i j : Nat) (x : Ordinal ) → osuc (od→ord (P i j x)) o< next x |
| 394 | 92 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) ) ) |
| 93 (subst (λ k → k o< next x) (sym diso) x<nx )) | |
| 393 | 94 lemma : (i j : Nat) (x : Ordinal ) → od→ord (Union (P i j x)) o< next x |
| 95 lemma i j x = next< (lemma1 i j x ) ho< | |
| 366 | 96 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅ |
| 97 odmax0 {y} r with hω2 r | |
| 98 ... | hφ = x<nx | |
| 393 | 99 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 0 x) |
| 100 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 1 x) | |
| 366 | 101 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx |
| 363 | 102 |
| 387 | 103 3→Hω2 : List (Maybe Two) → HOD |
| 385 | 104 3→Hω2 t = list→hod t 0 where |
| 387 | 105 list→hod : List (Maybe Two) → Nat → HOD |
| 385 | 106 list→hod [] _ = od∅ |
| 387 | 107 list→hod (just i0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) |
| 108 list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) | |
| 109 list→hod (nothing ∷ t) i = list→hod t (Suc i ) | |
| 385 | 110 |
| 387 | 111 Hω2→3 : (x : HOD) → HODω2 ∋ x → List (Maybe Two) |
| 385 | 112 Hω2→3 x = lemma where |
| 387 | 113 lemma : { y : Ordinal } → Hω2r y → List (Maybe Two) |
| 385 | 114 lemma record { count = 0 ; hω2 = hφ } = [] |
| 387 | 115 lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 } |
| 116 lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 = hω3 } | |
| 117 lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 = hω3 } | |
| 385 | 118 |
| 370 | 119 ω→2 : HOD |
| 394 | 120 ω→2 = Power infinite |
| 368 | 121 |
| 385 | 122 ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two |
| 394 | 123 ω→2f x lt n with ODC.∋-p O x (nat→ω n) |
| 124 ω→2f x lt n | yes p = i1 | |
| 125 ω→2f x lt n | no ¬p = i0 | |
| 385 | 126 |
| 395 | 127 fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n |
| 128 fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (od→ord x) ) → f (ω→nat x lt) ≡ i1 ) | |
| 129 | |
| 130 fω→2 : (Nat → Two) → HOD | |
| 131 fω→2 f = Select infinite (fω→2-sel f) | |
| 132 | |
| 133 open _==_ | |
| 134 | |
| 135 postulate f-extensionality : { n m : Level} → Relation.Binary.PropositionalEquality.Extensionality n m | |
| 136 | |
| 396 | 137 ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f |
| 138 ω2∋f f = power← infinite (fω→2 f) (λ {x} lt → proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt)) | |
| 139 | |
| 140 ω→2f≡i0 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω) ≡ i1 → X ∋ i | |
| 141 ω→2f≡i0 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω)) | |
| 400 | 142 ω→2f≡i0 X i iω lt eq | yes p = subst (λ k → X ∋ k ) {!!} p |
| 396 | 143 |
| 395 | 144 ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt ) =h= X |
| 145 ω→2f-iso X lt = record { | |
| 146 eq→ = eq1 | |
| 147 ; eq← = eq2 | |
| 148 } where | |
| 149 eq1 : {x : Ordinal} → odef (fω→2 (ω→2f X lt)) x → odef X x | |
| 396 | 150 eq1 {x} fx = {!!} where |
| 151 x-nat : odef infinite x | |
| 152 x-nat = subst (λ k → odef infinite k) diso ( ODC.double-neg-eilm O | |
| 153 (power→ infinite _ (ω2∋f (ω→2f X lt)) (d→∋ (fω→2 (ω→2f X lt)) fx ))) | |
| 154 i : Nat | |
| 155 i = ω→nat (ord→od x) (d→∋ infinite x-nat) | |
| 156 is-i1 : ω→2f X lt i ≡ i1 | |
| 157 is-i1 = {!!} | |
| 395 | 158 eq2 : {x : Ordinal} → odef X x → odef (fω→2 (ω→2f X lt)) x |
| 396 | 159 eq2 {x} Xx = {!!} where |
| 160 x-nat : odef infinite x | |
| 161 x-nat = {!!} | |
| 395 | 162 |
| 396 | 163 fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f |
| 395 | 164 fω→2-iso f = f-extensionality (λ x → eq1 x ) where |
| 396 | 165 eq1 : (x : Nat) → ω→2f (fω→2 f) (ω2∋f f) x ≡ f x |
| 395 | 166 eq1 x = {!!} |
| 167 | |
| 168 | |
| 385 | 169 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD |
| 170 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) )) | |
| 171 | |
| 386 | 172 record CountableOrdinal : Set (suc (suc n)) where |
| 173 field | |
| 174 ctl→ : Nat → Ordinal | |
| 175 ctl← : Ordinal → Nat | |
| 176 ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x | |
| 177 ctl-iso← : { x : Nat } → ctl← (ctl→ x ) ≡ x | |
| 388 | 178 |
| 179 record CountableHOD : Set (suc (suc n)) where | |
| 180 field | |
| 390 | 181 mhod : HOD |
| 182 mtl→ : Nat → Ordinal | |
| 183 mtl→∈P : (i : Nat) → odef mhod (mtl→ i) | |
| 184 mtl← : (x : Ordinal) → odef mhod x → Nat | |
| 185 mtl-iso→ : { x : Ordinal } → (lt : odef mhod x ) → mtl→ (mtl← x lt ) ≡ x | |
| 186 mtl-iso← : { x : Nat } → mtl← (mtl→ x ) (mtl→∈P x) ≡ x | |
| 388 | 187 |
| 386 | 188 |
| 387 | 189 open CountableOrdinal |
| 388 | 190 open CountableHOD |
| 387 | 191 |
|
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
192 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
|
193 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
|
194 ; odmax = odmax P ; <odmax = λ {y} lt → <odmax P (proj1 lt) } |
| 388 | 195 |
|
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
196 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
|
197 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
|
198 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
|
199 next-p C P i p | no not = od→ord (ODC.minimal O (PGHOD i C P p ) not) |
| 387 | 200 |
|
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
201 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
|
202 find-p C P Zero x = x |
|
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
203 find-p C P (Suc i) x = find-p C P i ( next-p C P i x ) |
| 388 | 204 |
|
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
205 record PDN (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where |
| 388 | 206 field |
|
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
207 gr : Nat |
|
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
208 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
|
209 px∈ω : odef P x |
| 388 | 210 |
| 211 open PDN | |
| 386 | 212 |
|
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
213 PDHOD : (C : CountableOrdinal) → (P : HOD ) → HOD |
|
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
214 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
|
215 ; odmax = odmax (Power P) ; <odmax = {!!} } where |
| 388 | 216 |
| 217 -- | |
| 218 -- p 0 ≡ ∅ | |
| 219 -- p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q | |
| 220 --- else p n | |
| 386 | 221 |
|
391
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
222 P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P |
|
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
223 P-GenericFilter C P = record { |
|
e98b5774d180
generic filter defined
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
390
diff
changeset
|
224 genf = record { filter = PDHOD C P ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } |
| 386 | 225 ; generic = λ D → {!!} |
| 226 } | |
| 392 | 227 |
| 228 open GenericFilter | |
| 229 open Filter | |
| 230 | |
| 231 record Incompatible (P : HOD ) : Set (suc (suc n)) where | |
| 232 field | |
| 233 except : HOD → ( HOD ∧ HOD ) | |
| 234 incompatible : { p : HOD } → P ∋ p → P ∋ proj1 (except p ) → P ∋ proj2 (except p ) | |
| 235 → ( p ⊆ proj1 (except p) ) ∧ ( p ⊆ proj2 (except p) ) | |
| 236 → ∀ ( r : HOD ) → P ∋ r → ¬ (( proj1 (except p) ⊆ r ) ∧ ( proj2 (except p) ⊆ r )) | |
| 237 | |
| 238 lemma725 : (M : CountableHOD ) (C : CountableOrdinal) (P : HOD ) → mhod M ∋ P | |
| 239 → Incompatible P → ¬ ( mhod M ∋ filter ( genf ( P-GenericFilter C P ))) | |
| 240 lemma725 = {!!} | |
| 241 | |
| 242 lemma725-1 : Incompatible HODω2 | |
| 243 lemma725-1 = {!!} | |
| 244 | |
| 245 lemma726 : (C : CountableOrdinal) (P : HOD ) | |
| 246 → Union ( filter ( genf ( P-GenericFilter C HODω2 ))) =h= ω→2 | |
| 247 lemma726 = {!!} | |
| 248 | |
| 249 -- | |
| 250 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > } | |
| 251 -- | |
| 252 | |
| 253 | |
| 254 | |
| 255 |