Data.List.HasLength

This module implements a relation between a natural number and a list.
The relation witnesses the fact the number is the length of the list.

It is meant to be used in a runtime-irrelevant fashion in computations
manipulating data indexed over lists where the computation actually only
depends on the length of said lists.

Instead of writing:
```idris example
f0 : (xs : List a) -> P xs
```

We would write either of:
```idris example
f1 : (n : Nat) -> (0 _ : HasLength n xs) -> P xs
f2 : (n : Subset n (flip HasLength xs)) -> P xs
```

See `sucR` for an example where the update to the runtime-relevant Nat is O(1)
but the udpate to the list (were we to keep it around) an O(n) traversal.

Definitions

data HasLength : Nat -> List a -> Type

  Ensure that the list's length is the provided natural number

Totality: total
Visibility: public export
Constructors:

Z : HasLength 0 []

S : HasLength n xs -> HasLength (S n) (x :: xs)

hasLength : (xs : List a) -> HasLength (length xs) xs

  This specification corresponds to the length function

Totality: total
Visibility: export

take : (n : Nat) -> (xs : Stream a) -> HasLength n (take n xs)

Totality: total
Visibility: export

hasLengthUnique : HasLength m xs -> HasLength n xs -> m = n

  The length is unique

Totality: total
Visibility: export

hasLengthAppend : HasLength m xs -> HasLength n ys -> HasLength (m + n) (xs ++ ys)

Totality: total
Visibility: export

hasLengthReverse : HasLength m acc -> HasLength m (reverse acc)

Totality: total
Visibility: export

map : (f : (a -> b)) -> HasLength n xs -> HasLength n (map f xs)

Totality: total
Visibility: export

sucR : HasLength n xs -> HasLength (S n) (snoc xs x)

  @sucR demonstrates that snoc only increases the lenght by one
  So performing this operation while carrying the list around would cost O(n)
  but relying on n together with an erased HasLength proof instead is O(1)

Totality: total
Visibility: export

data View : (xs : List a) -> Subset Nat (flip HasLength xs) -> Type

  We provide this view as a convenient way to perform nested pattern-matching
  on values of type `Subset Nat (flip HasLength xs)`. Functions using this view will
  be seen as terminating as long as the index list `xs` is left untouched.
  See e.g. listTerminating below for such a function.

Totality: total
Visibility: public export
Constructors:

Z : View [] (Element 0 Z)

S : (p : Subset Nat (flip HasLength xs)) -> View (x :: xs) (Element (S (fst p)) (S (snd p)))

view : (p : Subset Nat (flip HasLength xs)) -> View xs p

  Proof that the view covers all possible cases.

Totality: total
Visibility: export

data View : (xs : List a) -> (n : Nat) -> HasLength n xs -> Type

  We provide this view as a convenient way to perform nested pattern-matching
  on pairs of values of type `n : Nat` and `HasLength xs n`. If transformations
  to the list between recursive calls (e.g. mapping over the list) that prevent
  it from being a valid termination metric, it is best to take the Nat argument
  separately from the HasLength proof and the Subset view is not as useful anymore.
  See e.g. natTerminating below for (a contrived example of) such a function.

Totality: total
Visibility: public export
Constructors:

Z : View [] 0 Z

S : (n : Nat) -> (0 p : HasLength n xs) -> View (x :: xs) (S n) (S p)

view : (n : Nat) -> (0 p : HasLength n xs) -> View xs n p

  Proof that the view covers all possible cases.

Totality: total
Visibility: export