Exchanging two adjacent entries of a list

The lists u ++ b :: a :: v and u ++ a :: b :: v have the same entries, except that the two adjacent entries a and b trade places. This file records the induced identification of their index types, which exchanges the two positions u.length and u.length + 1 and fixes every other position. It is used to compare a construction built from a list with the same construction built after exchanging two adjacent entries.

Main definitions

• List.swapIndexEquiv: identify the entries of u ++ b :: a :: v with those of u ++ a :: b :: v.

Main results

• List.val_swapIndexEquiv: the swap exchanges the positions u.length and u.length + 1.
• List.getElem_swapIndexEquiv: the identification sends each entry to the same entry.

def List.swapIndexEquiv {α : Type u_1} (u v : List α) (a b : α) : Fin (u ++ b :: a :: v).length ≃ Fin (u ++ a :: b :: v).length

The equivalence which sends the index of an entry of u ++ b :: a :: v to the index of the same entry of u ++ a :: b :: v. It exchanges the positions u.length and u.length + 1 of the two entries a and b and fixes every other position.

Equations

• u.swapIndexEquiv v a b = (finCongr ⋯).trans (Equiv.swap ⟨u.length, ⋯⟩ ⟨u.length + 1, ⋯⟩)

theorem List.val_swapIndexEquiv {α : Type u_1} (u v : List α) (a b : α) (j : Fin (u ++ b :: a :: v).length) : ↑((u.swapIndexEquiv v a b) j) = if ↑j = u.length then u.length + 1 else if ↑j = u.length + 1 then u.length else ↑j

The swap of indices exchanges the positions u.length and u.length + 1 and fixes every other position.

theorem List.getElem_swapIndexEquiv {α : Type u_1} (u v : List α) (a b : α) (j : Fin (u ++ b :: a :: v).length) : (u ++ b :: a :: v)[↑j] = (u ++ a :: b :: v)[↑((u.swapIndexEquiv v a b) j)]

Looking up an entry of u ++ b :: a :: v and translating its index gives the same entry of u ++ a :: b :: v.

@[simp]

theorem List.swapIndexEquiv_symm {α : Type u_1} (u v : List α) (a b : α) : (u.swapIndexEquiv v a b).symm = u.swapIndexEquiv v b a

The swap of indices of u ++ b :: a :: v is inverse to the swap of indices of u ++ a :: b :: v.