Idris2Doc : Data.Fin.Extra

# Data.Fin.Extra

## Definitions

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

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

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

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

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

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

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

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

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

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

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

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

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

Totality: total
Visibility: export
weakenNZeroIdentity : (k : Finn) ->weakenN0k~~~k
Totality: total
Visibility: export
shiftFSLinear : (m : Nat) -> (f : Finn) ->shiftm (FSf) ~~~FS (shiftmf)
Totality: total
Visibility: export
shiftLastIsLast : (m : Nat) ->shiftmlast~~~last
Totality: total
Visibility: export
dataFractionView : 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) ->GTd0=> (q : Nat) -> (r : Find) -> (q*d) +finToNatr=n->FractionViewnd
divMod : (n : Nat) -> (d : Nat) ->GTd0=>FractionViewnd
Converts Nat to the fractional view with a non-zero divisor.

Totality: total
Visibility: export
modFin : Nat-> (m : Nat) ->NonZerom=>Finm
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_ : LTnm) ->Finm
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 : LTnm) ->finToNat (natToFinLTEnlte) =n
Converting from a Nat to a Fin and back is the identity.

Totality: total
Visibility: public export
(+) : Finm->Fin (Sn) ->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 (Sm) ->Fin (Sn) ->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 : Finm) -> (y : Fin (Sn)) ->finToNat (x+y) =finToNatx+finToNaty
Totality: total
Visibility: export
finToNatMultHomo : (x : Fin (Sm)) -> (y : Fin (Sn)) ->finToNat (x*y) =finToNatx*finToNaty
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 : Finm) -> (right : Fin (Sn)) ->FS (left+right) ~~~ (left+FSright)
Totality: total
Visibility: export
shiftAsPlus : (k : Fin (Sm)) ->shiftnk~~~ (last+k)
Totality: total
Visibility: export
weakenNAsPlusFZ : (k : Finn) ->weakenNmk=k+the (Fin (Sm)) FZ
Totality: total
Visibility: export
weakenNPlusHomo : (k : Finp) ->weakenNn (weakenNmk) ~~~weakenN (m+n) k
Totality: total
Visibility: export
weakenNOfPlus : (k : Finm) -> (l : Fin (Sn)) ->weakenNw (k+l) ~~~ (weakenNwk+l)
Totality: total
Visibility: export
plusZeroLeftNeutral : (k : Fin (Sn)) -> (FZ+k) ~~~k
Totality: total
Visibility: export
congPlusLeft : (c : Fin (Sp)) ->k~~~l-> (k+c) ~~~ (l+c)
Totality: total
Visibility: export
plusZeroRightNeutral : (k : Finm) -> (k+FZ) ~~~k
Totality: total
Visibility: export
congPlusRight : (c : Finm) ->k~~~l-> (c+k) ~~~ (c+l)
Totality: total
Visibility: export
plusCommutative : (left : Fin (Sm)) -> (right : Fin (Sn)) -> (left+right) ~~~ (right+left)
Totality: total
Visibility: export
plusAssociative : (left : Finm) -> (centre : Fin (Sn)) -> (right : Fin (Sp)) -> (left+ (centre+right)) ~~~ ((left+centre) +right)
Totality: total
Visibility: export
indexSum : Either (Finm) (Finn) ->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 (Finm) (Finn)
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 : Finm->Finn->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) -> (Finm, Finn)
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 (Rightlast) ~~~last
Totality: total
Visibility: export
indexProdPreservesLast : (m : Nat) -> (n : Nat) ->indexProdlastlast=last
Totality: total
Visibility: export
splitSumOfWeakenN : (k : Finm) ->splitSum (weakenNnk) =Leftk
Totality: total
Visibility: export
splitSumOfShift : (k : Finn) ->splitSum (shiftmk) =Rightk
Totality: total
Visibility: export
splitOfIndexSumInverse : (e : Either (Finm) (Finn)) ->splitSum (indexSume) =e
Totality: total
Visibility: export
indexOfSplitSumInverse : (f : Fin (m+n)) ->indexSum (splitSumf) =f
Totality: total
Visibility: export
splitOfIndexProdInverse : (k : Finm) -> (l : Finn) ->splitProd (indexProdkl) = (k, l)
Totality: total
Visibility: export
indexOfSplitProdInverse : (f : Fin (m*n)) ->uncurryindexProd (splitProdf) =f
Totality: total
Visibility: export