Zulip Chat Archive

Stream: Is there code for X?

Topic: list.update_same


view this post on Zulip Marcus Rossel (Mar 04 2021 at 07:27):

Is there something like: ?

lemma list.update_same {α : Type*} (l : list α) (n : ) (a a' : α) :
  (l.update_nth n a).update_nth n a' = l.update_nth n a'

view this post on Zulip Yakov Pechersky (Mar 04 2021 at 13:47):

As always, induction is your friend:

lemma list.update_same {α : Type*} (l : list α) (n : ) (a a' : α) :
  (l.update_nth n a).update_nth n a' = l.update_nth n a' :=
begin
  induction l with hd tl hl generalizing n,
  { simp [list.update_nth] },
  { cases n,
    { simp [list.update_nth] },
    { simp [list.update_nth, hl] } }
end

Last updated: May 19 2021 at 00:40 UTC