Agda-2.3.2.1: A dependently typed functional programming language and proof assistant

Agda.Utils.Permutation

Synopsis

# Documentation

`permute [1,2,0] [x0,x1,x2] = [x1,x2,x0]`

Agda typing would be: `Perm : {m : Nat}(n : Nat) -> Vec (Fin n) m -> Permutation` `m` is the `size` of the permutation.

Constructors

 Perm FieldspermRange :: Int permPicks :: [Int]

permute :: Permutation -> [a] -> [a]Source

`permute [1,2,0] [x0,x1,x2] = [x1,x2,x0]` More precisely, `permute indices list = sublist`, generates `sublist` from `list` by picking the elements of list as indicated by `indices`. `permute [1,3,0] [x0,x1,x2,x3] = [x1,x3,x0]`

Agda typing: `permute (Perm {m} n is) : Vec A m -> Vec A n`

`liftP k` takes a `Perm {m} n` to a `Perm {m+k} (n+k)`. Analogous to `liftS`, but Permutations operate on de Bruijn LEVELS, not indices.

`permute (compose p1 p2) == permute p1 . permute p2`

Turn a possible non-surjective permutation into a surjective permutation.

```permute (reverseP p) xs ==
reverse \$ permute p \$ reverse xs```

Example: ``` permute (reverseP (Perm 4 [1,3,0])) [x0,x1,x2,x3] == permute (Perm 4 \$ map (3-) [0,3,1]) [x0,x1,x2,x3] == permute (Perm 4 [3,0,2]) [x0,x1,x2,x3] == [x3,x0,x2] == reverse [x2,x0,x3] == reverse \$ permute (Perm 4 [1,3,0]) [x3,x2,x1,x0] == reverse \$ permute (Perm 4 [1,3,0]) \$ reverse [x0,x1,x2,x3] ```

`expandP i n π` in the domain of `π` replace the ith element by n elements.

topoSort :: (a -> a -> Bool) -> [a] -> Maybe PermutationSource

Stable topologic sort. The first argument decides whether its first argument is an immediate parent to its second argument.