Simproc for permuting vector components

Stream: Is there code for X?

[Oliver Nash]

Could we have a simproc to prove things like these:

import Mathlib.GroupTheory.Perm.Cycle.Concrete
import Mathlib.Tactic.FinCases

example {α : Type*} {a b c : α} :
    ![a, b, c] ∘ Equiv.swap 0 1 = ![b, a, c] := by
  ext a; fin_cases a <;> rfl

example {α : Type*} {a b c : α} :
    ![a, b, c] ∘ Equiv.swap 0 2 = ![c, b, a] := by
  ext a; fin_cases a <;> rfl

example {α : Type*} {a b c : α} :
    ![a, b, c] ∘ c[0, 1] = ![b, a, c] := by
  ext a; fin_cases a <;> rfl

example {α : Type*} {a b c : α} :
    ![a, b, c] ∘ c[2, 0, 1] = ![b, c, a] := by
  ext a; fin_cases a <;> rfl

example {α : Type*} {a b c d : α} :
    ![a, b, c, d] ∘ c[2, 3, 0, 1] = ![b, c, d, a] := by
  ext a; fin_cases a <;> rfl

[Aaron Liu]

the proof is docs#FinVec.etaExpand_eq now just need to hook it up to a simproc

[Yakov Pechersky]

Does decide work?

[Oliver Nash]

Yakov Pechersky said:

Does decide work?

Sadly no!

[Oliver Nash]

@Aaron Liu I see great, you're pointing out the following works:

import Mathlib.Data.Fin.Tuple.Reflection
import Mathlib.GroupTheory.Perm.Cycle.Concrete
import Mathlib.Tactic.FinCases

variable {α : Type*} {a b c d : α}

example : ![a, b, c] ∘ Equiv.swap 0 1 = ![b, a, c] :=
  (FinVec.etaExpand_eq _).symm

example : ![a, b, c] ∘ Equiv.swap 0 2 = ![c, b, a] :=
  (FinVec.etaExpand_eq _).symm

example : ![a, b, c] ∘ c[0, 1] = ![b, a, c] :=
  (FinVec.etaExpand_eq _).symm

example : ![a, b, c] ∘ c[2, 0, 1] = ![b, c, a] :=
  (FinVec.etaExpand_eq _).symm

example : ![a, b, c, d] ∘ c[2, 3, 0, 1] = ![b, c, d, a] :=
  (FinVec.etaExpand_eq _).symm

Who wants to hook it up?

[Paul Lezeau]

Happy to do that (unless you’ve already started @Aaron Liu ?)

[Aaron Liu]

no I haven't started yet

[Paul Lezeau]

(got a little distracted by other things, but here it is): #33129