New `seq` operation on maps + consistency tweaks for `seq` operation on sets

Merged Robbert Krebbers requested to merge robbert/map_seq into master

This MR introduces a seq operation on maps, which turns a list x_0; ...; x_n into a map:

{[ i := x_0; ... i+n := x_n ]}

On top of that, I made various improvements to the already existing seq operation on sets:

  • Rename it from seq_set into set_seq. Having _set as a suffix instead of a prefix is inconsistent, see also #24 (closed). This is done as part of !45 (merged) now.
  • Provide set_solver support for set_seq.
  • Make the lemmas for set_seq more consistent w.r.t. those for maps.

Due to the rename, it is not backwards compatible. I'm happy to fix Iris and friends.

Edited by Robbert Krebbers

Merge request reports