Zulip Chat Archive

Stream: Is there code for X?

Topic: list.update_nth_comm


view this post on Zulip Marcus Rossel (Jan 16 2021 at 21:28):

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?

view this post on Zulip Alex J. Best (Jan 16 2021 at 22:29):

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}

Last updated: May 07 2021 at 19:12 UTC