perf: improves the performance of the Repr (Equiv.Perm α) instance (2/4)

[Komyyy]

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, ⋯⟩

---

• depends on: [Merged by Bors] - perf: improves the performance of the Repr (Equiv.Perm α) instance (1/4) #20519

[github-actions]

PR summary f7513f9d14

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - perf: improves the performance of the Repr (Equiv.Perm α) instance (1/4) #20519
  By Dependent Issues (🤖). Happy coding!

[Komyyy]

@YaelDillies I wrote the comprehensible PR message.

[YaelDillies]

Can you provide some before/after comparison of timing?

[Komyyy]

@YaelDillies Sorry for late, I've written the PR description in #12610.

Even if we fix instance [Fintype α] [DecidableEq α] : DecidableRel (SameCycle (f : Equiv.Perm α)) in #12610, #eval (c[0, 1] * c[2, 3] * c[4, 5] * c[6, 7] * c[8, 9] : Equiv.Perm (Fin 10)) timeouts before this change.
This is immediately evaluated after this change and #12610.

[YaelDillies]

Okay great!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.