Permuting elements of a list

Stream: new members

[Ben Whitmore]

Given l : List T, how can I transpose two of its elements (or more generally, apply a permutation to l)? I can't find a function anywhere in the standard library or mathlib that does this.

[Martin Dvořák]

Are you searching for a function that can be executed?

As for formulation, what list permutations are, Mathlib.Data.List.Perm defines them as follows...
If s and t are lists of the same type, then s ~ t denotes that s is a permutation of t
where ~ is a binary relation defined by the following four rules:
• empty list is a permutation of empty list: [] ~ []
• if a is an element and x and y are lists such that x ~ y then we have: a :: x ~ a :: y
• if a and b are elements and x is a list then we have: b :: a :: x ~ a :: b :: x
• if x, y, z are lists such that x ~ y and y ~ z then we have: x ~ z

[Martin Dvořák]

Writing a function (executable) that swaps the first two elements is trivial.
However, if you want to write a function that applies a general permutation to a list, you first need to tell us what is the permutation term that you want to apply to the list.

[Ben Whitmore]

Yes I want a function that defines the action of permutations on lists, so e.g. something like List.swap [9,8,7,6,5] 1 4 = [9,5,7,6,8]. I saw List.Perm but it just seems to define the statement that two lists are permutations of each other.

[Ben Whitmore]

I didn't really want to write it myself if it's avoidable, I just assumed that this would be a basic thing that mathlib would have had for years already that I couldn't find in the documentation.

[Martin Dvořák]

Ah, you want a function that applies a single transposition to a list, given indices that elements should be swapped at?

[Ben Whitmore]

Either that, or something that permutes a list arbitrarily using an Equiv.Perm Nat or something

[Ben Whitmore]

I'm trying to implement the 15 puzzle as a list of numbers, and define moves as transpositions of pieces

[Martin Dvořák]

@loogle (List ?a -> Nat -> Nat -> List ?a)

[loogle]

:search: Nat.toDigitsCore, Array.toListLitAux, and 5 more

[Martin Dvořák]

@loogle (Nat -> Nat -> List ?a -> List ?a)

[loogle]

:search: Nat.toDigitsCore, Array.toListLitAux, and 5 more

[Martin Dvořák]

@loogle (Equiv.Perm Nat -> List ?a -> List ?a)

[loogle]

:shrug: nothing found

[Martin Dvořák]

I didn't find anything.

[Martin Dvořák]

@loogle (Equiv.Perm (Fin ?n) -> List ?a -> List ?a)

[loogle]

:shrug: nothing found

[ZHAO Jiecheng]

Since List provides set and get. You can do that easily.

def List.swap (l: List α) (i j: Nat) (ha: i < l.length) (hb: j < l.length): List α :=
  let a := l[i]
  let b := l[j]
  (l.set i b).set j a

[Mario Carneiro]

you should probably special case i = j there

[ZHAO Jiecheng]

Mario Carneiro said:

you should probably special case i = j there

Why? Is there any special reason?

[Eric Wieser]

A slight bigger hammer is List.ofFn (l.get ∘ e)

[ZHAO Jiecheng]

Another piece of code. BTW, if I want to upload this to Std or Mathlib. what shall I follow?

def List.select (l: List α) (idxs: List Nat) (h: idxs.all (fun x => x < l.length) = true) : List α :=
  match idxs with
  | [] => []
  | idx :: tail =>
    have : idx < length l ∧ foldr (fun idx r => decide (idx < length l) && r) true tail = true := by
      simp [all] at h
      unfold foldr at h
      simp at h
      exact h
    l[idx]'this.left :: (List.select l tail this.right)

[Eric Wieser]

Isn't that effectively just idxs.map get?

[Ben Whitmore]

After implementing a swap function manually, and many more hours of trawling through documentation, I found that I could have just done [1, 2, 3, 4, 5].map (Equiv.swap 1 3) to get [3, 2, 1, 4, 5].

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Equiv/Basic.html#Equiv.swap

[Ben Whitmore]

Actually no, that's not right either, that just swaps the 3 with a 4 and the 4 with a 3, not the 3rd and 4th element

[Ben Whitmore]

Eric Wieser said:

A slight bigger hammer is List.ofFn (l.get ∘ e)

This seems to work ok. I at least managed to implement the permutation as a scalar multiplication operation on fixed-length lists:

structure FixedLengthList (T : Type) (n : ℕ) where
  list : List T
  length : list.length = n

instance List.perm_smul {T n} [NeZero n] : SMul (Equiv.Perm (Fin n)) (FixedLengthList T n) where
  smul := by
    intro perm l
    let n' := l.list.length
    let f (k : Fin n) : Fin n' := Fin.cast l.length.symm (perm k)
    let list := List.ofFn (l.list.get ∘ f)
    let length : list.length = n := by apply List.length_ofFn
    exact FixedLengthList.mk list length

def l : FixedLengthList ℕ 5 := FixedLengthList.mk [5,4,3,2,1] (by rfl)
def p : Equiv.Perm (Fin 5) := Equiv.swap 1 2

#eval (p • l).list -- [5, 3, 4, 2, 1]