0 | module Theory.List
  1 |
  2 | import Data.List
  3 |
  4 | import Theory.General
  5 |
  6 | ||| Concatenation of lists os associative
  7 | total
  8 | export
  9 | concat_assoc : (l, l', l'' : List a) -> l ++ (l' ++ l'') = (l ++ l') ++ l''
 10 | concat_assoc Nil l' l'' = Refl
 11 | concat_assoc (x :: xs) l' l'' = rewrite revEq $ concat_assoc {l = xs, l', l''} in Refl
 12 |
 13 | ||| Concatenating a list with an emoty list results in the same list
 14 | total
 15 | export
 16 | concat_nil : (l : List a) -> l ++ Nil = l
 17 | concat_nil Nil = Refl
 18 | concat_nil (x :: xs) = rewrite concat_nil xs in Refl
 19 |
 20 |
 21 | ||| The mapping of a function on a concatenation of two lists
 22 | ||| is the concatenation of mappings of that function on those lists
 23 | total
 24 | export
 25 | map_concat
 26 |    : {f : a -> b}
 27 |   -> (l, l' : List a)
 28 |   -> map f (l ++ l') = map f l ++ map f l'
 29 | map_concat {f} Nil l = Refl
 30 | map_concat {f} (x :: xs) l = rewrite revEq $ map_concat {f} xs l in Refl
 31 |
 32 |
 33 | ||| `map_concat` in the case when the right operand is a singleton
 34 | total
 35 | export
 36 | map_append
 37 |    : {f : a -> b}
 38 |   -> (l : List a)
 39 |   -> (x : a)
 40 |   -> map f (l ++ [x]) = map f l ++ [f x]
 41 | map_append l x = map_concat l [x]
 42 |
 43 | ||| The concatenation of a non-empty list with another list is non-empty
 44 | total
 45 | export
 46 | nonempty_concat_left' : (xs, ys : List a) -> NonEmpty xs -> NonEmpty (xs ++ ys)
 47 | nonempty_concat_left' Nil        ys        IsNonEmpty impossible
 48 | nonempty_concat_left' (x :: xs)  Nil       IsNonEmpty = IsNonEmpty
 49 | nonempty_concat_left' (x :: xs)  (y :: ys) IsNonEmpty = IsNonEmpty
 50 |
 51 | ||| The concatenation of a non-empty list with another list is non-empty
 52 | total
 53 | export
 54 | nonempty_concat_left : {xs, ys : List a} -> NonEmpty xs -> NonEmpty (xs ++ ys)
 55 | nonempty_concat_left {xs, ys} = nonempty_concat_left' xs ys
 56 |
 57 | ||| The concatenation of a list with a non-empty list is non-empty
 58 | total
 59 | export
 60 | nonempty_concat_right' : (xs, ys : List a) -> NonEmpty ys -> NonEmpty (xs ++ ys)
 61 | nonempty_concat_right' xs         Nil       IsNonEmpty impossible
 62 | nonempty_concat_right' Nil        (y :: ys) IsNonEmpty = IsNonEmpty
 63 | nonempty_concat_right' (x :: xs)  (y :: ys) IsNonEmpty = IsNonEmpty
 64 |
 65 | ||| The concatenation of a list with a non-empty list is non-empty
 66 | total
 67 | export
 68 | nonempty_concat_right : {xs, ys : List a} -> NonEmpty ys -> NonEmpty (xs ++ ys)
 69 | nonempty_concat_right {xs, ys} = nonempty_concat_right' xs ys
 70 |
 71 | ||| If   the concatenation of one list  with another is non-empty,
 72 | ||| then the concatenation of the other with the one is non-empty
 73 | total
 74 | export
 75 | nonempty_flip_concat' : (xs, ys : List a) -> NonEmpty (xs ++ ys) -> NonEmpty (ys ++ xs)
 76 | nonempty_flip_concat' Nil        Nil       IsNonEmpty impossible
 77 | nonempty_flip_concat' Nil        (y :: ys) IsNonEmpty = IsNonEmpty
 78 | nonempty_flip_concat' (x :: xs)  Nil       IsNonEmpty = IsNonEmpty
 79 | nonempty_flip_concat' (x :: xs)  (y :: ys) IsNonEmpty = IsNonEmpty
 80 |
 81 | ||| If   the concatenation of one list  with another is non-empty,
 82 | ||| then the concatenation of the other with the one is non-empty
 83 | total
 84 | export
 85 | nonempty_flip_concat : {xs, ys : List a} -> NonEmpty (xs ++ ys) -> NonEmpty (ys ++ xs)
 86 | nonempty_flip_concat {xs, ys} = nonempty_flip_concat' xs ys
 87 |
 88 | ||| If a list is non-empty, then any mapping on that list is also non-empty
 89 | total
 90 | export
 91 | nonempty_map' : (xs : List a) -> (f : a -> b) -> NonEmpty xs -> NonEmpty (map f xs)
 92 | nonempty_map' Nil       f IsNonEmpty impossible
 93 | nonempty_map' (x :: xs) f IsNonEmpty = IsNonEmpty
 94 |
 95 | ||| If a list is non-empty, then any mapping on that list is also non-empty
 96 | total
 97 | export
 98 | nonempty_map : {xs : List a} -> {f : a -> b} -> NonEmpty xs -> NonEmpty (map f xs)
 99 | nonempty_map {xs} {f} = nonempty_map' xs f
100 |
101 | ||| If the concatenation of two lists is non-empty, then one of the two lists is non-empty
102 | total
103 | export
104 | nonempty_sublist' : (xs, ys : List a) -> NonEmpty (xs ++ ys) -> Either (NonEmpty xs) (NonEmpty ys)
105 | nonempty_sublist' Nil        Nil       IsNonEmpty impossible
106 | nonempty_sublist' Nil        (y :: ys) IsNonEmpty = Right IsNonEmpty
107 | nonempty_sublist' (x :: xs)  ys        IsNonEmpty = Left IsNonEmpty
108 |
109 | ||| If the concatenation of two lists is non-empty,
110 | ||| then one of the two lists is non-empty
111 | total
112 | export
113 | nonempty_sublist : {xs, ys : List a} -> NonEmpty (xs ++ ys) -> Either (NonEmpty xs) (NonEmpty ys)
114 | nonempty_sublist {xs, ys} = nonempty_sublist' xs ys
115 |
116 | ||| If   the concatenation of two               lists is non-empty,
117 | ||| then the concatenation of mappings on those lists is non-empty
118 | total
119 | export
120 | nonempty_concat_map'
121 |    : (xs, ys : List a)
122 |   -> (f, g : a -> b)
123 |   -> NonEmpty (xs ++ ys)
124 |   -> NonEmpty (map f xs ++ map g ys)
125 | nonempty_concat_map' Nil       Nil       f g IsNonEmpty impossible
126 | nonempty_concat_map' Nil       (y :: ys) f g IsNonEmpty = IsNonEmpty
127 | nonempty_concat_map' (x :: xs) ys        f g IsNonEmpty = IsNonEmpty
128 |
129 | ||| If   the concatenation of two               lists is non-empty,
130 | ||| then the concatenation of mappings on those lists is non-empty
131 | total
132 | export
133 | nonempty_concat_map
134 |    : {xs, ys : List a}
135 |   -> {f, g : a -> b}
136 |   -> NonEmpty (xs ++ ys)
137 |   -> NonEmpty (map f xs ++ map g ys)
138 | nonempty_concat_map {xs, ys, f, g} = nonempty_concat_map' xs ys f g
139 |