Add list_to_imap and associated theory
We have a function list_to_imap
in Perennial to convert a list to a gmap keyed by index, especially to wrap it in an auth and have ghost state for each element by index in Iris. I should upstream this at some point.
It has the following definition:
(** turn a list into a gmap from its indices to values *)
Definition list_to_imap {A} (l: list A) : gmap nat A :=
list_to_map (imap (λ i x, (i, x)) l).
The most important theorem is that list_to_imap l !! i = l !! i
.