0 | module Data.List
   1 |
   2 | import public Control.Function
   3 |
   4 | import Data.Nat
   5 | import Data.List1
   6 | import Data.Fin
   7 | import public Data.Zippable
   8 |
   9 | %default total
  10 |
  11 | ||| Boolean check for whether the list is the empty list.
  12 | public export
  13 | isNil : List a -> Bool
  14 | isNil [] = True
  15 | isNil _  = False
  16 |
  17 | ||| Boolean check for whether the list contains a cons (::) / is non-empty.
  18 | public export
  19 | isCons : List a -> Bool
  20 | isCons [] = False
  21 | isCons _  = True
  22 |
  23 | ||| Add an element to the end of a list.
  24 | ||| O(n). See the `Data.SnocList` module if you need to perform `snoc` often.
  25 | public export
  26 | snoc : List a -> a -> List a
  27 | snoc xs x = xs ++ [x]
  28 |
  29 | ||| Take `n` first elements from `xs`, returning the whole list if
  30 | ||| `n` >= length `xs`.
  31 | |||
  32 | ||| @ n  the number of elements to take
  33 | ||| @ xs the list to take the elements from
  34 | public export
  35 | take : (n : Nat) -> (xs : List a) -> List a
  36 | take (S k) (x :: xs) = x :: take k xs
  37 | take _ _ = []
  38 |
  39 | ||| Remove `n` first elements from `xs`, returning the empty list if
  40 | ||| `n >= length xs`
  41 | |||
  42 | ||| @ n  the number of elements to remove
  43 | ||| @ xs the list to drop the elements from
  44 | public export
  45 | drop : (n : Nat) -> (xs : List a) -> List a
  46 | drop Z     xs      = xs
  47 | drop (S n) []      = []
  48 | drop (S n) (_::xs) = drop n xs
  49 |
  50 | ||| Satisfiable if `k` is a valid index into `xs`.
  51 | |||
  52 | ||| @ k  the potential index
  53 | ||| @ xs the list into which k may be an index
  54 | public export
  55 | data InBounds : (k : Nat) -> (xs : List a) -> Type where
  56 |     ||| Z is a valid index into any cons cell
  57 |     InFirst : InBounds Z (x :: xs)
  58 |     ||| Valid indices can be extended
  59 |     InLater : InBounds k xs -> InBounds (S k) (x :: xs)
  60 |
  61 | public export
  62 | Uninhabited (InBounds k []) where
  63 |   uninhabited InFirst impossible
  64 |   uninhabited (InLater _) impossible
  65 |
  66 | export
  67 | Uninhabited (InBounds k xs) => Uninhabited (InBounds (S k) (x::xs)) where
  68 |   uninhabited (InLater y) = uninhabited y
  69 |
  70 | ||| Decide whether `k` is a valid index into `xs`.
  71 | public export
  72 | inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)
  73 | inBounds _ [] = No uninhabited
  74 | inBounds Z (_ :: _) = Yes InFirst
  75 | inBounds (S k) (x :: xs) with (inBounds k xs)
  76 |   inBounds (S k) (x :: xs) | (Yes prf) = Yes (InLater prf)
  77 |   inBounds (S k) (x :: xs) | (No contra)
  78 |       = No $ \(InLater y) => contra y
  79 |
  80 | ||| Find a particular element of a list.
  81 | |||
  82 | ||| @ ok a proof that the index is within bounds
  83 | public export
  84 | index : (n : Nat) -> (xs : List a) -> {auto 0 ok : InBounds n xs} -> a
  85 | index Z (x :: xs) {ok = InFirst} = x
  86 | index (S k) (_ :: xs) {ok = InLater _} = index k xs
  87 |
  88 | public export
  89 | index' : (xs : List a) -> Fin (length xs) -> a
  90 | index' (x::_)  FZ     = x
  91 | index' (_::xs) (FS i) = index' xs i
  92 |
  93 | ||| Generate a list by repeatedly applying a partial function until exhausted.
  94 | ||| @ f the function to iterate
  95 | ||| @ x the initial value that will be the head of the list
  96 | covering
  97 | public export
  98 | iterate : (f : a -> Maybe a) -> (x : a) -> List a
  99 | iterate f x  = x :: case f x of
 100 |   Nothing => []
 101 |   Just y => iterate f y
 102 |
 103 | ||| Given a function `f` which extracts an element of `b` and `b`'s
 104 | ||| continuation, return the list consisting of the extracted elements.
 105 | ||| CAUTION: Only terminates if `f` eventually returns `Nothing`.
 106 | |||
 107 | ||| @ f  a function which provides an element of `b` and the rest of `b`
 108 | ||| @ b  a structure containing any number of elements
 109 | covering
 110 | public export
 111 | unfoldr : (f : b -> Maybe (a, b)) -> b -> List a
 112 | unfoldr f c = case f c of
 113 |   Nothing     => []
 114 |   Just (a, n) => a :: unfoldr f n
 115 |
 116 | ||| Returns the list of elements obtained by applying `f` to `x` `0` to `n-1` times,
 117 | ||| starting with `x`.
 118 | |||
 119 | ||| @ n  the number of times to iterate `f` over `x`
 120 | ||| @ f  a function producing a series
 121 | ||| @ x  the initial element of the series
 122 | public export
 123 | iterateN : (n : Nat) -> (f : a -> a) -> (x : a) -> List a
 124 | iterateN Z     _ _ = []
 125 | iterateN (S k) f x = x :: iterateN k f (f x)
 126 |
 127 | ||| Get the longest prefix of the list that satisfies the predicate.
 128 | |||
 129 | ||| @ p  a custom predicate for the elements of the list
 130 | ||| @ xs the list of elements
 131 | public export
 132 | takeWhile : (p : a -> Bool) -> (xs : List a) -> List a
 133 | takeWhile p []      = []
 134 | takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
 135 |
 136 | ||| Remove elements from the list until an element no longer satisfies the
 137 | ||| predicate.
 138 | |||
 139 | ||| @ p  a custom predicate for the elements of the list
 140 | ||| @ xs the list of elements to remove from
 141 | public export
 142 | dropWhile : (p : a -> Bool) -> (xs : List a) -> List a
 143 | dropWhile p []      = []
 144 | dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
 145 |
 146 | ||| Find the first element of the list that satisfies the predicate.
 147 | public export
 148 | find : (p : a -> Bool) -> (xs : List a) -> Maybe a
 149 | find p [] = Nothing
 150 | find p (x::xs) = if p x then Just x else find p xs
 151 |
 152 | ||| Find the index and proof of InBounds of the first element (if exists) of a
 153 | ||| list that satisfies the given test, else `Nothing`.
 154 | public export
 155 | findIndex : (a -> Bool) -> (xs : List a) -> Maybe $ Fin (length xs)
 156 | findIndex _ [] = Nothing
 157 | findIndex p (x :: xs) = if p x
 158 |   then Just FZ
 159 |   else FS <$> findIndex p xs
 160 |
 161 | ||| Find indices of all elements that satisfy the given test.
 162 | public export
 163 | findIndices : (a -> Bool) -> List a -> List Nat
 164 | findIndices p = h 0 where
 165 |   h : Nat -> List a -> List Nat
 166 |   h _         []  = []
 167 |   h lvl (x :: xs) = if p x
 168 |     then lvl :: h (S lvl) xs
 169 |     else        h (S lvl) xs
 170 |
 171 | ||| Find associated information in a list using a custom comparison.
 172 | public export
 173 | lookupBy : (a -> b -> Bool) -> a -> List (b, v) -> Maybe v
 174 | lookupBy p e []      = Nothing
 175 | lookupBy p e ((l, r) :: xs) =
 176 |   if p e l then
 177 |     Just r
 178 |   else
 179 |     lookupBy p e xs
 180 |
 181 | ||| Find associated information in a list using Boolean equality.
 182 | public export
 183 | lookup : Eq a => a -> List (a, b) -> Maybe b
 184 | lookup = lookupBy (==)
 185 |
 186 | ||| Remove duplicate elements from a list using a custom comparison. The general
 187 | ||| case of `nub`.
 188 | ||| O(n^2).
 189 | |||
 190 | ||| @ p  a custom comparison for detecting duplicate elements
 191 | ||| @ xs the list to remove the duplicates from
 192 | public export
 193 | nubBy : (p : a -> a -> Bool) -> (xs : List a) -> List a
 194 | nubBy = nubBy' []
 195 |   where
 196 |     nubBy' : List a -> (a -> a -> Bool) -> List a -> List a
 197 |     nubBy' acc p []      = []
 198 |     nubBy' acc p (x::xs) =
 199 |       if elemBy p x acc then
 200 |         nubBy' acc p xs
 201 |       else
 202 |         x :: nubBy' (x::acc) p xs
 203 |
 204 | ||| The nub function removes duplicate elements from a list using
 205 | ||| boolean equality. In particular, it keeps only the first occurrence of each
 206 | ||| element. It is a special case of `nubBy`, which allows the programmer to
 207 | ||| supply their own equality test.
 208 | ||| O(n^2).
 209 | |||
 210 | ||| ```idris example
 211 | ||| nub (the (List _) [1,2,1,3])
 212 | ||| ```
 213 | public export
 214 | nub : Eq a => List a -> List a
 215 | nub = nubBy (==)
 216 |
 217 | ||| Insert an element at a particular index.
 218 | |||
 219 | ||| ```idris example
 220 | ||| insertAt 1 [6, 8, 9] 7
 221 | ||| ```
 222 | |||
 223 | ||| @idx The index of the inserted value in the resulting list.
 224 | ||| @x The value to insert.
 225 | ||| @xs The list to insert the value into.
 226 | public export
 227 | insertAt : (idx : Nat) -> (x : a) -> (xs : List a) -> {auto 0 ok : idx `LTE` length xs} -> List a
 228 | insertAt Z x xs = x :: xs
 229 | insertAt {ok=LTESucc _} (S n) x (y :: ys) = y :: (insertAt n x ys)
 230 |
 231 | ||| Construct a new list consisting of all but the indicated element.
 232 | |||
 233 | ||| ```idris example
 234 | ||| deleteAt 3 [5, 6, 7, 8, 9]
 235 | ||| ```
 236 | |||
 237 | ||| @ idx The index of the value to delete.
 238 | ||| @ xs The list to delete the value from.
 239 | public export
 240 | deleteAt : (idx : Nat) -> (xs : List a) -> {auto 0 prf : InBounds idx xs} -> List a
 241 | deleteAt {prf=InFirst} Z (_ :: xs) = xs
 242 | deleteAt {prf=InLater _} (S k) (x :: xs) = x :: deleteAt k xs
 243 |
 244 | ||| The deleteBy function behaves like delete, but takes a user-supplied equality predicate.
 245 | public export
 246 | deleteBy : (a -> b -> Bool) -> a -> List b -> List b
 247 | deleteBy _  _ []      = []
 248 | deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys
 249 |
 250 | ||| `delete x` removes the first occurrence of `x` from its list argument. For
 251 | ||| example,
 252 | |||
 253 | |||````idris example
 254 | |||delete 'a' ['b', 'a', 'n', 'a', 'n', 'a']
 255 | |||````
 256 | |||
 257 | ||| It is a special case of deleteBy, which allows the programmer to supply
 258 | ||| their own equality test.
 259 | public export
 260 | delete : Eq a => a -> List a -> List a
 261 | delete = deleteBy (==)
 262 |
 263 | ||| Delete the first occurrence of each element from the second list in the first
 264 | ||| list where equality is determined by the predicate passed as the first argument.
 265 | ||| @ p            A function that returns true when its two arguments should be considered equal.
 266 | ||| @ source       The list to delete elements from.
 267 | ||| @ undesirables The list of elements to delete.
 268 | public export
 269 | deleteFirstsBy : (p : a -> b -> Bool) -> (source : List b) -> (undesirables : List a) -> List b
 270 | deleteFirstsBy p = foldl (flip (deleteBy p))
 271 |
 272 | export infix 7 \\
 273 |
 274 | ||| The non-associative list-difference.
 275 | ||| A specialized form of @deleteFirstsBy@ where the predicate is equality under the @Eq@
 276 | ||| interface.
 277 | ||| Deletes the first occurrence of each element of the second list from the first list.
 278 | |||
 279 | ||| In the following example, the result is `[2, 4]`.
 280 | ||| ```idris example
 281 | ||| [1, 2, 3, 4] \\ [1, 3]
 282 | ||| ```
 283 | |||
 284 | public export
 285 | (\\) : Eq a => List a -> List a -> List a
 286 | (\\) = foldl (flip delete)
 287 |
 288 | ||| The unionBy function returns the union of two lists by user-supplied equality predicate.
 289 | public export
 290 | unionBy : (a -> a -> Bool) -> List a -> List a -> List a
 291 | unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
 292 |
 293 | ||| Compute the union of two lists according to their `Eq` implementation.
 294 | |||
 295 | ||| ```idris example
 296 | ||| union ['d', 'o', 'g'] ['c', 'o', 'w']
 297 | ||| ```
 298 | |||
 299 | public export
 300 | union : Eq a => List a -> List a -> List a
 301 | union = unionBy (==)
 302 |
 303 | ||| Like @span@ but using a predicate that might convert a to b, i.e. given a
 304 | ||| predicate from a to Maybe b and a list of as, returns a tuple consisting of
 305 | ||| the longest prefix of the list where a -> Just b, and the rest of the list.
 306 | public export
 307 | spanBy : (a -> Maybe b) -> List a -> (List b, List a)
 308 | spanBy p [] = ([], [])
 309 | spanBy p (x :: xs) = case p x of
 310 |   Nothing => ([], x :: xs)
 311 |   Just y => let (ys, zs) = spanBy p xs in (y :: ys, zs)
 312 |
 313 | ||| Given a predicate and a list, returns a tuple consisting of the longest
 314 | ||| prefix of the list whose elements satisfy the predicate, and the rest of the
 315 | ||| list.
 316 | public export
 317 | span : (a -> Bool) -> List a -> (List a, List a)
 318 | span p []      = ([], [])
 319 | span p (x::xs) =
 320 |   if p x then
 321 |     let (ys, zs) = span p xs in
 322 |         (x::ys, zs)
 323 |   else
 324 |     ([], x::xs)
 325 |
 326 | ||| Similar to `span` but negates the predicate, i.e.: returns a tuple
 327 | ||| consisting of the longest prefix of the list whose elements don't satisfy
 328 | ||| the predicate, and the rest of the list.
 329 | public export
 330 | break : (a -> Bool) -> List a -> (List a, List a)
 331 | break p xs = span (not . p) xs
 332 |
 333 | public export
 334 | singleton : a -> List a
 335 | singleton x = [x]
 336 |
 337 | public export
 338 | split : (a -> Bool) -> List a -> List1 (List a)
 339 | split p xs =
 340 |   case break p xs of
 341 |     (chunk, [])          => singleton chunk
 342 |     (chunk, (c :: rest)) => chunk ::: forget (split p (assert_smaller xs rest))
 343 |
 344 | ||| Split the list `xs` at the index `n`. If `n > length xs`, returns a tuple
 345 | ||| consisting of `xs` and `[]`.
 346 | |||
 347 | ||| @ n  the index to split the list at
 348 | ||| @ xs the list to split
 349 | public export
 350 | splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
 351 | splitAt Z xs = ([], xs)
 352 | splitAt (S k) [] = ([], [])
 353 | splitAt (S k) (x :: xs)
 354 |       = let (tk, dr) = splitAt k xs in
 355 |             (x :: tk, dr)
 356 |
 357 | ||| Divide the list into a tuple containing two smaller lists: one with the
 358 | ||| elements that satisfies the given predicate and another with the elements
 359 | ||| that don't.
 360 | |||
 361 | ||| @ p  the predicate to partition according to
 362 | ||| @ xs the list to partition
 363 | public export
 364 | partition : (p : a -> Bool) -> (xs : List a) -> (List a, List a)
 365 | partition p []      = ([], [])
 366 | partition p (x::xs) =
 367 |   let (lefts, rights) = partition p xs in
 368 |     if p x then
 369 |       (x::lefts, rights)
 370 |     else
 371 |       (lefts, x::rights)
 372 |
 373 | ||| The inits function returns all initial segments of the argument, shortest
 374 | ||| first. For example,
 375 | |||
 376 | ||| ```idris example
 377 | ||| inits [1,2,3]
 378 | ||| ```
 379 | public export
 380 | inits : List a -> List (List a)
 381 | inits xs = [] :: case xs of
 382 |   []        => []
 383 |   x :: xs'  => map (x ::) (inits xs')
 384 |
 385 | ||| The tails function returns all final segments of the argument, longest
 386 | ||| first. For example,
 387 | |||
 388 | ||| ```idris example
 389 | ||| tails [1,2,3] == [[1,2,3], [2,3], [3], []]
 390 | |||```
 391 | public export
 392 | tails : List a -> List (List a)
 393 | tails xs = xs :: case xs of
 394 |   []        => []
 395 |   _ :: xs'  => tails xs'
 396 |
 397 | ||| Split on the given element.
 398 | |||
 399 | ||| ```idris example
 400 | ||| splitOn 0 [1,0,2,0,0,3]
 401 | ||| ```
 402 | |||
 403 | public export
 404 | splitOn : Eq a => a -> List a -> List1 (List a)
 405 | splitOn a = split (== a)
 406 |
 407 | ||| Replace an element at a particular index with another.
 408 | |||
 409 | ||| ```idris example
 410 | ||| replaceAt 2 6 [1, 2, 3, 4]
 411 | ||| ```
 412 | |||
 413 | ||| @idx The index of the value to replace.
 414 | ||| @x The value to insert.
 415 | ||| @xs The list in which to replace an element.
 416 | public export
 417 | replaceAt : (idx : Nat) -> a -> (xs : List a) -> {auto 0 ok : InBounds idx xs} -> List a
 418 | replaceAt Z y (_ :: xs) {ok=InFirst} = y :: xs
 419 | replaceAt (S k) y (x :: xs) {ok=InLater _} = x :: replaceAt k y xs
 420 |
 421 | ||| Replace the elements in the list that satisfy the predicate with the given
 422 | ||| value. The general case of `replaceOn`.
 423 | |||
 424 | ||| @ p  the predicate to replace elements in the list according to
 425 | ||| @ b  the element to replace with
 426 | ||| @ l  the list to perform the replacements on
 427 | public export
 428 | replaceWhen : (p : a -> Bool) -> (b : a) -> (l : List a) -> List a
 429 | replaceWhen p b l = map (\c => if p c then b else c) l
 430 |
 431 | ||| Replace the elements in the list that are equal to `e`, using boolean
 432 | ||| equality, with `b`. A special case of `replaceWhen`, using `== e` as the
 433 | ||| predicate.
 434 | |||
 435 | ||| ```idris example
 436 | ||| > replaceOn '-' ',' ['1', '-', '2', '-', '3']
 437 | ||| ['1', ',', '2', ',', '3']
 438 | ||| ```
 439 | |||
 440 | ||| @ e  the element to find and replace
 441 | ||| @ b  the element to replace with
 442 | ||| @ l  the list to perform the replacements on
 443 | public export
 444 | replaceOn : Eq a => (e : a) -> (b : a) -> (l : List a) -> List a
 445 | replaceOn e = replaceWhen (== e)
 446 |
 447 | replicateTR : List a -> Nat -> a -> List a
 448 | replicateTR as Z     _ = as
 449 | replicateTR as (S n) x = replicateTR (x :: as) n x
 450 |
 451 | ||| Construct a list with `n` copies of `x`.
 452 | |||
 453 | ||| @ n how many copies
 454 | ||| @ x the element to replicate
 455 | public export
 456 | replicate : (n : Nat) -> (x : a) -> List a
 457 | replicate Z     _ = []
 458 | replicate (S n) x = x :: replicate n x
 459 |
 460 | -- Data.List.replicateTRIsReplicate proves these are equivalent.
 461 | %transform "tailRecReplicate" List.replicate = List.replicateTR Nil
 462 |
 463 |
 464 | ||| Compute the intersect of two lists by user-supplied equality predicate.
 465 | export
 466 | intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
 467 | intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]
 468 |
 469 | ||| Compute the intersection of two lists according to the `Eq` implementation for
 470 | ||| the elements.
 471 | export
 472 | intersect : Eq a => List a -> List a -> List a
 473 | intersect = intersectBy (==)
 474 |
 475 | ||| Compute the intersect of all the lists in the given list of lists, according
 476 | ||| to the user-supplied equality predicate.
 477 | |||
 478 | ||| @ eq the predicate for computing the intersection
 479 | ||| @ ls the list of lists to compute the intersect of
 480 | export
 481 | intersectAllBy : (eq : a -> a -> Bool) -> (ls : List (List a)) -> List a
 482 | intersectAllBy eq [] = []
 483 | intersectAllBy eq (xs :: xss) = filter (\x => all (elemBy eq x) xss) xs
 484 |
 485 | ||| Compute the intersect of all the lists in the given list of lists, according
 486 | ||| to boolean equality. A special case of `intersectAllBy`, using `==` as the
 487 | ||| equality predicate.
 488 | |||
 489 | ||| @ ls the list of lists to compute the intersect of
 490 | export
 491 | intersectAll : Eq a => (ls : List (List a)) -> List a
 492 | intersectAll = intersectAllBy (==)
 493 |
 494 | ---------------------------
 495 | -- Zippable --
 496 | ---------------------------
 497 |
 498 | public export
 499 | Zippable List where
 500 |   zipWith _ [] _ = []
 501 |   zipWith _ _ [] = []
 502 |   zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
 503 |
 504 |   zipWith3 _ [] _ _ = []
 505 |   zipWith3 _ _ [] _ = []
 506 |   zipWith3 _ _ _ [] = []
 507 |   zipWith3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: zipWith3 f xs ys zs
 508 |
 509 |   unzipWith f [] = ([], [])
 510 |   unzipWith f (x :: xs) = let (b, c) = f x
 511 |                               (bs, cs) = unzipWith f xs in
 512 |                               (b :: bs, c :: cs)
 513 |
 514 |   unzipWith3 f [] = ([], [], [])
 515 |   unzipWith3 f (x :: xs) = let (b, c, d) = f x
 516 |                                (bs, cs, ds) = unzipWith3 f xs in
 517 |                                (b :: bs, c :: cs, d :: ds)
 518 |
 519 | ---------------------------
 520 | -- Non-empty List
 521 | ---------------------------
 522 |
 523 | ||| Proof that a given list is non-empty.
 524 | public export
 525 | data NonEmpty : (xs : List a) -> Type where
 526 |     IsNonEmpty : NonEmpty (x :: xs)
 527 |
 528 | -- The empty list (Nil) cannot be `NonEmpty`.
 529 | export
 530 | Uninhabited (NonEmpty []) where
 531 |   uninhabited IsNonEmpty impossible
 532 |
 533 | ||| Get the head of a non-empty list.
 534 | ||| @ ok proof the list is non-empty
 535 | public export
 536 | head : (l : List a) -> {auto 0 ok : NonEmpty l} -> a
 537 | head [] impossible
 538 | head (x :: _) = x
 539 |
 540 | ||| Get the tail of a non-empty list.
 541 | ||| @ ok proof the list is non-empty
 542 | public export
 543 | tail : (l : List a) -> {auto 0 ok : NonEmpty l} -> List a
 544 | tail [] impossible
 545 | tail (_ :: xs) = xs
 546 |
 547 | ||| Retrieve the last element of a non-empty list.
 548 | ||| @ ok proof that the list is non-empty
 549 | public export
 550 | last : (l : List a) -> {auto 0 ok : NonEmpty l} -> a
 551 | last [] impossible
 552 | last [x] = x
 553 | last (x :: xs@(_::_)) = last xs
 554 |
 555 | ||| Return all but the last element of a non-empty list.
 556 | ||| @ ok proof the list is non-empty
 557 | public export
 558 | init : (l : List a) -> {auto 0 ok : NonEmpty l} -> List a
 559 | init [] impossible
 560 | init [x] = []
 561 | init (x :: xs@(_::_)) = x :: init xs
 562 |
 563 | ||| Computes the minimum of a non-empty list
 564 | public export
 565 | minimum : Ord a => (xs : List a) -> {auto 0 _ : NonEmpty xs} -> a
 566 | minimum (x :: xs) = foldl min x xs
 567 |
 568 | ||| Attempt to deconstruct the list into a head and a tail.
 569 | public export
 570 | uncons' : List a -> Maybe (a, List a)
 571 | uncons' []        = Nothing
 572 | uncons' (x :: xs) = Just (x, xs)
 573 |
 574 | ||| Attempt to get the head of a list. If the list is empty, return `Nothing`.
 575 | public export
 576 | head' : List a -> Maybe a
 577 | head' = map fst . uncons'
 578 |
 579 | ||| Attempt to get the tail of a list. If the list is empty, return `Nothing`.
 580 | export
 581 | tail' : List a -> Maybe (List a)
 582 | tail' = map snd . uncons'
 583 |
 584 | ||| Attempt to retrieve the last element of a non-empty list.
 585 | |||
 586 | ||| If the list is empty, return `Nothing`.
 587 | export
 588 | last' : List a -> Maybe a
 589 | last' [] = Nothing
 590 | last' xs@(_::_) = Just (last xs)
 591 |
 592 | ||| Attempt to return all but the last element of a non-empty list.
 593 | |||
 594 | ||| If the list is empty, return `Nothing`.
 595 | export
 596 | init' : List a -> Maybe (List a)
 597 | init' [] = Nothing
 598 | init' xs@(_::_) = Just (init xs)
 599 |
 600 | ||| Foldr a non-empty list, using `map` to transform the first accumulated
 601 | ||| element to something of the desired type and `func` to accumulate the
 602 | ||| elements.
 603 | |||
 604 | ||| @ func the function used to accumulate the elements
 605 | ||| @ map  an initial transformation from the element to the accumulated type
 606 | ||| @ l    the non-empty list to foldr
 607 | ||| @ ok   proof that the list is non-empty
 608 | public export
 609 | foldr1By : (func : a -> b -> b) -> (map : a -> b) ->
 610 |            (l : List a) -> {auto 0 ok : NonEmpty l} -> b
 611 | foldr1By f map [] impossible
 612 | foldr1By f map [x] = map x
 613 | foldr1By f map (x :: xs@(_::_)) = f x (foldr1By f map xs)
 614 |
 615 | ||| Foldl a non-empty list, using `map` to transform the first accumulated
 616 | ||| element to something of the desired type and `func` to accumulate the
 617 | ||| elements.
 618 | |||
 619 | ||| @ func the function used to accumulate the elements
 620 | ||| @ map  an initial transformation from the element to the accumulated type
 621 | ||| @ l    the non-empty list to foldl
 622 | ||| @ ok   proof that the list is non-empty
 623 | public export
 624 | foldl1By : (func : b -> a -> b) -> (map : a -> b) ->
 625 |            (l : List a) -> {auto 0 ok : NonEmpty l} -> b
 626 | foldl1By f map [] impossible
 627 | foldl1By f map (x::xs) = foldl f (map x) xs
 628 |
 629 | ||| Foldr a non-empty list without seeding the accumulator.
 630 | |||
 631 | ||| @ ok proof that the list is non-empty
 632 | public export
 633 | foldr1 : (a -> a -> a) -> (l : List a) -> {auto 0 ok : NonEmpty l} -> a
 634 | foldr1 f xs = foldr1By f id xs
 635 |
 636 | ||| Foldl a non-empty list without seeding the accumulator.
 637 | |||
 638 | ||| @ ok proof that the list is non-empty
 639 | public export
 640 | foldl1 : (a -> a -> a) -> (l : List a) -> {auto 0 ok : NonEmpty l} -> a
 641 | foldl1 f xs = foldl1By f id xs
 642 |
 643 | ||| Convert to a non-empty list.
 644 | |||
 645 | ||| @ ok proof the list is non-empty
 646 | export
 647 | toList1 : (l : List a) -> {auto 0 ok : NonEmpty l} -> List1 a
 648 | toList1 [] impossible
 649 | toList1 (x :: xs) = x ::: xs
 650 |
 651 | ||| Convert to a non-empty list, returning Nothing if the list is empty.
 652 | public export
 653 | toList1' : (l : List a) -> Maybe (List1 a)
 654 | toList1' [] = Nothing
 655 | toList1' (x :: xs) = Just (x ::: xs)
 656 |
 657 | ||| Interleave two lists.
 658 | ||| ```idris example
 659 | ||| > interleave ["a", "c", "e"]  ["b", "d", "f"]
 660 | ||| ["a", "b", "c", "d", "e", "f"]
 661 | ||| ```
 662 | public export
 663 | interleave : (xs, ys : List a) -> List a
 664 | interleave [] ys = ys
 665 | interleave (x :: xs) ys = x :: interleave ys xs
 666 |
 667 | ||| Prefix every element in the list with the given element.
 668 | |||
 669 | ||| @ sep the value to prefix
 670 | ||| @ xs  the list of elements to prefix with the given element
 671 | |||
 672 | ||| ```idris example
 673 | ||| > with List (mergeReplicate '>' ['a', 'b', 'c', 'd', 'e'])
 674 | ||| ['>', 'a', '>', 'b', '>', 'c', '>', 'd', '>', 'e']
 675 | ||| ```
 676 | public export
 677 | mergeReplicate : (sep : a) -> (xs : List a) -> List a
 678 | mergeReplicate sep []      = []
 679 | mergeReplicate sep (y::ys) = sep :: y :: mergeReplicate sep ys
 680 |
 681 | ||| Insert some separator between the elements of a list.
 682 | |||
 683 | ||| @ sep the value to intersperse
 684 | ||| @ xs  the list of elements to intersperse with the separator
 685 | |||
 686 | ||| ```idris example
 687 | ||| > with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
 688 | ||| ['a', ',', 'b', ',', 'c', ',', 'd', ',', 'e']
 689 | ||| ```
 690 | public export
 691 | intersperse : (sep : a) -> (xs : List a) -> List a
 692 | intersperse sep []      = []
 693 | intersperse sep (x::xs) = x :: mergeReplicate sep xs
 694 |
 695 | ||| Given a separator list and some more lists, produce a new list by
 696 | ||| placing the separator between each of the lists.
 697 | |||
 698 | ||| @ sep the separator
 699 | ||| @ xss the lists between which the separator will be placed
 700 | |||
 701 | ||| ```idris example
 702 | ||| intercalate [0, 0, 0] [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ]
 703 | ||| ```
 704 | export
 705 | intercalate : (sep : List a) -> (xss : List (List a)) -> List a
 706 | intercalate sep xss = concat $ intersperse sep xss
 707 |
 708 | ||| Extract all of the values contained in a List of Maybes
 709 | public export
 710 | catMaybes : List (Maybe a) -> List a
 711 | catMaybes = mapMaybe id
 712 |
 713 | --------------------------------------------------------------------------------
 714 | -- Sorting
 715 | --------------------------------------------------------------------------------
 716 |
 717 | ||| Check whether a list is sorted with respect to the default ordering for the type of its elements.
 718 | export
 719 | sorted : Ord a => List a -> Bool
 720 | sorted (x :: xs @ (y :: _)) = x <= y && sorted xs
 721 | sorted _ = True
 722 |
 723 | ||| Merge two sorted lists using an arbitrary comparison
 724 | ||| predicate. Note that the lists must have been sorted using this
 725 | ||| predicate already.
 726 | export
 727 | mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
 728 | mergeBy order []      right   = right
 729 | mergeBy order left    []      = left
 730 | mergeBy order (x::xs) (y::ys) =
 731 |   -- The code below will emit `y` before `x` whenever `x == y`.
 732 |   -- If you change this, `sortBy` will stop being stable, unless you fix `sortBy`, too.
 733 |   case order x y of
 734 |        LT => x :: mergeBy order xs (y::ys)
 735 |        _  => y :: mergeBy order (x::xs) ys
 736 |
 737 | ||| Merge two sorted lists using the default ordering for the type of their elements.
 738 | export
 739 | merge : Ord a => List a -> List a -> List a
 740 | merge left right = mergeBy compare left right
 741 |
 742 | ||| Sort a list using some arbitrary comparison predicate.
 743 | |||
 744 | ||| @ cmp how to compare elements
 745 | ||| @ xs the list to sort
 746 | export
 747 | sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
 748 | sortBy cmp []  = []
 749 | sortBy cmp [x] = [x]
 750 | sortBy cmp xs  = let (x, y) = split xs in
 751 |     mergeBy cmp
 752 |           (sortBy cmp (assert_smaller xs x))
 753 |           (sortBy cmp (assert_smaller xs y)) -- not structurally smaller, hence assert
 754 |   where
 755 |     splitRec : List b -> List a -> (List a -> List a) -> (List a, List a)
 756 |     splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))
 757 |     splitRec _          ys      zs = (ys, zs [])
 758 |     -- In the above base-case clause, we put `ys` on the LHS to get a stable sort.
 759 |     -- This is because `mergeBy` prefers taking elements from its RHS operand
 760 |     -- if both heads are equal, and all elements in `zs []` precede all elements of `ys`
 761 |     -- in the original list.
 762 |
 763 |     split : List a -> (List a, List a)
 764 |     split xs = splitRec xs xs id
 765 |
 766 | ||| Sort a list using the default ordering for the type of its elements.
 767 | export
 768 | sort : Ord a => List a -> List a
 769 | sort = sortBy compare
 770 |
 771 | ||| Check whether the `left` list is a prefix of the `right` one, according to
 772 | ||| `match`. Returns the matched prefix together with the leftover suffix.
 773 | |||
 774 | ||| @ match a custom matching function for checking the elements are convertible
 775 | ||| @ left  the list which might be a prefix of `right`
 776 | ||| @ right the list of elements to compare against
 777 | public export
 778 | prefixOfBy : (match : a -> b -> Maybe m) ->
 779 |              (left : List a) -> (right : List b) ->
 780 |              Maybe (List m, List b)
 781 | prefixOfBy p = go [<] where
 782 |   go : SnocList m -> List a -> List b -> Maybe (List m, List b)
 783 |   go sm [] bs = pure (sm <>> [], bs)
 784 |   go sm as [] = Nothing
 785 |   go sm (a :: as) (b :: bs) = go (sm :< !(p a b)) as bs
 786 |
 787 | ||| Check whether the `left` list is a prefix of the `right` one, using the
 788 | ||| provided equality function to compare elements.
 789 | |||
 790 | ||| @ eq    a custom equality function for comparing the elements
 791 | ||| @ left  the list which might be a prefix of `right`
 792 | ||| @ right the list of elements to compare against
 793 | public export
 794 | isPrefixOfBy : (eq : a -> b -> Bool) ->
 795 |                (left : List a) -> (right : List b) -> Bool
 796 | isPrefixOfBy p [] _            = True
 797 | isPrefixOfBy p _ []            = False
 798 | isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
 799 |
 800 | ||| The isPrefixOf function takes two lists and returns True iff the first list
 801 | ||| is a prefix of the second when comparing elements using `==`.
 802 | public export
 803 | isPrefixOf : Eq a => List a -> List a -> Bool
 804 | isPrefixOf = isPrefixOfBy (==)
 805 |
 806 | ||| Check whether the `left` is a suffix of the `right` one, according to
 807 | ||| `match`. Returns the matched suffix together with the leftover prefix.
 808 | |||
 809 | ||| @ match a custom matching function for checking the elements are convertible
 810 | ||| @ left  the list which might be a prefix of `right`
 811 | ||| @ right the list of elements to compare against
 812 | public export
 813 | suffixOfBy : (match : a -> b -> Maybe m) ->
 814 |              (left : List a) -> (right : List b) ->
 815 |              Maybe (List b, List m)
 816 | suffixOfBy match left right
 817 |   = do (ms, bs) <- prefixOfBy match (reverse left) (reverse right)
 818 |        pure (reverse bs, reverse ms)
 819 |
 820 | ||| Check whether the `left` is a suffix of the `right` one, using the provided
 821 | ||| equality function to compare elements.
 822 | |||
 823 | ||| @ eq    a custom equality function for comparing the elements
 824 | ||| @ left  the list which might be a suffix of `right`
 825 | ||| @ right the list of elements to compare againts
 826 | public export
 827 | isSuffixOfBy : (eq : a -> b -> Bool) ->
 828 |                (left : List a) -> (right : List b) -> Bool
 829 | isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
 830 |
 831 | ||| The isSuffixOf function takes two lists and returns True iff the first list
 832 | ||| is a suffix of the second when comparing elements using `==`.
 833 | public export
 834 | isSuffixOf : Eq a => List a -> List a -> Bool
 835 | isSuffixOf = isSuffixOfBy (==)
 836 |
 837 | ||| Check whether the `left` list is an infix of the `right` one, according to
 838 | ||| `match`. Returns the shortest unmatched prefix, matched infix and the leftover suffix.
 839 | public export
 840 | infixOfBy : (match : a -> b -> Maybe m) ->
 841 |             (left : List a) -> (right : List b) ->
 842 |             Maybe (List b, List m, List b)
 843 | infixOfBy _ []          right = Just ([], [], right)
 844 | infixOfBy p left@(_::_) right = go [<] right where
 845 |   go : (acc : SnocList b) -> List b -> Maybe (List b, List m, List b)
 846 |   go _   []             = Nothing
 847 |   go pre curr@(c::rest) = case prefixOfBy p left curr of
 848 |     Just (inf, post) => Just (pre <>> [], inf, post)
 849 |     Nothing          => go (pre:<c) rest
 850 |
 851 | ||| Check whether the `left` is an infix of the `right` one, using the provided
 852 | ||| equality function to compare elements.
 853 | public export
 854 | isInfixOfBy : (eq : a -> b -> Bool) ->
 855 |               (left : List a) -> (right : List b) -> Bool
 856 | isInfixOfBy p n h = any (isPrefixOfBy p n) (tails h)
 857 |
 858 | ||| The isInfixOf function takes two lists and returns True iff the first list
 859 | ||| is contained, wholly and intact, anywhere within the second.
 860 | |||
 861 | ||| ```idris example
 862 | ||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']
 863 | ||| ```
 864 | ||| ```idris example
 865 | ||| isInfixOf ['b','d'] ['a', 'b', 'c', 'd']
 866 | ||| ```
 867 | |||
 868 | public export
 869 | isInfixOf : Eq a => List a -> List a -> Bool
 870 | isInfixOf = isInfixOfBy (==)
 871 |
 872 | ||| Transposes rows and columns of a list of lists.
 873 | |||
 874 | ||| ```idris example
 875 | ||| with List transpose [[1, 2], [3, 4]]
 876 | ||| ```
 877 | |||
 878 | ||| This also works for non square scenarios, thus
 879 | ||| involution does not always hold:
 880 | |||
 881 | |||     transpose [[], [1, 2]] = [[1], [2]]
 882 | |||     transpose (transpose [[], [1, 2]]) = [[1, 2]]
 883 | export
 884 | transpose : List (List a) -> List (List a)
 885 | transpose [] = []
 886 | transpose (heads :: tails) = spreadHeads heads (transpose tails) where
 887 |   spreadHeads : List a -> List (List a) -> List (List a)
 888 |   spreadHeads []              tails           = tails
 889 |   spreadHeads (head :: heads) []              = [head] :: spreadHeads heads []
 890 |   spreadHeads (head :: heads) (tail :: tails) = (head :: tail) :: spreadHeads heads tails
 891 |
 892 | ------------------------------------------------------------------------
 893 | -- Grouping
 894 | ------------------------------------------------------------------------
 895 |
 896 | ||| `groupBy` operates like `group`, but uses the provided equality
 897 | ||| predicate instead of `==`.
 898 | public export
 899 | groupBy : (a -> a -> Bool) -> List a -> List (List1 a)
 900 | groupBy _ [] = []
 901 | groupBy eq (h :: t) = let (ys,zs) = go h t
 902 |                        in ys :: zs
 903 |
 904 |   where go : a -> List a -> (List1 a, List (List1 a))
 905 |         go v [] = (singleton v,[])
 906 |         go v (x :: xs) = let (ys,zs) = go x xs
 907 |                           in if eq v x
 908 |                                 then (cons v ys, zs)
 909 |                                 else (singleton v, ys :: zs)
 910 |
 911 | ||| The `group` function takes a list of values and returns a list of
 912 | ||| lists such that flattening the resulting list is equal to the
 913 | ||| argument.  Moreover, each list in the resulting list
 914 | ||| contains only equal elements.
 915 | public export
 916 | group : Eq a => List a -> List (List1 a)
 917 | group = groupBy (==)
 918 |
 919 | ||| `groupWith` operates like `group`, but uses the provided projection when
 920 | ||| comparing for equality
 921 | public export
 922 | groupWith : Eq b => (a -> b) -> List a -> List (List1 a)
 923 | groupWith f = groupBy (\x,y => f x == f y)
 924 |
 925 | ||| `groupAllWith` operates like `groupWith`, but sorts the list
 926 | ||| first so that each equivalence class has, at most, one list in the
 927 | ||| output
 928 | public export
 929 | groupAllWith : Ord b => (a -> b) -> List a -> List (List1 a)
 930 | groupAllWith f = groupWith f . sortBy (comparing f)
 931 |
 932 | ||| Partitions a list into fixed sized sublists.
 933 | |||
 934 | ||| Note: The last list in the result might be shorter than the rest if
 935 | |||       the input cannot evenly be split into groups of the same size.
 936 | |||
 937 | ||| ```idris example
 938 | ||| grouped 3 [1..10] === [[1,2,3],[4,5,6],[7,8,9],[10]]
 939 | ||| ```
 940 | public export
 941 | grouped : (n : Nat) -> {auto 0 p : IsSucc n} -> List a -> List (List a)
 942 | grouped _     []      = []
 943 | grouped (S m) (x::xs) = go [<] [<x] m xs
 944 |   where
 945 |     go : SnocList (List a) -> SnocList a -> Nat -> List a -> List (List a)
 946 |     go sxs sx c     []        = sxs <>> [sx <>> []]
 947 |     go sxs sx 0     (x :: xs) = go (sxs :< (sx <>> [])) [<x] m xs
 948 |     go sxs sx (S k) (x :: xs) = go sxs (sx :< x) k xs
 949 |
 950 | --------------------------------------------------------------------------------
 951 | -- Properties
 952 | --------------------------------------------------------------------------------
 953 |
 954 | -- Nil is not Cons
 955 | export
 956 | Uninhabited ([] = x :: xs) where
 957 |   uninhabited Refl impossible
 958 |
 959 | -- Cons is not Nil
 960 | export
 961 | Uninhabited (x :: xs = []) where
 962 |   uninhabited Refl impossible
 963 |
 964 | -- If the heads or the tails of two lists are provably non-equal, then the
 965 | -- combination of the respective heads with their respective tails must be
 966 | -- provably non-equal.
 967 | export
 968 | {0 xs : List a} -> Either (Uninhabited $ x === y) (Uninhabited $ xs === ys) => Uninhabited (x::xs = y::ys) where
 969 |   uninhabited @{Left  z} Refl = uninhabited @{z} Refl
 970 |   uninhabited @{Right z} Refl = uninhabited @{z} Refl
 971 |
 972 | ||| (::) is injective
 973 | export
 974 | Biinjective Prelude.(::) where
 975 |   biinjective Refl = (Refl, Refl)
 976 |
 977 | ||| Heterogeneous injectivity for (::)
 978 | export
 979 | consInjective : forall x, xs, y, ys .
 980 |                 the (List a) (x :: xs) = the (List b) (y :: ys) -> (x = y, xs = ys)
 981 | consInjective Refl = (Refl, Refl)
 982 |
 983 | lengthPlusIsLengthPlus : (n : Nat) -> (xs : List a) ->
 984 |                          lengthPlus n xs = n + length xs
 985 | lengthPlusIsLengthPlus n [] = sym $ plusZeroRightNeutral n
 986 | lengthPlusIsLengthPlus n (x::xs) =
 987 |   trans
 988 |   (lengthPlusIsLengthPlus (S n) xs)
 989 |   (plusSuccRightSucc n (length xs))
 990 |
 991 | lengthTRIsLength : (xs : List a) -> lengthTR xs = length xs
 992 | lengthTRIsLength = lengthPlusIsLengthPlus Z
 993 |
 994 | ||| List `reverse` applied to `reverseOnto` is equivalent to swapping the
 995 | ||| arguments of `reverseOnto`.
 996 | reverseReverseOnto : (l, r : List a) ->
 997 |                      reverse (reverseOnto l r) = reverseOnto r l
 998 | reverseReverseOnto _ [] = Refl
 999 | reverseReverseOnto l (x :: xs) = reverseReverseOnto (x :: l) xs
1000 |
1001 | ||| List `reverse` applied twice yields the identity function.
1002 | export
1003 | reverseInvolutive : (xs : List a) -> reverse (reverse xs) = xs
1004 | reverseInvolutive = reverseReverseOnto []
1005 |
1006 | ||| Appending `x` to `l` and then reversing the result onto `r` is the same as
1007 | ||| using (::) with `x` and the result of reversing `l` onto `r`.
1008 | consReverse : (x : a) -> (l, r : List a) ->
1009 |               x :: reverseOnto r l = reverseOnto r (reverseOnto [x] (reverse l))
1010 | consReverse _ [] _ = Refl
1011 | consReverse x (y::ys) r
1012 |   = rewrite consReverse x ys (y :: r) in
1013 |       rewrite cong (reverseOnto r . reverse) $ consReverse x ys [y] in
1014 |         rewrite reverseInvolutive (y :: reverseOnto [x] (reverse ys)) in
1015 |           Refl
1016 |
1017 | ||| Proof that it is safe to lift a (::) out of the first `tailRecAppend`
1018 | ||| argument.
1019 | consTailRecAppend : (x : a) -> (l, r : List a) ->
1020 |                     tailRecAppend (x :: l) r = x :: (tailRecAppend l r)
1021 | consTailRecAppend x l r
1022 |   = rewrite consReverse x (reverse l) r in
1023 |       rewrite reverseInvolutive l in
1024 |         Refl
1025 |
1026 | ||| Proof that `(++)` and `tailRecAppend` do the same thing, so the %transform
1027 | ||| directive is safe.
1028 | tailRecAppendIsAppend : (xs, ys : List a) -> tailRecAppend xs ys = xs ++ ys
1029 | tailRecAppendIsAppend [] ys = Refl
1030 | tailRecAppendIsAppend (x::xs) ys =
1031 |   trans (consTailRecAppend x xs ys) (cong (x ::) $ tailRecAppendIsAppend xs ys)
1032 |
1033 | ||| The empty list is a right identity for append.
1034 | export
1035 | appendNilRightNeutral : (l : List a) -> l ++ [] = l
1036 | appendNilRightNeutral []      = Refl
1037 | appendNilRightNeutral (_::xs) = rewrite appendNilRightNeutral xs in Refl
1038 |
1039 | ||| Appending lists is associative.
1040 | export
1041 | appendAssociative : (l, c, r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r
1042 | appendAssociative []      c r = Refl
1043 | appendAssociative (_::xs) c r = rewrite appendAssociative xs c r in Refl
1044 |
1045 | ||| `reverseOnto` reverses the list and prepends it to the "onto" argument
1046 | revOnto : (xs, vs : List a) -> reverseOnto xs vs = reverse vs ++ xs
1047 | revOnto _ [] = Refl
1048 | revOnto xs (v :: vs)
1049 |     = rewrite revOnto (v :: xs) vs in
1050 |         rewrite appendAssociative (reverse vs) [v] xs in
1051 |                                   rewrite revOnto [v] vs in Refl
1052 |
1053 | ||| `reverse` is distributive
1054 | export
1055 | revAppend : (vs, ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)
1056 | revAppend [] ns = rewrite appendNilRightNeutral (reverse ns) in Refl
1057 | revAppend (v :: vs) ns
1058 |     = rewrite revOnto [v] vs in
1059 |         rewrite revOnto [v] (vs ++ ns) in
1060 |           rewrite sym (revAppend vs ns) in
1061 |             rewrite appendAssociative (reverse ns) (reverse vs) [v] in
1062 |               Refl
1063 |
1064 | ||| Dropping `m` elements from `l` and then dropping `n` elements from the
1065 | ||| result, is the same as simply dropping `n+m` elements from `l`
1066 | export
1067 | dropFusion : (n, m : Nat) -> (l : List t) -> drop n (drop m l) = drop (n+m) l
1068 | dropFusion  Z     m    l      = Refl
1069 | dropFusion (S n)  Z    l      = rewrite plusZeroRightNeutral n in Refl
1070 | dropFusion (S n) (S m) []     = Refl
1071 | dropFusion (S n) (S m) (x::l) = rewrite plusAssociative n 1 m in
1072 |                                 rewrite plusCommutative n 1 in
1073 |                                 dropFusion (S n) m l
1074 |
1075 | ||| Mapping a function over a list does not change the length of the list.
1076 | export
1077 | lengthMap : (xs : List a) -> length (map f xs) = length xs
1078 | lengthMap [] = Refl
1079 | lengthMap (x :: xs) = cong S (lengthMap xs)
1080 |
1081 | ||| Proof that replicate produces a list of the requested length.
1082 | export
1083 | lengthReplicate : (n : Nat) -> length (replicate n x) = n
1084 | lengthReplicate 0 = Refl
1085 | lengthReplicate (S k) = cong S (lengthReplicate k)
1086 |
1087 | export
1088 | foldlAppend : (f : acc -> a -> acc) -> (init : acc) -> (xs : List a) -> (ys : List a) -> foldl f init (xs ++ ys) = foldl f (foldl f init xs) ys
1089 | foldlAppend f init []      ys = Refl
1090 | foldlAppend f init (x::xs) ys = rewrite foldlAppend f (f init x) xs ys in Refl
1091 |
1092 | export
1093 | filterAppend : (f : a -> Bool) -> (xs, ys : List a) -> filter f (xs ++ ys) = filter f xs ++ filter f ys
1094 | filterAppend f []      ys = Refl
1095 | filterAppend f (x::xs) ys with (f x)
1096 |   _ | False = rewrite filterAppend f xs ys in Refl
1097 |   _ | True  = rewrite filterAppend f xs ys in Refl
1098 |
1099 | export
1100 | mapMaybeFusion : (g : b -> Maybe c) -> (f : a -> Maybe b) -> (xs : List a) -> mapMaybe g (mapMaybe f xs) = mapMaybe (f >=> g) xs
1101 | mapMaybeFusion g f []      = Refl
1102 | mapMaybeFusion g f (x::xs) with (f x)
1103 |   _ | Nothing = mapMaybeFusion g f xs
1104 |   _ | (Just y) with (g y)
1105 |     _ | Nothing = mapMaybeFusion g f xs
1106 |     _ | (Just z) = rewrite mapMaybeFusion g f xs in Refl
1107 |
1108 | export
1109 | mapMaybeAppend : (f : a -> Maybe b) -> (xs, ys : List a) -> mapMaybe f (xs ++ ys) = mapMaybe f xs ++ mapMaybe f ys
1110 | mapMaybeAppend f []      ys = Refl
1111 | mapMaybeAppend f (x::xs) ys with (f x)
1112 |   _ | Nothing  = rewrite mapMaybeAppend f xs ys in Refl
1113 |   _ | (Just y) = rewrite mapMaybeAppend f xs ys in Refl
1114 |
1115 | export
1116 | mapFusion : (g : b -> c) -> (f : a -> b) -> (xs : List a) -> map g (map f xs) = map (g . f) xs
1117 | mapFusion g f []      = Refl
1118 | mapFusion g f (x::xs) = rewrite mapFusion g f xs in Refl
1119 |
1120 | export
1121 | mapAppend : (f : a -> b) -> (xs, ys : List a) -> map f (xs ++ ys) = map f xs ++ map f ys
1122 | mapAppend f []      ys = Refl
1123 | mapAppend f (x::xs) ys = rewrite mapAppend f xs ys in Refl
1124 |
1125 | 0 mapTRIsMap :  (f : a -> b) -> (as : List a) -> mapTR f as === map f as
1126 | mapTRIsMap f = lemma Lin
1127 |   where lemma :  (sb : SnocList b)
1128 |               -> (as : List a)
1129 |               -> mapAppend sb f as === (sb <>> map f as)
1130 |         lemma sb []        = Refl
1131 |         lemma sb (x :: xs) = lemma (sb :< f x) xs
1132 |
1133 |
1134 | 0 mapMaybeTRIsMapMaybe :  (f : a -> Maybe b)
1135 |                        -> (as : List a)
1136 |                        -> mapMaybeTR f as === mapMaybe f as
1137 | mapMaybeTRIsMapMaybe f = lemma Lin
1138 |   where lemma :  (sb : SnocList b)
1139 |               -> (as : List a)
1140 |               -> mapMaybeAppend sb f as === (sb <>> mapMaybe f as)
1141 |         lemma sb []        = Refl
1142 |         lemma sb (x :: xs) with (f x)
1143 |           lemma sb (x :: xs) | Nothing = lemma sb xs
1144 |           lemma sb (x :: xs) | Just v  = lemma (sb :< v) xs
1145 |
1146 | 0 filterTRIsFilter :  (f : a -> Bool)
1147 |                    -> (as : List a)
1148 |                    -> filterTR f as === filter f as
1149 | filterTRIsFilter f = lemma Lin
1150 |
1151 |   where lemma :  (sa : SnocList a)
1152 |               -> (as : List a)
1153 |               -> filterAppend sa f as === (sa <>> filter f as)
1154 |         lemma sa []        = Refl
1155 |         lemma sa (x :: xs) with (f x)
1156 |           lemma sa (x :: xs) | False = lemma sa xs
1157 |           lemma sa (x :: xs) | True  = lemma (sa :< x) xs
1158 |
1159 | 0 replicateTRIsReplicate : (n : Nat) -> (x : a) -> replicateTR [] n x === replicate n x
1160 | replicateTRIsReplicate n x = trans (lemma [] n) (appendNilRightNeutral _)
1161 |   where lemma1 : (as : List a) -> (m : Nat) -> (x :: replicate m x) ++ as === replicate m x ++ (x :: as)
1162 |         lemma1 as 0     = Refl
1163 |         lemma1 as (S k) = cong (x ::) (lemma1 as k)
1164 |
1165 |         lemma : (as : List a) -> (m : Nat) -> replicateTR as m x === replicate m x ++ as
1166 |         lemma as 0     = Refl
1167 |         lemma as (S k) =
1168 |           let prf := lemma (x :: as) k
1169 |            in trans prf (sym $ lemma1 as k)
1170 |