Data.Permutation

Definitions

factorial : Integer -> Integer

Totality: total
Visibility: public export

data Permutation : Nat -> Type

  A permutation on `n` elements. This can be used to reorder values
  in a list or define actions on objects in a symmetric monoidal
  category.
  
  The permutation is stored in Lehmer code form as a list of factorial
  digits.

Totality: total
Visibility: public export
Constructors:

Nil : Permutation 0
(::) : Fin (S n) -> Permutation n -> Permutation (S n)

toVect : Permutation n -> Vect n Nat

Totality: total
Visibility: public export

toList : Permutation n -> List Nat

Totality: total
Visibility: public export

permSeq : Permutation n -> Vect n (Fin n)

  Convert a permutation into its *permutation sequence*.
  
  The output is a `Vect` of indices where the `i`-th value is the
  image of `i`. The output is guaranteed to have unique elements.

Totality: total
Visibility: public export

fromPermSeq : Vect n (Fin n) -> Maybe (Permutation n)

  Maybe convert a permutation sequence into a permutation.
  
  The input is a `Vect` of indices where the `i`-th value is the
  image of `i`. The function will return `Nothing` if any of the
  incides is repeated.

Totality: total
Visibility: public export

lehmerCode : Permutation n -> Integer

  Return the Lehmer code of the permutation as a machine integer.

Totality: total
Visibility: public export

fromLehmerCode : (x : Integer) -> {auto 0 _ : So ((x >= 0) && Delay (x < factorial (natToInteger n)))} -> Permutation n

  Compute the permutation associated with the given Lehmer code.

Totality: total
Visibility: public export

identity : Permutation n

  The identity permutation on `n` elements.

Totality: total
Visibility: public export

inverse : Permutation n -> Permutation n

  Compute the inverse of the permutation.

Totality: total
Visibility: public export

compose : Permutation n -> Permutation n -> Permutation n

  Compose two permutations into a new permutation.
  
  Note that this uses function composition order, so that the right
  permutation is applied first.

Totality: total
Visibility: public export

horiz : Permutation m -> Permutation n -> Permutation (m + n)

  Horizontally compose two permutations into a larger permutation.
  
  This corresponds to the action of the Cartesian product on
  isomorphisms.

Totality: total
Visibility: public export

permuteVect : Permutation n -> Vect n a -> Vect n a

  Permute the elements of the `Vect` using the permutation.

Totality: total
Visibility: public export

permuteList : (xs : List a) -> Permutation (length xs) -> List a

  Permute the elements of the list using the permutation.

Totality: total
Visibility: public export

permuteHVect : (p : Permutation n) -> All q ts -> All q (permuteVect p ts)

  Permute the elements of the `HVect` using the permutation.

Totality: total
Visibility: public export

permuteHList : (p : Permutation (length ts)) -> All q ts -> All q (permuteList ts p)

  Permute the elements of the `HList` using the permutation.

Totality: total
Visibility: public export

permSeqInv : (p : Permutation n) -> fromPermSeq (permSeq p) = Just p