Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison filter.agda @ 382:c3a0fb13e267

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Jul 2020 21:32:58 +0900
parents d2cb5278e46d
children 5994f10d9bfd
comparison
equal deleted inserted replaced
381:d2cb5278e46d 382:c3a0fb13e267
357 ... | i1 = ↑app f x (j1 ∷ y ) 357 ... | i1 = ↑app f x (j1 ∷ y )
358 358
359 _3↑_ : (Nat → Two) → Nat → List Three 359 _3↑_ : (Nat → Two) → Nat → List Three
360 f 3↑ x = ↑app f x [] 360 f 3↑ x = ↑app f x []
361 361
362 listn : Nat → List Nat 362 3↑22 : (f : Nat → Two) (i j : Nat) → List Three
363 listn 0 = [] 363 3↑22 f Zero j = []
364 listn (Suc n) = n ∷ listn n 364 3↑22 f (Suc i) j with f i
365 365 3↑22 f (Suc i) j | i0 = j0 ∷ 3↑22 f i (Suc j)
366 rev : {A : Set} → List A → List A 366 3↑22 f (Suc i) j | i1 = j1 ∷ 3↑22 f i (Suc j)
367 rev {A} x = rev1 x [] where 367
368 rev1 : List A → List A → List A 368 3↑2 : (Nat → Two) → Nat → List Three
369 rev1 [] y = y 369 3↑2 f i = 3↑22 f i 0
370 rev1 (h ∷ x) y = rev1 x (h ∷ y) 370
371 371 lemma10 : (s t : List Three ) → (s 3⊆ t) → ((j0 ∷ s) 3⊆ (j0 ∷ t))
372 Lmap : {A B : Set} → (A → B ) → List A → List B 372 lemma10 s t eq = eq
373 Lmap f [] = [] 373 lemma11 : (s t : List Three ) → (s 3⊆ t) → ((j1 ∷ s) 3⊆ (j1 ∷ t))
374 Lmap f (h ∷ t) = f h ∷ Lmap f t 374 lemma11 s t eq = eq
375 375 lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t))
376 3↑1 : (Nat → Two) → Nat → List Three 376 lemma12 s t eq = eq
377 3↑1 f i with f i 377 lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t))
378 ... | i0 = Lmap (λ x → j0) (rev ( listn i )) 378 lemma13 s t eq = eq
379 ... | i1 = Lmap (λ x → j1) (rev ( listn i )) 379 lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t))
380 380 lemma14 s t eq = eq
381 3↑<1 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑1 f x) 3⊆ (3↑1 f y) 381
382 3↑<1 {f} {x} {y} x<y = lemma (rev ( listn x )) where 382 3↑<2 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑2 f x) 3⊆ (3↑2 f y)
383 lemma : (z : List Nat ) → {!!} 383 3↑<2 {f} {x} {y} x<y = lemma x 0 y x<y (3↑22 f x 0) (3↑22 f y 0) where
384 lemma = {!!} 384 lemma : (i j y : Nat) → i ≤ y → (s t : List Three) → s 3⊆ t
385 lemma Zero j y z≤n [] [] = refl
386 lemma Zero j y z≤n [] (x ∷ t) = 3⊆-[] {x ∷ t}
387 lemma Zero j y z≤n (x ∷ s) [] = {!!}
388 lemma Zero j y z≤n (j0 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t
389 lemma Zero j y z≤n (j0 ∷ s) (j1 ∷ t) = {!!}
390 lemma Zero j y z≤n (j0 ∷ s) (j2 ∷ t) = {!!}
391 lemma Zero j y z≤n (j1 ∷ s) (j0 ∷ t) = {!!}
392 lemma Zero j y z≤n (j1 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t
393 lemma Zero j y z≤n (j1 ∷ s) (j2 ∷ t) = {!!}
394 lemma Zero j y z≤n (j2 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t
395 lemma Zero j y z≤n (j2 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t
396 lemma Zero j y z≤n (j2 ∷ s) (j2 ∷ t) = lemma Zero j y z≤n s t
397 lemma (Suc i) j (Suc y) (s≤s i<y) [] t = 3⊆-[] {t}
398 lemma (Suc i) j (Suc y) (s≤s i<y) (x ∷ s) [] = {!!}
399 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j0 ∷ t) = {!!}
400 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j1 ∷ t) = {!!}
401 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j2 ∷ t) = {!!}
402 lemma (Suc i) j (Suc y) (s≤s i<y) (j1 ∷ s) (x1 ∷ t) = {!!}
403 lemma (Suc i) j (Suc y) (s≤s i<y) (j2 ∷ s) (x1 ∷ t) = {!!}
404 -- with lemma i j y i<y s t
385 405
386 406
387 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x) 3⊆ (f 3↑ y) 407 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x) 3⊆ (f 3↑ y)
388 3↑< {f} {x} {y} x<y = {!!} where 408 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)) 409 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))