0 | module Theory.List1
 1 |
 2 | import Data.List1
 3 |
 4 | import Theory.List
 5 |
 6 | ||| Concatenation of non-empty lists os associative
 7 | total
 8 | export
 9 | concat_assoc : (l, l', l'' : List1 a) -> l ++ (l' ++ l'') = (l ++ l') ++ l''
10 | concat_assoc (x ::: xs) (y ::: ys) (z ::: zs)
11 |   = rewrite List.concat_assoc xs (y :: ys) (z :: zs)
12 |     in Refl
13 |
14 | ||| The mapping of a function on a concatenation of two non-empty lists
15 | ||| is the concatenation of mappings of that function on those lists
16 | total
17 | export
18 | map_concat : {f : a -> b}
19 |           -> (l, l' : List1 a)
20 |           -> map f (l ++ l') = map f l ++ map f l'
21 | map_concat {f} (x ::: xs) (y ::: ys)
22 |   = rewrite List.map_concat {f} xs (y :: ys)
23 |     in Refl
24 |
25 |
26 | ||| `map_concat` in the case when the right operand is a singleton
27 | total
28 | export
29 | map_append : {f : a -> b}
30 |           -> (l : List1 a)
31 |           -> (x : a)
32 |           -> map f (l ++ (x ::: Nil)) = map f l ++ (f x ::: Nil)
33 | map_append l x = map_concat l (x ::: Nil)
34 |
35 |
36 |
37 |