obtaining an index permutation from a `List.Perm`?

Stream: Is there code for X?

[Kim Morrison]

I'd like the following

def idx [BEq α] {l₁ l₂ : List α} (h : l₁ ~ l₂) (i : Nat) : Nat := ...

theorem getElem?_idx [BEq α] [LawfulBEq α] {l₁ l₂ : List α} (h : l₁ ~ l₂) (i : Nat) :
    l₁[h.idx i]? = l₂[i]? := by sorry

allowing index-based arguments about permutations. Do we have this, or something functionally equivalent, somewhere?

[Kim Morrison]

One approach I considered was

def idxAux [BEq α] (l₁ : List (Bool × α)) (l₂ : List α) (i : Nat) : Option Nat :=
  match i, l₂ with
  | 0, [] => some 0
  | 0, x :: _ => l₁.idxOf? (true, x)
  | i + 1, [] => some (i + 1)
  | i + 1, x :: l₂ => idxAux (l₁ := l₁.replace (true, x) (false, x)) (l₂ := l₂) i

def idx [BEq α] [LawfulBEq α] {l₁ l₂ : List α} (h : l₁ ~ l₂) (i : Nat) : Nat :=
  (idxAux (l₁.map ((true, ·))) l₂ i).get sorry

but the proofs seemed pretty annoying.

[Kim Morrison]

(auxiliary theorems, such as getting the inverse function from h.symm, optional :-)

[Markus Himmel]

If you don't need it to be computable, then here is one way to get started:

open List

-- Like `List.Perm` but data
inductive List.Perm' {α : Type u} : List α → List α → Type u where
  | nil : [].Perm' []
  | cons (x : α) {l₁ l₂ : List α} : Perm' l₁ l₂ → Perm' (x :: l₁) (x :: l₂ )
  | swap (x y : α) (l : List α) : Perm' (y :: x :: l) (x :: y :: l)
  | trans {l₁ l₂ l₃} : Perm' l₁ l₂ → Perm' l₂ l₃ → Perm' l₁ l₃

theorem List.Perm'.perm : {l₁ l₂ : List α} → Perm' l₁ l₂ → l₁ ~ l₂
  | _, _, nil => Perm.nil
  | _, _, cons x p => Perm.cons x p.perm
  | _, _, swap x y l => Perm.swap x y l
  | _, _, trans p q => Perm.trans p.perm q.perm

theorem List.Perm.perm' {l₁ l₂ : List α} (h : l₁ ~ l₂) : Nonempty (Perm' l₁ l₂) := by
  induction h with
  | nil => exact ⟨Perm'.nil⟩
  | cons _ _ p =>
    rcases p with ⟨pp⟩
    exact ⟨Perm'.cons _ pp⟩
  | swap => exact ⟨Perm'.swap _ _ _⟩
  | trans _ _ p q =>
    rcases p with ⟨pp⟩
    rcases q with ⟨qq⟩
    exact ⟨Perm'.trans pp qq⟩

def List.Perm'.idx : {l₁ l₂ : List α} → Perm' l₁ l₂ → Nat → Nat
  | _, _, nil, n => n
  | _, _, cons x p, n => if n = 0 then 0 else p.idx (n - 1) + 1
  | _, _, swap x y l, n => if n = 0 then 1 else if n = 1 then 0 else n
  | _, _, trans p q, n => p.idx (q.idx n)

theorem List.Perm'.getElem?_idx : {l₁ l₂ : List α} → (h : Perm' l₁ l₂) → (i : Nat) → l₁[h.idx i]? = l₂[i]?
  | _, _, nil, i => by simp
  | _, _, cons x p, i => by
    rw [idx]
    split
    · simp_all
    · rw [getElem?_cons_succ, getElem?_idx]
      rw (occs := [2]) [(show i = (i - 1) + 1 by omega)]
      rw [getElem?_cons_succ]
  | _, _, swap x y l, i => by
    rw [idx]
    split <;> (try split)
    · simp_all
    · simp_all
    · rw [(show i = (i - 2) + 2 by omega)]
      simp only [getElem?_cons_succ]
  | _, _, trans p q, i => by rw [idx, p.getElem?_idx, q.getElem?_idx]

noncomputable def List.Perm.idx {l₁ l₂ : List α} (h : l₁ ~ l₂) (i : Nat) : Nat :=
  (Classical.choice h.perm').idx i

theorem List.Perm.getElem?_idx {l₁ l₂ : List α} (h : l₁ ~ l₂) (i : Nat) :
    l₁[h.idx i]? = l₂[i]? := by
  rw [idx, List.Perm'.getElem?_idx]

I think this recovers your approach if instead of any permutation you pick the lexicographically smallest one.