list.update_nth_same

Stream: Is there code for X?

[Marcus Rossel]

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]

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]

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

[Ruben Van de Velde]

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

[Marcus Rossel]

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

[Kevin Buzzard]

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

[Marcus Rossel]

That's the first post in this thread :D

[Kevin Buzzard]

The joys of reading on mobile. Sorry :-)

[Yakov Pechersky]

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