Idris2Doc : Data.Fin.Extra

Data.Fin.Extra

Definitions
elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
  A Fin's underlying natural number is smaller than the bound

  Totality: total
  Visibility: export
finToNatLastIsBound : finToNat last = n
  Last's underlying natural number is the bound's predecessor

  Totality: total
  Visibility: export
finToNatWeakenNeutral : finToNat (weaken n) = finToNat n
  Weaken does not modify the underlying natural number

  Totality: total
  Visibility: export
finToNatWeakenNNeutral : (0 m : Nat) -> (k : Fin n) -> finToNat (weakenN m k) = finToNat k
  WeakenN does not modify the underlying natural number

  Totality: total
  Visibility: export
finToNatShift : (k : Nat) -> (a : Fin n) -> finToNat (shift k a) = k + finToNat a
  `Shift k` shifts the underlying natural number by `k`.

  Totality: total
  Visibility: export
invFin : Fin n -> Fin n
  Compute the Fin such that `k + invFin k = n - 1`

  Totality: total
  Visibility: public export
invFinSpec : (i : Fin n) -> (1 + finToNat i) + finToNat (invFin i) = n
  Totality: total
  Visibility: export
invFinWeakenIsFS : (m : Fin n) -> invFin (weaken m) = FS (invFin m)
  The inverse of a weakened element is the successor of its inverse

  Totality: total
  Visibility: export
invFinLastIsFZ : invFin last = FZ
  Totality: total
  Visibility: export
invFinInvolutive : (m : Fin n) -> invFin (invFin m) = m
  `invFin` is involutive (i.e. applied twice it is the identity)

  Totality: total
  Visibility: export
strengthenWeakenIsRight : (n : Fin m) -> strengthen (weaken n) = Just n
  It's possible to strengthen a weakened element of Fin **m**.

  Totality: total
  Visibility: export
strengthenLastIsLeft : strengthen last = Nothing
  It's not possible to strengthen the last element of Fin **n**.

  Totality: total
  Visibility: export
strengthenNotLastIsRight : (m : Fin n) -> strengthen (invFin (FS m)) = Just (invFin m)
  It's possible to strengthen the inverse of a succesor

  Totality: total
  Visibility: export
strengthen' : (m : Fin (S n)) -> Either (m = last) (m' : Fin n ** finToNat m = finToNat m')
  Either tightens the bound on a Fin or proves that it's the last.

  Totality: total
  Visibility: export
strengthenMod : Fin n -> (m : Nat) -> NonZero m => Fin m
  Tighten the bound on a Fin by taking its current bound modulo the given
  non-zero number.

  Totality: total
  Visibility: export
weakenNZeroIdentity : (k : Fin n) -> weakenN 0 k ~~~ k
  Totality: total
  Visibility: export
shiftFSLinear : (m : Nat) -> (f : Fin n) -> shift m (FS f) ~~~ FS (shift m f)
  Totality: total
  Visibility: export
shiftLastIsLast : (m : Nat) -> shift m last ~~~ last
  Totality: total
  Visibility: export
data FractionView : Nat -> Nat -> Type
  A view of Nat as a quotient of some number and a finite remainder.

  Totality: total
  Visibility: public export
  Constructor: 
Fraction : (n : Nat) -> (d : Nat) -> GT d 0 => (q : Nat) -> (r : Fin d) -> (q * d) + finToNat r = n -> FractionView n d
divMod : (n : Nat) -> (d : Nat) -> GT d 0 => FractionView n d
  Converts Nat to the fractional view with a non-zero divisor.

  Totality: total
  Visibility: export
modFin : Nat -> (m : Nat) -> NonZero m => Fin m
  Compute n % m as a Fin with upper bound m.
  
  Useful, for example, when iterating through a large index, computing
  subindices as a function of the larger index (e.g. a flattened 2D-array)

  Totality: total
  Visibility: export
natToFinLTE : (n : Nat) -> (0 _ : LT n m) -> Fin m
  Total function to convert a nat to a Fin, given a proof
  that it is less than the bound.

  Totality: total
  Visibility: public export
natToFinToNat : (n : Nat) -> (lte : LT n m) -> finToNat (natToFinLTE n lte) = n
  Converting from a Nat to a Fin and back is the identity.

  Totality: total
  Visibility: public export
(+) : Fin m -> Fin (S n) -> Fin (m + n)
  Addition of `Fin`s as bounded naturals.
  The resulting type has the smallest possible bound
  as illustated by the relations with the `last` function.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 8
(*) : Fin (S m) -> Fin (S n) -> Fin (S (m * n))
  Multiplication of `Fin`s as bounded naturals.
  The resulting type has the smallest possible bound
  as illustated by the relations with the `last` function.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 9
finToNatPlusHomo : (x : Fin m) -> (y : Fin (S n)) -> finToNat (x + y) = finToNat x + finToNat y
  Totality: total
  Visibility: export
finToNatMultHomo : (x : Fin (S m)) -> (y : Fin (S n)) -> finToNat (x * y) = finToNat x * finToNat y
  Totality: total
  Visibility: export
plusPreservesLast : (m : Nat) -> (n : Nat) -> last + last = last
  Totality: total
  Visibility: export
multPreservesLast : (m : Nat) -> (n : Nat) -> last * last = last
  Totality: total
  Visibility: export
plusSuccRightSucc : (left : Fin m) -> (right : Fin (S n)) -> FS (left + right) ~~~ (left + FS right)
  Totality: total
  Visibility: export
shiftAsPlus : (k : Fin (S m)) -> shift n k ~~~ (last + k)
  Totality: total
  Visibility: export
weakenNAsPlusFZ : (k : Fin n) -> weakenN m k = k + the (Fin (S m)) FZ
  Totality: total
  Visibility: export
weakenNPlusHomo : (k : Fin p) -> weakenN n (weakenN m k) ~~~ weakenN (m + n) k
  Totality: total
  Visibility: export
weakenNOfPlus : (k : Fin m) -> (l : Fin (S n)) -> weakenN w (k + l) ~~~ (weakenN w k + l)
  Totality: total
  Visibility: export
plusZeroLeftNeutral : (k : Fin (S n)) -> (FZ + k) ~~~ k
  Totality: total
  Visibility: export
congPlusLeft : (c : Fin (S p)) -> k ~~~ l -> (k + c) ~~~ (l + c)
  Totality: total
  Visibility: export
plusZeroRightNeutral : (k : Fin m) -> (k + FZ) ~~~ k
  Totality: total
  Visibility: export
congPlusRight : (c : Fin m) -> k ~~~ l -> (c + k) ~~~ (c + l)
  Totality: total
  Visibility: export
plusCommutative : (left : Fin (S m)) -> (right : Fin (S n)) -> (left + right) ~~~ (right + left)
  Totality: total
  Visibility: export
plusAssociative : (left : Fin m) -> (centre : Fin (S n)) -> (right : Fin (S p)) -> (left + (centre + right)) ~~~ ((left + centre) + right)
  Totality: total
  Visibility: export
indexSum : Either (Fin m) (Fin n) -> Fin (m + n)
  Converts `Fin`s that are used as indexes of parts to an index of a sum.
  
  For example, if you have a `Vect` that is a concatenation of two `Vect`s and
  you have an index either in the first or the second of the original `Vect`s,
  using this function you can get an index in the concatenated one.

  Totality: total
  Visibility: public export
splitSum : Fin (m + n) -> Either (Fin m) (Fin n)
  Extracts an index of the first or the second part from the index of a sum.
  
  For example, if you have a `Vect` that is a concatenation of the `Vect`s and
  you have an index of this `Vect`, you have get an index of either left or right
  original `Vect` using this function.

  Totality: total
  Visibility: public export
indexProd : Fin m -> Fin n -> Fin (m * n)
  Calculates the index of a square matrix of size `a * b` by indices of each side.

  Totality: total
  Visibility: public export
splitProd : Fin (m * n) -> (Fin m, Fin n)
  Splits the index of a square matrix of size `a * b` to indices of each side.

  Totality: total
  Visibility: public export
indexSumPreservesLast : (m : Nat) -> (n : Nat) -> indexSum (Right last) ~~~ last
  Totality: total
  Visibility: export
indexProdPreservesLast : (m : Nat) -> (n : Nat) -> indexProd last last = last
  Totality: total
  Visibility: export
splitSumOfWeakenN : (k : Fin m) -> splitSum (weakenN n k) = Left k
  Totality: total
  Visibility: export
splitSumOfShift : (k : Fin n) -> splitSum (shift m k) = Right k
  Totality: total
  Visibility: export
splitOfIndexSumInverse : (e : Either (Fin m) (Fin n)) -> splitSum (indexSum e) = e
  Totality: total
  Visibility: export
indexOfSplitSumInverse : (f : Fin (m + n)) -> indexSum (splitSum f) = f
  Totality: total
  Visibility: export
splitOfIndexProdInverse : (k : Fin m) -> (l : Fin n) -> splitProd (indexProd k l) = (k, l)
  Totality: total
  Visibility: export
indexOfSplitProdInverse : (f : Fin (m * n)) -> uncurry indexProd (splitProd f) = f
  Totality: total
  Visibility: export