Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate generic-filter.agda @ 387:8b0715e28b33
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 25 Jul 2020 09:09:00 +0900 |
| parents | filter.agda@24a66a246316 |
| children | 19687f3304c9 |
| 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 Gf (f : Nat → Two) (p : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where |
|
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
|
64 field |
|
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 gn : Nat |
|
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
|
66 f<n : (f ↑ gn) f⊆ p |
|
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
|
67 |
| 387 | 68 record FiniteF (p : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where |
| 379 | 69 field |
| 70 f-max : Nat | |
| 71 f-func : Nat → Two | |
| 72 f-p⊆f : p f⊆ (f-func ↑ f-max) | |
| 73 f-f⊆p : (f-func ↑ f-max) f⊆ p | |
| 74 | |
| 75 open FiniteF | |
| 76 | |
| 387 | 77 |
| 381 | 78 -- Dense-Gf : {n : Level} → F-Dense (PFunc {n}) (λ x → Lift (suc n) (One {n})) _f⊆_ _f∩_ |
| 79 -- Dense-Gf = record { | |
| 80 -- dense = λ x → FiniteF x | |
| 81 -- ; d⊆P = lift OneObj | |
| 387 | 82 -- ; dense-f = λ x → record { dom = {!!} ; pmap = {!!} } |
| 381 | 83 -- ; dense-d = λ {p} d → {!!} |
| 84 -- ; dense-p = λ {p} d → {!!} | |
| 85 -- } | |
| 379 | 86 |
|
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
|
87 open Gf |
| 387 | 88 open _f⊆_ |
| 89 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
|
90 |
| 387 | 91 GF : (Nat → Two ) → F-Filter (PFunc (Lift n Nat) (Lift n Two)) (λ x → Lift (suc n) (One {n}) ) _f⊆_ _f∩_ |
| 92 GF f = record { | |
| 372 | 93 filter = λ p → Gf f p |
| 374 | 94 ; f⊆P = lift OneObj |
| 95 ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q } | |
| 96 ; filter2 = λ {p} {q} fp fq → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq } | |
| 372 | 97 } where |
| 387 | 98 f1 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q |
| 379 | 99 f1 {p} {q} fp p⊆q = record { extend = λ {x} x<g → extend p⊆q (extend (f<n fp ) x<g) ; feq = λ {x} {fr} → lemma {x} {fr} } where |
| 387 | 100 lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → pmap (f ↑ gn fp) (lift x) fr ≡ pmap q (lift x) (extend p⊆q (extend (f<n fp) fr)) |
| 379 | 101 lemma {x} {fr} = begin |
| 387 | 102 pmap (f ↑ gn fp) (lift x) fr |
| 379 | 103 ≡⟨ feq (f<n fp ) ⟩ |
| 387 | 104 pmap p (lift x) (extend (f<n fp) fr) |
| 379 | 105 ≡⟨ feq p⊆q ⟩ |
| 387 | 106 pmap q (lift x) (extend p⊆q (extend (f<n fp) fr)) |
| 379 | 107 ∎ where open ≡-Reasoning |
| 387 | 108 f2 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (fp : Gf f p ) → (fq : Gf f q ) → (f ↑ (min (gn fp) (gn fq))) f⊆ (p f∩ q) |
| 379 | 109 f2 {p} {q} fp fq = record { extend = λ {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where |
| 387 | 110 fmin : PFunc (Lift n Nat) (Lift n Two) |
| 379 | 111 fmin = f ↑ (min (gn fp) (gn fq)) |
| 387 | 112 lemma1 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p (lift x)) (gr : dom q (lift x)) → pmap p (lift x) fr ≡ pmap q (lift x) gr |
| 379 | 113 lemma1 {x} x<g fr gr = begin |
| 387 | 114 pmap p (lift x) fr |
| 379 | 115 ≡⟨ meq p ⟩ |
| 387 | 116 pmap p (lift x) (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _)))) |
| 379 | 117 ≡⟨ sym (feq (f<n fp)) ⟩ |
| 387 | 118 pmap (f ↑ (min (gn fp) (gn fq))) (lift x) x<g |
| 379 | 119 ≡⟨ feq (f<n fq) ⟩ |
| 387 | 120 pmap q (lift x) (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _)))) |
| 379 | 121 ≡⟨ meq q ⟩ |
| 387 | 122 pmap q (lift x) gr |
| 379 | 123 ∎ where open ≡-Reasoning |
| 387 | 124 lemma2 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) (lift x) |
| 379 | 125 lemma2 x<g = record { proj1 = extend (f<n fp ) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))) ; |
| 126 proj2 = record {proj1 = extend (f<n fq ) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))) ; proj2 = lemma1 x<g }} | |
| 387 | 127 f∩→⊆ : (p q : PFunc (Lift n Nat) (Lift n Two) ) → (p f∩ q ) f⊆ q |
| 379 | 128 f∩→⊆ p q = record { |
| 129 extend = λ {x} pq → proj1 (proj2 pq) | |
| 130 ; feq = λ {x} {fr} → (proj2 (proj2 fr)) (proj1 fr) (proj1 (proj2 fr)) | |
| 131 } | |
| 387 | 132 lemma3 : {x : Nat} → ( fr : Lift n (x ≤ min (gn fp) (gn fq))) → pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr ≡ pmap (p f∩ q) (lift x) (lemma2 fr) |
| 379 | 133 lemma3 {x} fr = |
| 387 | 134 pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr |
| 379 | 135 ≡⟨ feq (f<n fq) ⟩ |
| 387 | 136 pmap q (lift x) (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) )) |
| 379 | 137 ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} ) ⟩ |
| 387 | 138 pmap (p f∩ q) (lift x) (lemma2 fr) |
| 379 | 139 ∎ where open ≡-Reasoning |
| 140 | |
| 370 | 141 |
| 363 | 142 ODSuc : (y : HOD) → infinite ∋ y → HOD |
| 143 ODSuc y lt = Union (y , (y , y)) | |
| 144 | |
| 366 | 145 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where |
| 146 hφ : Hω2 0 o∅ | |
| 147 h0 : {i : Nat} {x : Ordinal } → Hω2 i x → | |
| 148 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) , ord→od x ))) | |
| 149 h1 : {i : Nat} {x : Ordinal } → Hω2 i x → | |
| 150 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) , ord→od x ))) | |
| 151 he : {i : Nat} {x : Ordinal } → Hω2 i x → | |
| 152 Hω2 (Suc i) x | |
| 153 | |
| 154 record Hω2r (x : Ordinal) : Set n where | |
| 155 field | |
| 156 count : Nat | |
| 157 hω2 : Hω2 count x | |
| 158 | |
| 159 open Hω2r | |
| 363 | 160 |
| 161 HODω2 : HOD | |
| 366 | 162 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where |
| 365 | 163 ω<next : {y : Ordinal} → infinite-d y → y o< next o∅ |
| 164 ω<next = ω<next-o∅ ho< | |
| 366 | 165 lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x |
| 166 lemma = {!!} | |
| 167 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅ | |
| 168 odmax0 {y} r with hω2 r | |
| 169 ... | hφ = x<nx | |
| 170 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x}) | |
| 171 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x}) | |
| 172 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx | |
| 363 | 173 |
| 387 | 174 3→Hω2 : List (Maybe Two) → HOD |
| 385 | 175 3→Hω2 t = list→hod t 0 where |
| 387 | 176 list→hod : List (Maybe Two) → Nat → HOD |
| 385 | 177 list→hod [] _ = od∅ |
| 387 | 178 list→hod (just i0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) |
| 179 list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) | |
| 180 list→hod (nothing ∷ t) i = list→hod t (Suc i ) | |
| 385 | 181 |
| 387 | 182 Hω2→3 : (x : HOD) → HODω2 ∋ x → List (Maybe Two) |
| 385 | 183 Hω2→3 x = lemma where |
| 387 | 184 lemma : { y : Ordinal } → Hω2r y → List (Maybe Two) |
| 385 | 185 lemma record { count = 0 ; hω2 = hφ } = [] |
| 387 | 186 lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 } |
| 187 lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 = hω3 } | |
| 188 lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 = hω3 } | |
| 385 | 189 |
| 370 | 190 ω→2 : HOD |
| 379 | 191 ω→2 = Replace (Power infinite) (λ p → Replace infinite (λ x → < x , repl p x > )) where |
| 370 | 192 repl : HOD → HOD → HOD |
| 193 repl p x with ODC.∋-p O p x | |
| 194 ... | yes _ = nat→ω 1 | |
| 195 ... | no _ = nat→ω 0 | |
| 368 | 196 |
| 385 | 197 ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two |
| 198 ω→2f x = {!!} | |
| 199 | |
| 200 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD | |
| 201 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) )) | |
| 202 | |
| 203 record Gfo (x : Ordinal) : Set n where | |
| 204 field | |
| 205 gfunc : Ordinal | |
| 206 gmax : Ordinal | |
| 207 gcond : (odef ω→2 gfunc) ∧ (odef infinite gmax) | |
| 208 gfdef : {!!} -- ( ↑n (ord→od gfunc) (ord→od gmax) (subst₂ ? ? ? gcond) ) ⊆ ord→od x | |
| 209 pcond : odef HODω2 x | |
| 210 | |
| 211 open Gfo | |
| 212 | |
| 213 HODGf : HOD | |
| 214 HODGf = record { od = record { def = λ x → Gfo x } ; odmax = next o∅ ; <odmax = {!!} } | |
| 368 | 215 |
| 216 G : (Nat → Two) → Filter HODω2 | |
| 217 G f = record { | |
| 385 | 218 filter = HODGf |
| 365 | 219 ; f⊆PL = {!!} |
| 220 ; filter1 = {!!} | |
| 221 ; filter2 = {!!} | |
| 222 } where | |
| 223 filter0 : HOD | |
| 224 filter0 = {!!} | |
| 225 f⊆PL1 : filter0 ⊆ Power HODω2 | |
| 226 f⊆PL1 = {!!} | |
| 227 filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q | |
| 228 filter11 = {!!} | |
| 229 filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q) | |
| 230 filter12 = {!!} | |
| 231 | |
| 363 | 232 -- the set of finite partial functions from ω to 2 |
| 233 | |
| 234 Hω2f : Set (suc n) | |
| 235 Hω2f = (Nat → Set n) → Two | |
| 236 | |
| 237 Hω2f→Hω2 : Hω2f → HOD | |
| 381 | 238 Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} } |
| 363 | 239 |
| 240 | |
| 386 | 241 record CountableOrdinal : Set (suc (suc n)) where |
| 242 field | |
| 243 ctl→ : Nat → Ordinal | |
| 244 ctl← : Ordinal → Nat | |
| 245 ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x | |
| 246 ctl-iso← : { x : Nat } → ctl← (ctl→ x ) ≡ x | |
| 247 | |
| 387 | 248 open CountableOrdinal |
| 249 | |
| 250 PGOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Set n | |
| 251 PGOD i C p q = ¬ ( odef (ord→od (ctl→ C i)) q ∧ ( (x : Ordinal ) → odef (ord→od p) x → odef (ord→od q) x )) | |
| 252 | |
| 253 PGHOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD | |
| 254 PGHOD i C p = record { od = record { def = λ x → PGOD i C {!!} {!!} } ; odmax = {!!} ; <odmax = {!!} } | |
| 386 | 255 |
| 387 | 256 ord-compare : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Ordinal |
| 257 ord-compare i C p q with ODC.p∨¬p O ( (q : Ordinal ) → PGOD i C p q ) | |
| 258 ord-compare i C p q | case1 y = p | |
| 259 ord-compare i C p q | case2 n = od→ord (ODC.minimal O (PGHOD i C p ) (∅< (subst₂ (λ j k → odef j {!!} ) refl {!!} n)) ) | |
| 386 | 260 |
| 387 | 261 data PD (P : HOD) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) → Set (suc n) where |
| 262 pd0 : PD P C o∅ 0 | |
| 263 -- pdq : {q pnx : Ordinal } {n : Nat} → (pn : PD P C pnx n ) → odef (ctl→ C n) q → ord→od p0x ⊆ ord→od q → PD P C q (suc n) | |
| 386 | 264 |
| 265 P-GenericFilter : {P : HOD} → (C : CountableOrdinal) → GenericFilter P | |
| 266 P-GenericFilter {P} C = record { | |
| 267 genf = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } | |
| 268 ; generic = λ D → {!!} | |
| 269 } |