Zulip Chat Archive

Stream: Is there code for X?

Topic: list.update_nth_same


view this post on Zulip Marcus Rossel (Mar 09 2021 at 19:31):

Is there something like: ?

lemma list.update_nth_same {α : Type*} (l : list (option α)) (n : ) :
  l.update_nth n (l.nth n).join = l :=
  sorry

view this post on Zulip Mario Carneiro (Mar 09 2021 at 19:51):

the .join there is weird (not to mention quite limiting on the types). I would instead look for a \in l.nth n -> l.update_nth n a = l

view this post on Zulip Marcus Rossel (Mar 09 2021 at 20:03):

What does a ∈ l.nth n mean, if l.nth n : option?

view this post on Zulip Ruben Van de Velde (Mar 09 2021 at 20:07):

l.nth n = some a, I believe. (Don't remember why \in is better)

view this post on Zulip Marcus Rossel (Mar 10 2021 at 07:11):

Ok, then there's a difference. I still want the lemma to work for n > l.length.

view this post on Zulip Kevin Buzzard (Mar 10 2021 at 07:18):

Why not formalise the statement you want and post a #mwe with a sorry?

view this post on Zulip Marcus Rossel (Mar 10 2021 at 07:19):

That's the first post in this thread :D

view this post on Zulip Kevin Buzzard (Mar 10 2021 at 07:26):

The joys of reading on mobile. Sorry :-)

view this post on Zulip Yakov Pechersky (Mar 10 2021 at 13:49):

import data.list.basic

lemma list.update_nth_same {α : Type*} (l : list (option α)) (n : ) :
  l.update_nth n (l.nth n).join = l :=
begin
  ext k,
  by_cases hk : k = n,
  { cases h : l.nth n;
    simp [list.nth_update_nth_eq, hk, h] },
  { rw list.nth_update_nth_ne _ l (ne.symm hk) }
end

Last updated: May 07 2021 at 21:10 UTC