Data.Fin.Extra

(*) : 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
Fixity Declaration: infixl operator, level 9

(+) : 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
Fixity Declaration: infixl operator, level 8

data FractionView : Nat -> Nat -> Type

  A view of Nat as a quotient of some number and a finite remainder.

Totality: total
Constructor:

Fraction : (n : Nat) -> (d : Nat) -> GT d 0 => (q : Nat) -> (r : Fin d) -> (q * d) + finToNat r = n -> FractionView n d

congPlusLeft : (c : Fin (S p)) -> k ~~~ l -> (k + c) ~~~ (l + c)

Totality: total

congPlusRight : (c : Fin m) -> k ~~~ l -> (c + k) ~~~ (c + l)

Totality: total

divMod : (n : Nat) -> (d : Nat) -> GT d 0 => FractionView n d

  Converts Nat to the fractional view with a non-zero divisor.

Totality: total

elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m

  A Fin's underlying natural number is smaller than the bound

Totality: total

finToNatLastIsBound : finToNat last = n

  Last's underlying natural number is the bound's predecessor

Totality: total

finToNatMultHomo : (x : Fin (S m)) -> (y : Fin (S n)) -> finToNat (x * y) = finToNat x * finToNat y

Totality: total

finToNatPlusHomo : (x : Fin m) -> (y : Fin (S n)) -> finToNat (x + y) = finToNat x + finToNat y

Totality: total

finToNatShift : (k : Nat) -> (a : Fin n) -> finToNat (shift k a) = k + finToNat a

  `Shift k` shifts the underlying natural number by `k`.

Totality: total

finToNatWeakenNNeutral : (0 m : Nat) -> (k : Fin n) -> finToNat (weakenN m k) = finToNat k

  WeakenN does not modify the underlying natural number

Totality: total

finToNatWeakenNeutral : finToNat (weaken n) = finToNat n

  Weaken does not modify the underlying natural number

Totality: total

indexOfSplitProdInverse : (f : Fin (m * n)) -> uncurry indexProd (splitProd f) = f

Totality: total

indexOfSplitSumInverse : (f : Fin (m + n)) -> indexSum (splitSum f) = f

Totality: total

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

indexProdPreservesLast : (m : Nat) -> (n : Nat) -> indexProd last last = last

Totality: total

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

indexSumPreservesLast : (m : Nat) -> (n : Nat) -> indexSum (Right last) ~~~ last

Totality: total

invFin : Fin n -> Fin n

  Compute the Fin such that `k + invFin k = n - 1`

Totality: total

invFinInvolutive : (m : Fin n) -> invFin (invFin m) = m

  `invFin` is involutive (i.e. applied twice it is the identity)

Totality: total

invFinLastIsFZ : invFin last = FZ

Totality: total

invFinSpec : (i : Fin n) -> (1 + finToNat i) + finToNat (invFin i) = n

Totality: total

invFinWeakenIsFS : (m : Fin n) -> invFin (weaken m) = FS (invFin m)

  The inverse of a weakened element is the successor of its inverse

Totality: total

multPreservesLast : (m : Nat) -> (n : Nat) -> last * last = last

Totality: total

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

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

plusAssociative : (left : Fin m) -> (centre : Fin (S n)) -> (right : Fin (S p)) -> (left + (centre + right)) ~~~ ((left + centre) + right)

Totality: total

plusCommutative : (left : Fin (S m)) -> (right : Fin (S n)) -> (left + right) ~~~ (right + left)

Totality: total

plusPreservesLast : (m : Nat) -> (n : Nat) -> last + last = last

Totality: total

plusSuccRightSucc : (left : Fin m) -> (right : Fin (S n)) -> FS (left + right) ~~~ (left + FS right)

Totality: total

plusZeroLeftNeutral : (k : Fin (S n)) -> (FZ + k) ~~~ k

Totality: total

plusZeroRightNeutral : (k : Fin m) -> (k + FZ) ~~~ k

Totality: total

shiftAsPlus : (k : Fin (S m)) -> shift n k ~~~ (last + k)

Totality: total

shiftFSLinear : (m : Nat) -> (f : Fin n) -> shift m (FS f) ~~~ FS (shift m f)

Totality: total

shiftLastIsLast : (m : Nat) -> shift m last ~~~ last

Totality: total

splitOfIndexProdInverse : (k : Fin m) -> (l : Fin n) -> splitProd (indexProd k l) = (k, l)

Totality: total

splitOfIndexSumInverse : (e : Either (Fin m) (Fin n)) -> splitSum (indexSum e) = e

Totality: total

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

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

splitSumOfShift : (k : Fin n) -> splitSum (shift m k) = Right k

Totality: total

splitSumOfWeakenN : (k : Fin m) -> splitSum (weakenN n k) = Left k

Totality: total

strengthen' : (m : Fin (S n)) -> Either (m = last) (DPair (Fin n) (\m' => finToNat m = finToNat m'))

  Either tightens the bound on a Fin or proves that it's the last.

Totality: total

strengthenLastIsLeft : strengthen last = Nothing

  It's not possible to strengthen the last element of Fin **n**.

Totality: total

strengthenNotLastIsRight : (m : Fin n) -> strengthen (invFin (FS m)) = Just (invFin m)

  It's possible to strengthen the inverse of a succesor

Totality: total

strengthenWeakenIsRight : (n : Fin m) -> strengthen (weaken n) = Just n

  It's possible to strengthen a weakened element of Fin **m**.

Totality: total

weakenNAsPlusFZ : (k : Fin n) -> weakenN m k = k + the (Fin (S m)) FZ

Totality: total

weakenNOfPlus : (k : Fin m) -> (l : Fin (S n)) -> weakenN w (k + l) ~~~ (weakenN w k + l)

Totality: total

weakenNPlusHomo : (k : Fin p) -> weakenN n (weakenN m k) ~~~ weakenN (m + n) k

Totality: total

weakenNZeroIdentity : (k : Fin n) -> weakenN 0 k ~~~ k

Totality: total