Commit 2025-01-24 08:47 ffaf9758

perf: improves the performance of the Repr (Equiv.Perm α) instance (2/4) (#20538) The instance of Repr (Equiv.Perm α) uses the following truncCycleFactors function:

def cycleFactorsAux [DecidableEq α] [Fintype α] (l : List α) (f : Perm α)
    (h : ∀ {x}, f x ≠ x → x ∈ l) :
    { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
  match l with
  | [] => ⟨[], ⋯⟩
  | x :: l =>
    if hx : f x = x then cycleFactorsAux l f ⋯
    else
      let ⟨m, hm⟩ := cycleFactorsAux l ((cycleOf f x)⁻¹ * f) ⋯
      ⟨cycleOf f x :: m, ⋯⟩
def truncCycleFactors [DecidableEq α] [Fintype α] (f : Perm α) :
    Trunc { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
  Quotient.recOnSubsingleton
    (motive := fun m =>
      (∀ x, f x ≠ x → x ∈ m) →
        Trunc { l // l.prod = f ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l })
    (Finset.univ : Finset α).val
    (fun l h => Trunc.mk (cycleFactorsAux l f ⋯))
    ⋯

However, for a permutation consisted of many disjoint cycles, like (c[0, 1] * c[2, 3] * c[4, 5] * c[6, 7] : Equiv.Perm (Fin 10)), evaluating returned permutations takes too long. This is because the argument f in cycleFactorsAux gets more complex per step; f to (cycleOf f x)⁻¹ * f. To solve this problem, we memorize the first permutation:

def cycleFactorsAux [DecidableEq α] [Fintype α]
    (l : List α) (f : Perm α) (h : ∀ {x}, f x ≠ x → x ∈ l) :
    { pl : List (Perm α) // pl.prod = f ∧ (∀ g ∈ pl, IsCycle g) ∧ pl.Pairwise Disjoint } :=
  go l f ⋯ ⋯
where
  go (l : List α) (g : Perm α) (hg : ∀ {x}, g x ≠ x → x ∈ l)
    (hfg : ∀ {x}, g x ≠ x → cycleOf f x = cycleOf g x) :
    { pl : List (Perm α) // pl.prod = g ∧ (∀ g' ∈ pl, IsCycle g') ∧ pl.Pairwise Disjoint } :=
  match l with
  | [] => ⟨[], ⋯⟩
  | x :: l =>
    if hx : g x = x then go l g ⋯ ⋯
    else
      let ⟨m, hm₁, hm₂, hm₃⟩ := go l ((cycleOf f x)⁻¹ * g) ⋯ ⋯
      ⟨cycleOf f x :: m, ⋯⟩