Add lemma lookup_gmap_uncurry_empty

This lemma is needed to completely characterize what gmap_uncurry is.

Sounds like a useful addition.

Note that for most other operations we have similar lemmas, for example:

Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
  alter f i m !! j = None ↔ m !! j = None.
Lemma lookup_delete_None {A} (m : M A) i j :
  delete i m !! j = None ↔ i = j ∨ m !! j = None.

It would be good if the lemma were in the same style, i.e.:

• The name should be suffixed _None, it has nothing to do with the empty map after all.
• It should be proven as a bi-implication.

added 1 commit

• 13c7d213 - Add lemma lookup_gmap_uncurry_empty

Compare with previous version

Updated. Any other comment?

mentioned in commit a485dd7d

merged

LGTM! Merged, and thanks for the MR.

PS: I would be good to also have the _Some and _is_Some variants of these lemmas, as well as lemmas about the interaction with other finite map functions like delete, insert, alter, and so on. Similarly for curry.

PS: I would be good to also have the _Some and _is_Some variants of these lemmas, as well as lemmas about the interaction with other finite map functions like delete, insert, alter, and so on. Similarly for curry.

Sure. The _None is however more important because it cannot be proved without breaking the abstraction.