## Stream: Is there code for X?

### Topic: list.update_nth_same

#### 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


#### 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

#### Marcus Rossel (Mar 09 2021 at 20:03):

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

#### Ruben Van de Velde (Mar 09 2021 at 20:07):

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

#### 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.

#### Kevin Buzzard (Mar 10 2021 at 07:18):

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

#### Marcus Rossel (Mar 10 2021 at 07:19):

That's the first post in this thread :D

#### Kevin Buzzard (Mar 10 2021 at 07:26):

The joys of reading on mobile. Sorry :-)

#### 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