Abstractions for working with permutation

Stream: lean4

[Zhuanhao Wu]

Hi all, I'm wondering what I should use to reason about permutations of some T (that is also a Fintype, if needed), any suggestions would be appreciated.

I know I can probably use List T, but my problem with using List T is that doesn't really capture the fact that it is a permutation of elements of T (so it may not have all elements, it has duplication).
Similar issue with Finset T, where I don't have the order of elements embedded.
My question would be: What should I use in Mathlib to represent the permutation so that (1) I can operate on the actual permutation like a List T where I can take or swap elements, and (2) embed the property that it is indeed a permutation within the type.

Thanks!

---

Some context of what I'm trying to do:

1. Have some way of representing permutations of (all) elements in T (currently I knew I can use List T)
2. Define equivalence between two permutations based on some domain specific logic (so something like Equiv: List T -> List T -> Prop)
3. Define a partial order on T, and measure the "unorderness" in a permutation (something like: f: List T -> Nat)
4. Define operations that can transform one permutation to another (g: List T -> List T) that maintains equivalence and alter the "unorderness".
5. Proving that for certain permutations, there exists an equivalent permutation with certain "unorderness".

[Henrik Böving]

How about docs#List.Perm

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

You could also consider the type of equivalences T ≃ T.

[Mario Carneiro]

which is docs#Equiv.Perm

[Zhuanhao Wu]

thanks! i will give it a try