Draft: add lemma lookup_insert_eq

For most map operations we have a lemma lookup_foo that always applies -- except, ironically, for insert.

Unfortunately the lemma really should be called lookup_insert, but that name is already taken, so I called it lookup_insert_eq. Arguably that would be a good name for the i = j case and nicely symmetric with lookup_insert_ne (well, the really symmetric version would take i = j as precondition, which can make it easier to rewrite with). lookup_insert is used a lot so I feel renaming might be a bit too disruptive...

I am strongly in favor of having these lemmas that apply without i = j/i ≠ j condition, but instead use an if/match.

I think we should use lookup_foo for the general lemma, and lookup_foo_eq and lookup_foo_ne for the =/≠ version.

You are right, such a change is disruptive, but it can very easily be done by sed. I would be in favor of batching all these changes, so add the general versions for all lookup lemmas and make their makes consistent in one go. Then this disruption happens once, and running a sed script that performs one rename or many does not really make a difference.

I don't think it's just insert where the general lemma is missing. From a brief look, I also see lookup_alter, lookup_delete, lookup_partial_alter, lookup_singleton.

Yeah, I agree that's the right change. Unfortunately I don't currently have the time to pursue that. Should we leave this MR open as a reminder to get back to that problem when one of us has the time?

What's your stance on <[i:=v]> m !! i = Some v vs i = j → <[i:=v]> m !! j = Some v? That can't be seded, but it might be worth having both of these lemmas, if we're touching this theory anyway.

Should we leave this MR open as a reminder to get back to that problem when one of us has the time?

Sounds fine.

What's your stance on <[i:=v]> m !! i = Some v vs i = j → <[i:=v]> m !! j = Some v?

Once we have the general lemmas, is it worth having the second? You can do rewrite lookup_insert decide_True, and that generates the side condition.

That said, without the general lemma, I don't know how to emulate the second easily, apart from performing a replace of i and j, say rewrite (_ : i = j), first. So I can imagine not having it, when you need it, is very annoying.

You can do rewrite lookup_insert decide_True, and that generates the side condition.

Ah yeah that works too. It might be a little harder to discover, but uses common enough patterns that it doesn't seem worth a separate lemma, at least for now (assuming we have the general lemma).

marked this merge request as draft

mentioned in merge request !526 (merged)

Closing in favor of !526 (merged).

closed

mentioned in merge request !532