Building a list of lists in a type with given lengths

Stream: Is there code for X?

[Antoine Chambert-Loir]

In order to compute the cardinality of the conjugacy classes of permutations in a given Fintype α

theorem Equiv.Perm.card_of_cycleType_mul_eq (m : Multiset ℕ) :
    (Finset.univ.filter fun g : Equiv.Perm α => g.cycleType = m).card *
        ((Fintype.card α - m.sum).factorial * m.prod *
          (m.dedup.map fun n : ℕ => (m.count n).factorial).prod) =
      ite (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) (Fintype.card α).factorial 0 := by sorry

one step requires to know whenever m : Multiset ℕ is realized as the Equiv.Perm.cycleType of some permutation g : Equiv.Perm α:

theorem Equiv.permWithCycleType_nonempty_iff {m : Multiset ℕ} :
    Set.Nonempty { g : Equiv.Perm α | g.cycleType = m).Nonempty ↔
      (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) := by sorry

For this, it is needed to construct, given m :Multiset ℕ such that m.sum ≤ Fintype.card α , some l : List (List α) with pairwise distinct members and whose lengths are given by m = l.map length. The first thing I do is defining this function

/-- From `l: List ℕ`, construct `ml: List (List ℕ)` such that
  `ml.map List.length = l` and `ml.join = range l.sum` -/
def List.ranges : List ℕ → List (List ℕ)
  | [] => List.nil
  | a::l => List.range a::List.map (List.map (Nat.add a)) (List.ranges l)

that turns, for example, [1,3,2] into [[0], [1,2,3],[4,5]] and then prove what you can guess, so that this list of lists
becomes a permutation of Fin 6, and then of Fin α.
All in all, this is quite long, and I wonder whether there could have been an obvious approach…

[Antoine Chambert-Loir]

(The whole stuff that proves the first function and its companion for the alternating group will be made into a bunch of PRs, this is around 3000 lines…
If people are interested, that's here :
https://github.com/AntoineChambert-Loir/Jordan4/blob/main/Jordan/ConjClassCount.lean)

[Eric Wieser]

Is there any useful connection to docs#List.Nat.antidiagonalTuple here?

[Antoine Chambert-Loir]

I don't see any obvious one…

[Eric Wieser]

The web editor is down so I haven't tested this, but this seems a bit nicer:

def List.multiSplit : List α → List ℕ → List (List α)
  | _l, [] => List.nil
  | l, i::is => let (h, t) := l.splitAt i; h :: t.multiSplit is

which gives

#eval ["this", "should", "work"].multiSplit [0, 2, 0, 1]
-- [[], ["this", "should"], [], ["work"]]

[Antoine Chambert-Loir]

Thanks, it looks good but the subsequent proofs are not really easier. I'll think about it…