Data.List.AtIndex

Indexing into Lists.

`Elem` proofs give existential quantification that a given element
*is* in the list, but not where in the list it is!  Here we give a
predicate that presents proof that a given index in a list, given
by a natural number, will return a certain element.

Definitions

data AtIndex : a -> List a -> Nat -> Type

  @AtIndex witnesses the fact that a natural number encodes a membership proof.
  It is meant to be used as a runtime-irrelevant gadget to guarantee that the
  natural number is indeed a valid index.

Totality: total
Visibility: public export
Constructors:

Z : AtIndex a (a :: as) 0

S : AtIndex a as n -> AtIndex a (b :: as) (S n)

Hint: 

Uninhabited (AtIndex a [] n)

inverseZ : AtIndex x (y :: xs) 0 -> x = y

  Inversion principle for Z constructor

Totality: total
Visibility: export

inverseS : AtIndex x (y :: xs) (S n) -> AtIndex x xs n

  inversion principle for S constructor

Totality: total
Visibility: export

atIndexUnique : AtIndex a as n -> AtIndex b as n -> a = b

  For a given list and a given index, there is only one possible value
  stored at that index in that list

Totality: total
Visibility: export

find : DecEq a => (x : a) -> (xs : List a) -> Dec (Subset Nat (AtIndex x xs))

  Provided that equality is decidable, we can look for the first occurrence
  of a value inside of a list

Totality: total
Visibility: public export

lookup : (n : Nat) -> (xs : List a) -> Dec (Subset a (\x => AtIndex x xs n))

  Given an index, we can decide whether there is a value corresponding to it

Totality: total
Visibility: public export

inRange : (n : Nat) -> (xs : List a) -> (0 _ : AtIndex x xs n) -> LTE n (length xs)

  An AtIndex proof implies that n is less than the length of the list indexed into

Totality: total
Visibility: public export

weakenR : AtIndex x xs n -> AtIndex x (xs ++ ys) n

  An index remains unchanged if we extend the list to the right

Totality: total
Visibility: export

weakenL : (p : Subset Nat (flip HasLength ws)) -> AtIndex x xs n -> AtIndex x (ws ++ xs) (fst p + n)

  An index into `xs` is shifted by `m` if we prepend a list of size `m`
  in front of it

Totality: total
Visibility: export

strengthenL : (p : Subset Nat (flip HasLength xs)) -> lt n (fst p) = True -> AtIndex x (xs ++ ys) n -> AtIndex x xs n

  Conversely to `weakenR`, if an index is smaller than the length of
  a prefix then it points into that prefix.

Totality: total
Visibility: export

strengthenR : (p : Subset Nat (flip HasLength ws)) -> lte (fst p) n = True -> AtIndex x (ws ++ xs) n -> AtIndex x xs (minus n (fst p))

  Conversely to `weakenL`, if an index is larger than the length of
  a prefix then it points into the suffix.

Totality: total
Visibility: export