Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison filter.agda @ 381:d2cb5278e46d
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 21 Jul 2020 14:34:27 +0900 |
parents | 0a116938a564 |
children | c3a0fb13e267 |
comparison
equal
deleted
inserted
replaced
380:0a116938a564 | 381:d2cb5278e46d |
---|---|
182 ------- | 182 ------- |
183 -- the set of finite partial functions from ω to 2 | 183 -- the set of finite partial functions from ω to 2 |
184 -- | 184 -- |
185 -- | 185 -- |
186 | 186 |
187 data Two : Set n where | 187 data Two : Set where |
188 i0 : Two | 188 i0 : Two |
189 i1 : Two | 189 i1 : Two |
190 | 190 |
191 data Three : Set n where | 191 data Three : Set where |
192 j0 : Three | 192 j0 : Three |
193 j1 : Three | 193 j1 : Three |
194 j2 : Three | 194 j2 : Three |
195 | 195 |
196 open import Data.List hiding (map) | 196 open import Data.List hiding (map) |
197 | 197 |
198 import OPair | 198 import OPair |
199 open OPair O | 199 open OPair O |
200 | 200 |
201 record PFunc : Set (suc n) where | 201 record PFunc {n : Level} : Set (suc n) where |
202 field | 202 field |
203 dom : Nat → Set n | 203 dom : Nat → Set n |
204 map : (x : Nat ) → dom x → Two | 204 map : (x : Nat ) → dom x → Two |
205 meq : {x : Nat } → { p q : dom x } → map x p ≡ map x q | 205 meq : {x : Nat } → { p q : dom x } → map x p ≡ map x q |
206 | 206 |
207 open PFunc | 207 open PFunc |
208 | 208 |
209 data Findp : List Three → (x : Nat) → Set n where | 209 data Findp : List Three → (x : Nat) → Set where |
210 v0 : {n : List Three} → Findp ( j0 ∷ n ) Zero | 210 v0 : {n : List Three} → Findp ( j0 ∷ n ) Zero |
211 v1 : {n : List Three} → Findp ( j1 ∷ n ) Zero | 211 v1 : {n : List Three} → Findp ( j1 ∷ n ) Zero |
212 vn : {n : List Three} {d : Three} → {x : Nat} → Findp n x → Findp (d ∷ n) (Suc x) | 212 vn : {n : List Three} {d : Three} → {x : Nat} → Findp n x → Findp (d ∷ n) (Suc x) |
213 | 213 |
214 FPFunc→PFunc : List Three → PFunc | 214 findp : List Three → (x : Nat) → Set |
215 FPFunc→PFunc fp = record { dom = λ x → findp fp x ; map = λ x p → find fp x p ; meq = λ {x} {p} {q} → feq fp } where | 215 findp n x = Findp n x |
216 findp : List Three → (x : Nat) → Set n | 216 |
217 findp n x = Findp n x | 217 find : (n : List Three ) → (x : Nat) → Findp n x → Two |
218 find : (n : List Three ) → (x : Nat) → Findp n x → Two | 218 find (j0 ∷ _) 0 v0 = i0 |
219 find (j0 ∷ _) 0 v0 = i0 | 219 find (j1 ∷ _) 0 v1 = i1 |
220 find (j1 ∷ _) 0 v1 = i1 | 220 find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p |
221 find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p | 221 |
222 lemma : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p) | 222 Findp=n : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p) |
223 lemma j0 n {x} {p} = refl | 223 Findp=n j0 n {x} {p} = refl |
224 lemma j1 n {x} {p} = refl | 224 Findp=n j1 n {x} {p} = refl |
225 lemma j2 n {x} {p} = refl | 225 Findp=n j2 n {x} {p} = refl |
226 feq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q | 226 |
227 feq n {0} {v0} {v0} = refl | 227 findpeq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q |
228 feq n {0} {v1} {v1} = refl | 228 findpeq n {0} {v0} {v0} = refl |
229 feq [] {Suc x} {()} | 229 findpeq n {0} {v1} {v1} = refl |
230 feq (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (lemma h n) (lemma h n) (feq n {x} {p} {q}) | 230 findpeq [] {Suc x} {()} |
231 | 231 findpeq (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (Findp=n h n) (Findp=n h n) (findpeq n {x} {p} {q}) |
232 record _f⊆_ (f g : PFunc) : Set (suc n) where | 232 |
233 3List→PFunc : List Three → PFunc | |
234 3List→PFunc fp = record { dom = λ x → findp fp x ; map = λ x p → find fp x p ; meq = λ {x} {p} {q} → findpeq fp } | |
235 | |
236 _3⊆b_ : (f g : List Three) → Bool | |
237 [] 3⊆b [] = true | |
238 [] 3⊆b (j2 ∷ g) = [] 3⊆b g | |
239 [] 3⊆b (_ ∷ g) = true | |
240 (j2 ∷ f) 3⊆b [] = f 3⊆b [] | |
241 (j2 ∷ f) 3⊆b (_ ∷ g) = f 3⊆b g | |
242 (j0 ∷ f) 3⊆b (j0 ∷ g) = f 3⊆b g | |
243 (j1 ∷ f) 3⊆b (j1 ∷ g) = f 3⊆b g | |
244 _ 3⊆b _ = false | |
245 | |
246 _3⊆_ : (f g : List Three) → Set | |
247 f 3⊆ g = (f 3⊆b g) ≡ true | |
248 | |
249 _3∩_ : (f g : List Three) → List Three | |
250 [] 3∩ (j2 ∷ g) = j2 ∷ ([] 3∩ g) | |
251 [] 3∩ g = [] | |
252 (j2 ∷ f) 3∩ [] = j2 ∷ f 3∩ [] | |
253 f 3∩ [] = [] | |
254 (j0 ∷ f) 3∩ (j0 ∷ g) = j0 ∷ ( f 3∩ g ) | |
255 (j1 ∷ f) 3∩ (j1 ∷ g) = j1 ∷ ( f 3∩ g ) | |
256 (_ ∷ f) 3∩ (_ ∷ g) = j2 ∷ ( f 3∩ g ) | |
257 | |
258 3∩⊆f : { f g : List Three } → (f 3∩ g ) 3⊆ f | |
259 3∩⊆f {[]} {[]} = refl | |
260 3∩⊆f {[]} {j0 ∷ g} = refl | |
261 3∩⊆f {[]} {j1 ∷ g} = refl | |
262 3∩⊆f {[]} {j2 ∷ g} = 3∩⊆f {[]} {g} | |
263 3∩⊆f {j0 ∷ f} {[]} = refl | |
264 3∩⊆f {j1 ∷ f} {[]} = refl | |
265 3∩⊆f {j2 ∷ f} {[]} = 3∩⊆f {f} {[]} | |
266 3∩⊆f {j0 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g} | |
267 3∩⊆f {j1 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g} | |
268 3∩⊆f {j0 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g} | |
269 3∩⊆f {j1 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g} | |
270 3∩⊆f {j2 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g} | |
271 3∩⊆f {j2 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g} | |
272 3∩⊆f {j0 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g} | |
273 3∩⊆f {j1 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g} | |
274 3∩⊆f {j2 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g} | |
275 | |
276 3∩sym : { f g : List Three } → (f 3∩ g ) ≡ (g 3∩ f ) | |
277 3∩sym {[]} {[]} = refl | |
278 3∩sym {[]} {j0 ∷ g} = refl | |
279 3∩sym {[]} {j1 ∷ g} = refl | |
280 3∩sym {[]} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {[]} {g}) | |
281 3∩sym {j0 ∷ f} {[]} = refl | |
282 3∩sym {j1 ∷ f} {[]} = refl | |
283 3∩sym {j2 ∷ f} {[]} = cong (λ k → j2 ∷ k) (3∩sym {f} {[]}) | |
284 3∩sym {j0 ∷ f} {j0 ∷ g} = cong (λ k → j0 ∷ k) (3∩sym {f} {g}) | |
285 3∩sym {j0 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
286 3∩sym {j0 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
287 3∩sym {j1 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
288 3∩sym {j1 ∷ f} {j1 ∷ g} = cong (λ k → j1 ∷ k) (3∩sym {f} {g}) | |
289 3∩sym {j1 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
290 3∩sym {j2 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
291 3∩sym {j2 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
292 3∩sym {j2 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
293 | |
294 3⊆-[] : { h : List Three } → [] 3⊆ h | |
295 3⊆-[] {[]} = refl | |
296 3⊆-[] {j0 ∷ h} = refl | |
297 3⊆-[] {j1 ∷ h} = refl | |
298 3⊆-[] {j2 ∷ h} = 3⊆-[] {h} | |
299 | |
300 3⊆trans : { f g h : List Three } → f 3⊆ g → g 3⊆ h → f 3⊆ h | |
301 3⊆trans {[]} {[]} {[]} f<g g<h = refl | |
302 3⊆trans {[]} {[]} {j0 ∷ h} f<g g<h = refl | |
303 3⊆trans {[]} {[]} {j1 ∷ h} f<g g<h = refl | |
304 3⊆trans {[]} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h | |
305 3⊆trans {[]} {j2 ∷ g} {[]} f<g g<h = refl | |
306 3⊆trans {[]} {j0 ∷ g} {j0 ∷ h} f<g g<h = refl | |
307 3⊆trans {[]} {j1 ∷ g} {j1 ∷ h} f<g g<h = refl | |
308 3⊆trans {[]} {j2 ∷ g} {j0 ∷ h} f<g g<h = refl | |
309 3⊆trans {[]} {j2 ∷ g} {j1 ∷ h} f<g g<h = refl | |
310 3⊆trans {[]} {j2 ∷ g} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h | |
311 3⊆trans {j2 ∷ f} {[]} {[]} f<g g<h = f<g | |
312 3⊆trans {j2 ∷ f} {[]} {j0 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h}) | |
313 3⊆trans {j2 ∷ f} {[]} {j1 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h}) | |
314 3⊆trans {j2 ∷ f} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h | |
315 3⊆trans {j0 ∷ f} {j0 ∷ g} {[]} f<g () | |
316 3⊆trans {j0 ∷ f} {j1 ∷ g} {[]} f<g () | |
317 3⊆trans {j0 ∷ f} {j2 ∷ g} {[]} () g<h | |
318 3⊆trans {j1 ∷ f} {j0 ∷ g} {[]} f<g () | |
319 3⊆trans {j1 ∷ f} {j1 ∷ g} {[]} f<g () | |
320 3⊆trans {j1 ∷ f} {j2 ∷ g} {[]} () g<h | |
321 3⊆trans {j2 ∷ f} {j2 ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h | |
322 3⊆trans {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
323 3⊆trans {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
324 3⊆trans {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
325 3⊆trans {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
326 3⊆trans {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
327 3⊆trans {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
328 3⊆trans {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
329 | |
330 3⊆∩f : { f g h : List Three } → f 3⊆ g → f 3⊆ h → f 3⊆ (g 3∩ h ) | |
331 3⊆∩f {[]} {[]} {[]} f<g f<h = refl | |
332 3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)} | |
333 3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h} | |
334 3⊆∩f {j2 ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h | |
335 3⊆∩f {j2 ∷ f} {[]} {j0 ∷ h} f<g f<h = f<g | |
336 3⊆∩f {j2 ∷ f} {[]} {j1 ∷ h} f<g f<h = f<g | |
337 3⊆∩f {j2 ∷ f} {[]} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h | |
338 3⊆∩f {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
339 3⊆∩f {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
340 3⊆∩f {j2 ∷ f} {j0 ∷ g} {[]} f<g f<h = f<h | |
341 3⊆∩f {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
342 3⊆∩f {j2 ∷ f} {j0 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
343 3⊆∩f {j2 ∷ f} {j0 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
344 3⊆∩f {j2 ∷ f} {j1 ∷ g} {[]} f<g f<h = f<h | |
345 3⊆∩f {j2 ∷ f} {j1 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
346 3⊆∩f {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
347 3⊆∩f {j2 ∷ f} {j1 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
348 3⊆∩f {j2 ∷ f} {j2 ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h | |
349 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
350 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
351 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
352 | |
353 ↑app :(Nat → Two) → Nat → List Three → List Three | |
354 ↑app f Zero y = y | |
355 ↑app f (Suc x) y with f x | |
356 ... | i0 = ↑app f x (j0 ∷ y ) | |
357 ... | i1 = ↑app f x (j1 ∷ y ) | |
358 | |
359 _3↑_ : (Nat → Two) → Nat → List Three | |
360 f 3↑ x = ↑app f x [] | |
361 | |
362 listn : Nat → List Nat | |
363 listn 0 = [] | |
364 listn (Suc n) = n ∷ listn n | |
365 | |
366 rev : {A : Set} → List A → List A | |
367 rev {A} x = rev1 x [] where | |
368 rev1 : List A → List A → List A | |
369 rev1 [] y = y | |
370 rev1 (h ∷ x) y = rev1 x (h ∷ y) | |
371 | |
372 Lmap : {A B : Set} → (A → B ) → List A → List B | |
373 Lmap f [] = [] | |
374 Lmap f (h ∷ t) = f h ∷ Lmap f t | |
375 | |
376 3↑1 : (Nat → Two) → Nat → List Three | |
377 3↑1 f i with f i | |
378 ... | i0 = Lmap (λ x → j0) (rev ( listn i )) | |
379 ... | i1 = Lmap (λ x → j1) (rev ( listn i )) | |
380 | |
381 3↑<1 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑1 f x) 3⊆ (3↑1 f y) | |
382 3↑<1 {f} {x} {y} x<y = lemma (rev ( listn x )) where | |
383 lemma : (z : List Nat ) → {!!} | |
384 lemma = {!!} | |
385 | |
386 | |
387 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x) 3⊆ (f 3↑ y) | |
388 3↑< {f} {x} {y} x<y = {!!} where | |
389 lemma0 : (i : Nat) → (y : List Three ) → ( ↑app f (Suc i) y ≡ ↑app f i (j0 ∷ y)) ∨ ( ↑app f (Suc i) y ≡ ↑app f i (j1 ∷ y)) | |
390 lemma0 i y with f i | |
391 lemma0 i y | i0 = case1 refl | |
392 lemma0 i y | i1 = case2 refl | |
393 lemma : (i : Nat) → (f 3↑ i) 3⊆ (f 3↑ Suc i) | |
394 lemma i with f i | |
395 lemma i | i0 = {!!} | |
396 lemma i | i1 = {!!} | |
397 | |
398 record Finite3 (p : List Three ) : Set where | |
399 field | |
400 3-max : Nat | |
401 3-func : Nat → Two | |
402 3-p⊆f : p 3⊆ (3-func 3↑ 3-max) | |
403 3-f⊆p : (3-func 3↑ 3-max) 3⊆ p | |
404 | |
405 Finite3b : (p : List Three ) → Bool | |
406 Finite3b [] = true | |
407 Finite3b (j0 ∷ f) = Finite3b f | |
408 Finite3b (j1 ∷ f) = Finite3b f | |
409 Finite3b (j2 ∷ f) = false | |
410 | |
411 finite3cov : (p : List Three ) → List Three | |
412 finite3cov [] = [] | |
413 finite3cov (j0 ∷ x) = j0 ∷ finite3cov x | |
414 finite3cov (j1 ∷ x) = j1 ∷ finite3cov x | |
415 finite3cov (j2 ∷ x) = j0 ∷ finite3cov x | |
416 | |
417 Dense-3 : F-Dense (List Three) (λ x → One) _3⊆_ _3∩_ | |
418 Dense-3 = record { | |
419 dense = λ x → Finite3b x ≡ true | |
420 ; d⊆P = OneObj | |
421 ; dense-f = λ x → finite3cov x | |
422 ; dense-d = λ {p} d → lemma1 p | |
423 ; dense-p = λ {p} d → lemma2 p | |
424 } where | |
425 lemma1 : (p : List Three ) → Finite3b (finite3cov p) ≡ true | |
426 lemma1 [] = refl | |
427 lemma1 (j0 ∷ p) = lemma1 p | |
428 lemma1 (j1 ∷ p) = lemma1 p | |
429 lemma1 (j2 ∷ p) = lemma1 p | |
430 lemma2 : (p : List Three) → p 3⊆ finite3cov p | |
431 lemma2 [] = refl | |
432 lemma2 (j0 ∷ p) = lemma2 p | |
433 lemma2 (j1 ∷ p) = lemma2 p | |
434 lemma2 (j2 ∷ p) = lemma2 p | |
435 | |
436 record 3Gf (f : Nat → Two) (p : List Three ) : Set where | |
437 field | |
438 3gn : Nat | |
439 3f<n : (f 3↑ 3gn) 3⊆ p | |
440 | |
441 open 3Gf | |
442 | |
443 min = Data.Nat._⊓_ | |
444 -- m≤m⊔n = Data.Nat._⊔_ | |
445 open import Data.Nat.Properties | |
446 | |
447 3GF : {n : Level } → (Nat → Two ) → F-Filter (List Three) (λ x → One) _3⊆_ _3∩_ | |
448 3GF {n} f = record { | |
449 filter = λ p → 3Gf f p | |
450 ; f⊆P = OneObj | |
451 ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q | |
452 ; filter2 = λ {p} {q} fp fq → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq } | |
453 } where | |
454 lemma1 : (p q : List Three ) → (fp : 3Gf f p) → (p⊆q : p 3⊆ q) → 3Gf f q | |
455 lemma1 p q fp p⊆q = record { 3gn = 3gn fp ; 3f<n = 3⊆trans {f 3↑ 3gn fp } {p} {q} (3f<n fp) p⊆q } | |
456 lemma2 : (p q : List Three ) → (fp : 3Gf f p) → (fq : 3Gf f q) → (f 3↑ min (3gn fp) (3gn fq)) 3⊆ (p 3∩ q) | |
457 lemma2 p q fp fq = 3⊆∩f {f 3↑ min (3gn fp) (3gn fq) } {p} {q} (3⊆trans {bb} {f 3↑ (3gn fp)} {p} (3↑< {_} {bm} (m⊓n≤m _ _ )) (3f<n fp)) | |
458 (3⊆trans {bb} {f 3↑ (3gn fq)} {q} (3↑< {_} {bm} (m⊓n≤n _ _ )) (3f<n fq)) where | |
459 bb = f 3↑ min (3gn fp) (3gn fq) | |
460 bm = min (3gn fp) (3gn fq) | |
461 | |
462 record _f⊆_ {n : Level } (f g : PFunc {n} ) : Set (suc n) where | |
233 field | 463 field |
234 extend : {x : Nat} → (fr : dom f x ) → dom g x | 464 extend : {x : Nat} → (fr : dom f x ) → dom g x |
235 feq : {x : Nat} → {fr : dom f x } → map f x fr ≡ map g x (extend fr) | 465 feq : {x : Nat} → {fr : dom f x } → map f x fr ≡ map g x (extend fr) |
236 | 466 |
237 open _f⊆_ | 467 open _f⊆_ |
238 | 468 |
239 min = Data.Nat._⊓_ | 469 _f∩_ : {n : Level} → (f g : PFunc {n} ) → PFunc {n} |
240 -- m≤m⊔n = Data.Nat._⊔_ | |
241 open import Data.Nat.Properties | |
242 | |
243 _f∩_ : (f g : PFunc) → PFunc | |
244 f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → map f x fr ≡ map g x gr) | 470 f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → map f x fr ≡ map g x gr) |
245 ; map = λ x p → map f x (proj1 p) ; meq = meq f } | 471 ; map = λ x p → map f x (proj1 p) ; meq = meq f } |
246 | 472 |
247 _↑_ : (Nat → Two) → Nat → PFunc | 473 _↑_ : {n : Level} → (Nat → Two) → Nat → PFunc {n} |
248 f ↑ i = record { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl } | 474 _↑_ {n} f i = record { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl } |
249 | 475 |
250 record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where | 476 record Gf {n : Level} (f : Nat → Two) (p : PFunc {n} ) : Set (suc n) where |
251 field | 477 field |
252 gn : Nat | 478 gn : Nat |
253 f<n : (f ↑ gn) f⊆ p | 479 f<n : (f ↑ gn) f⊆ p |
254 | 480 |
255 record FiniteF (p : PFunc ) : Set (suc n) where | 481 record FiniteF {n : Level} (p : PFunc {n} ) : Set (suc n) where |
256 field | 482 field |
257 f-max : Nat | 483 f-max : Nat |
258 f-func : Nat → Two | 484 f-func : Nat → Two |
259 f-p⊆f : p f⊆ (f-func ↑ f-max) | 485 f-p⊆f : p f⊆ (f-func ↑ f-max) |
260 f-f⊆p : (f-func ↑ f-max) f⊆ p | 486 f-f⊆p : (f-func ↑ f-max) f⊆ p |
261 | 487 |
262 open FiniteF | 488 open FiniteF |
263 | 489 |
264 Dense-Gf : F-Dense PFunc (λ x → Lift (suc n) One) _f⊆_ _f∩_ | 490 -- Dense-Gf : {n : Level} → F-Dense (PFunc {n}) (λ x → Lift (suc n) (One {n})) _f⊆_ _f∩_ |
265 Dense-Gf = record { | 491 -- Dense-Gf = record { |
266 dense = λ x → FiniteF x | 492 -- dense = λ x → FiniteF x |
267 ; d⊆P = lift OneObj | 493 -- ; d⊆P = lift OneObj |
268 ; dense-f = λ x → record { dom = {!!} ; map = {!!} } | 494 -- ; dense-f = λ x → record { dom = {!!} ; map = {!!} } |
269 ; dense-d = λ {p} d → {!!} | 495 -- ; dense-d = λ {p} d → {!!} |
270 ; dense-p = λ {p} d → {!!} | 496 -- ; dense-p = λ {p} d → {!!} |
271 } | 497 -- } |
272 | 498 |
273 open Gf | 499 open Gf |
274 | 500 |
275 GF : (Nat → Two ) → F-Filter PFunc (λ x → Lift (suc n) One ) _f⊆_ _f∩_ | 501 GF : {n : Level } → (Nat → Two ) → F-Filter (PFunc {n}) (λ x → Lift (suc n) (One {n}) ) _f⊆_ _f∩_ |
276 GF f = record { | 502 GF {n} f = record { |
277 filter = λ p → Gf f p | 503 filter = λ p → Gf f p |
278 ; f⊆P = lift OneObj | 504 ; f⊆P = lift OneObj |
279 ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q } | 505 ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q } |
280 ; filter2 = λ {p} {q} fp fq → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq } | 506 ; filter2 = λ {p} {q} fp fq → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq } |
281 } where | 507 } where |
282 f1 : {p q : PFunc } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q | 508 f1 : {p q : PFunc {n} } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q |
283 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 | 509 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 |
284 lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → map (f ↑ gn fp) x fr ≡ map q x (extend p⊆q (extend (f<n fp) fr)) | 510 lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → map (f ↑ gn fp) x fr ≡ map q x (extend p⊆q (extend (f<n fp) fr)) |
285 lemma {x} {fr} = begin | 511 lemma {x} {fr} = begin |
286 map (f ↑ gn fp) x fr | 512 map (f ↑ gn fp) x fr |
287 ≡⟨ feq (f<n fp ) ⟩ | 513 ≡⟨ feq (f<n fp ) ⟩ |
288 map p x (extend (f<n fp) fr) | 514 map p x (extend (f<n fp) fr) |
289 ≡⟨ feq p⊆q ⟩ | 515 ≡⟨ feq p⊆q ⟩ |
290 map q x (extend p⊆q (extend (f<n fp) fr)) | 516 map q x (extend p⊆q (extend (f<n fp) fr)) |
291 ∎ where open ≡-Reasoning | 517 ∎ where open ≡-Reasoning |
292 f2 : {p q : PFunc } → (fp : Gf f p ) → (fq : Gf f q ) → (f ↑ (min (gn fp) (gn fq))) f⊆ (p f∩ q) | 518 f2 : {p q : PFunc {n} } → (fp : Gf {n} f p ) → (fq : Gf {n} f q ) → (f ↑ (min (gn fp) (gn fq))) f⊆ (p f∩ q) |
293 f2 {p} {q} fp fq = record { extend = λ {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where | 519 f2 {p} {q} fp fq = record { extend = λ {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where |
520 fmin : PFunc {n} | |
294 fmin = f ↑ (min (gn fp) (gn fq)) | 521 fmin = f ↑ (min (gn fp) (gn fq)) |
295 lemma1 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p x) (gr : dom q x) → map p x fr ≡ map q x gr | 522 lemma1 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p x) (gr : dom q x) → map p x fr ≡ map q x gr |
296 lemma1 {x} x<g fr gr = begin | 523 lemma1 {x} x<g fr gr = begin |
297 map p x fr | 524 map p x fr |
298 ≡⟨ meq p ⟩ | 525 ≡⟨ meq p ⟩ |
389 | 616 |
390 Hω2f : Set (suc n) | 617 Hω2f : Set (suc n) |
391 Hω2f = (Nat → Set n) → Two | 618 Hω2f = (Nat → Set n) → Two |
392 | 619 |
393 Hω2f→Hω2 : Hω2f → HOD | 620 Hω2f→Hω2 : Hω2f → HOD |
394 Hω2f→Hω2 p = record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} } | 621 Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} } |
395 | 622 |
396 | 623 |