Zulip Chat Archive

Stream: new members

Topic: updating vectors

Marcus Klaas (Dec 11 2018 at 14:02):

Hi! Can anyone provide some pointers here? I'm trying to define a function that updates a vector at a given index. This seems to work, but it's very unwieldy:

def update_nth {n : ℕ} {α : Type} : vector α n → fin n → α → vector α n
| v i a := vector.map₂ (λ b idx, if idx = i then a else b) v $ vector.of_fn id

In particular, proving elementary lemmas on it seems near impossible:

lemma update_nth_helper {n : ℕ} {α : Type} (v : vector α n) (i : fin n) (a b : α)
    : vector.cons b (update_nth v i a) = update_nth (vector.cons b v) (fin.succ i) a :=
sorry

I'd like to provide a recursive definition, but I can't get it to work. Lean seems to think n is fixed.

Any tips on best approach here?

Mario Carneiro (Dec 11 2018 at 14:11):

another way to define that function is using vector.nth with vector.of_fn

Mario Carneiro (Dec 11 2018 at 14:11):

or by referring to list.update_nth

Marcus Klaas (Dec 11 2018 at 14:12):

ooh, there is a list.update_nth? hadn't seen that! thanks!

Mario Carneiro (Dec 11 2018 at 14:12):

as for n fixed, that happens when you put it left of the colon

Marcus Klaas (Dec 11 2018 at 14:13):

I'd like to put it right of the colon, but then I cannot name it any more, correct?

Mario Carneiro (Dec 11 2018 at 14:13):

sure you can

Marcus Klaas (Dec 11 2018 at 14:13):

and almost all other arguments depend on it :o

Marcus Klaas (Dec 11 2018 at 14:13):

oh wow

Marcus Klaas (Dec 11 2018 at 14:13):

i feel silly now

Marcus Klaas (Dec 11 2018 at 14:14):

can u provide 1 more hint on how vector.nth + vector.of_fn would work?

Marcus Klaas (Dec 11 2018 at 14:22):

list.update_nth worked beautifully btw - thanks a million mario!

Rob Lewis (Dec 11 2018 at 14:25):

I guess Mario might have been thinking of something like vector.of_fn (λ k, if k = n then a else v.nth k).

Rob Lewis (Dec 11 2018 at 14:26):

Depending on your application here, you might consider using array instead of vector.

Marcus Klaas (Dec 11 2018 at 14:33):

:O

Marcus Klaas (Dec 11 2018 at 14:33):

what's the trade-off?

Mario Carneiro (Dec 11 2018 at 14:35):

array is already basically functions from fin n

Mario Carneiro (Dec 11 2018 at 14:36):

it's also more efficient for computational purposes, dunno if that matters

Mario Carneiro (Dec 11 2018 at 14:36):

plus this function already exists on array, it's called array.write and it's the most basic array function (everything else is in terms of it) so you should be in a good place wrt lemmas

Marcus Klaas (Dec 11 2018 at 14:37):

i like that

Marcus Klaas (Dec 11 2018 at 14:37):

thanks a bunch folks!

Marcus Klaas (Dec 11 2018 at 14:39):

can't wait to see your presentation on p-adic numbers this thursday btw @Rob Lewis :-)

Rob Lewis (Dec 11 2018 at 14:42):

Hmm, yeah, I should finish those slides at some point.

Marcus Klaas (Dec 11 2018 at 14:44):

^^

Last updated: Dec 20 2023 at 11:08 UTC