Data.Fin

Reexports

import public Control.Ord
import public Data.Maybe
import public Data.Nat
import public Data.So

Definitions

data Fin : Nat -> Type

  Numbers strictly less than some bound.  The name comes from "finite sets".
  
  It's probably not a good idea to use `Fin` for arithmetic, and they will be
  exceedingly inefficient at run time.
  @ n the upper bound

Totality: total
Visibility: public export
Constructors:

FZ : Fin (S k)
FS : Fin k -> Fin (S k)

Hints:

Cast (Fin n) Nat
Cast (Fin n) Integer
DecEq (Fin n)
Eq (Fin n)
Injective FS
Injective finToNat
Neg (Fin (S n))
Num (Fin (S n))
Ord (Fin n)
Show (Fin n)
Uninhabited (Fin 0)
Uninhabited (FZ = FS k)
Uninhabited (FS k = FZ)
Uninhabited (n = m) => Uninhabited (FS n = FS m)
Uninhabited (FS k ~~~ FZ)
Uninhabited (FZ ~~~ FS k)

coerce : (0 _ : m = n) -> Fin m -> Fin n

  Coerce between Fins with equal indices

Totality: total
Visibility: public export

finToNat : Fin n -> Nat

  Convert a Fin to a Nat

Totality: total
Visibility: public export

finToInteger : Fin n -> Integer

  Convert a Fin to an Integer

Totality: total
Visibility: public export

weaken : Fin n -> Fin (S n)

  Weaken the bound on a Fin by 1

Totality: total
Visibility: public export

weakenN : (0 n : Nat) -> Fin m -> Fin (m + n)

  Weaken the bound on a Fin by some amount

Totality: total
Visibility: public export

weakenLTE : Fin n -> LTE n m -> Fin m

  Weaken the bound on a Fin using a constructive comparison

Totality: total
Visibility: public export

strengthen : Fin (S n) -> Maybe (Fin n)

  Attempt to tighten the bound on a Fin.
  Return the tightened bound if there is one, else nothing.

Totality: total
Visibility: export

shift : (m : Nat) -> Fin n -> Fin (m + n)

  Add some natural number to a Fin, extending the bound accordingly
  @ n the previous bound
  @ m the number to increase the Fin by

Totality: total
Visibility: public export

finS : Fin n -> Fin n

  Increment a Fin, wrapping on overflow

Totality: total
Visibility: public export

last : Fin (S n)

  The largest element of some Fin type

Totality: total
Visibility: public export

complement : Fin n -> Fin n

  The finite complement of some Fin.
  The number as far along as the input, but starting from the other end.

Totality: total
Visibility: public export

allFins : (n : Nat) -> List (Fin n)

  All of the Fin elements

Totality: total
Visibility: public export

allFins : (n : Nat) -> List1 (Fin (S n))

  All of the Fin elements

Totality: total
Visibility: public export

natToFinLT : (x : Nat) -> {auto 0 _ : LT x n} -> Fin n

Totality: total
Visibility: public export

natToFinLt : (x : Nat) -> {auto 0 _ : So (x < n)} -> Fin n

Totality: total
Visibility: public export

natToFin : Nat -> (n : Nat) -> Maybe (Fin n)

Totality: total
Visibility: public export

integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)

  Convert an `Integer` to a `Fin`, provided the integer is within bounds.
  @n The upper bound of the Fin

Totality: total
Visibility: public export

maybeLTE : (x : Nat) -> (y : Nat) -> Maybe (LTE x y)

Totality: total
Visibility: public export

maybeLT : (x : Nat) -> (y : Nat) -> Maybe (LT x y)

Totality: total
Visibility: public export

finFromInteger : (x : Integer) -> {auto 0 _ : So (fromInteger x < n)} -> Fin n

Totality: total
Visibility: public export

integerLessThanNat : Integer -> Nat -> Bool

Totality: total
Visibility: public export

fromInteger : (x : Integer) -> {auto 0 _ : So (integerLessThanNat x n)} -> Fin n

  Allow overloading of Integer literals for Fin.
  @ x the Integer that the user typed
  @ prf an automatically-constructed proof that `x` is in bounds

Totality: total
Visibility: public export

restrict : (n : Nat) -> Integer -> Fin (S n)

  Convert an Integer to a Fin in the required bounds/
  This is essentially a composition of `mod` and `fromInteger`

Totality: total
Visibility: public export

data Pointwise : Fin m -> Fin n -> Type

  Pointwise equality of Fins
  It is sometimes complicated to prove equalities on type-changing
  operations on Fins.
  This inductive definition can be used to simplify proof. We can
  recover proofs of equalities by using `homoPointwiseIsEqual`.

Totality: total
Visibility: public export
Constructors:

FZ : Pointwise FZ FZ
FS : Pointwise k l -> Pointwise (FS k) (FS l)

(~~~) : Fin m -> Fin n -> Type

  Convenient infix notation for the notion of pointwise equality of Fins

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6

reflexive : k ~~~ k

  Pointwise equality is reflexive

Totality: total
Visibility: export

symmetric : k ~~~ l -> l ~~~ k

  Pointwise equality is symmetric

Totality: total
Visibility: export

transitive : j ~~~ k -> k ~~~ l -> j ~~~ l

  Pointwise equality is transitive

Totality: total
Visibility: export

coerceEq : (0 eq : m = n) -> coerce eq k ~~~ k

  Pointwise equality is compatible with coerce

Totality: total
Visibility: export

congCoerce : k ~~~ l -> coerce eq1 k ~~~ coerce eq2 l

  The actual proof used by coerce is irrelevant

Totality: total
Visibility: export

congLast : (0 _ : m = n) -> last ~~~ last

  Last is congruent wrt index equality

Totality: total
Visibility: export

congShift : (m : Nat) -> k ~~~ l -> shift m k ~~~ shift m l

Totality: total
Visibility: export

congWeakenN : k ~~~ l -> weakenN n k ~~~ weakenN n l

  WeakenN is congruent wrt pointwise equality

Totality: total
Visibility: export

homoPointwiseIsEqual : k ~~~ l -> k = l

  Pointwise equality is propositional equality on Fins that have the same type

Totality: total
Visibility: export

hetPointwiseIsTransport : (0 eq : m = n) -> k ~~~ l -> k = rewrite__impl {_:5275} {_:5274} l

  Pointwise equality is propositional equality modulo transport on Fins that
  have provably equal types

Totality: total
Visibility: export

finToNatQuotient : k ~~~ l -> finToNat k = finToNat l

Totality: total
Visibility: export

finToNatEqualityAsPointwise : (k : Fin m) -> (l : Fin n) -> finToNat k = finToNat l -> k ~~~ l

  Propositional equality on `finToNat`s implies pointwise equality on the `Fin`s themselves

Totality: total
Visibility: export

weakenNeutral : (k : Fin n) -> weaken k ~~~ k

Totality: total
Visibility: export

weakenNNeutral : (0 m : Nat) -> (k : Fin n) -> weakenN m k ~~~ k

Totality: total
Visibility: export