list.update_nth_comm

Stream: Is there code for X?

[Marcus Rossel]

There exists a very nice lemma called function.update_comm. Is there something analogous for list.update_nth - i.e. a lemma that proves that list.update_nth is commutative if the updated indices aren't equal?

[Alex J. Best]

Looks like list.update_nth is missing a bunch of lemmas really.

@[simp]
lemma list.update_nth_nil (α : Type) (n : ℕ) (a : α) : [].update_nth n a = [] := rfl
lemma list.update_nth_comm (α : Type) (a b : α) : Π (n m : ℕ) (h : n ≠ m) (l : list α),
(l.update_nth n a).update_nth m b =
(l.update_nth m b).update_nth n a
| _ _ _ [] := by simp
| 0 0 h (x :: t) := absurd rfl h
| (n + 1) 0 h (x :: t) := by simp [list.update_nth]
| 0 (m + 1) h (x :: t) := by simp [list.update_nth]
| (n + 1) (m + 1) h (x :: t) := by { simp [list.update_nth], exact list.update_nth_comm n m (λ h', h $ nat.succ_inj'.mpr h') t}