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

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.

I don't think I can give meaningful feedback here, since I've never used seq.

Ok, but any concerns w.r.t. renaming seq_set into set_seq, and the relation to #24 (closed).

My only concern is to please keep the amount of renaming to a minimum :) This always has a long-term cost, and while you can fix our projects you cannot fix external reverse dependencies.

This one will probably not affect many people, seq is not used a lot.

However, I would like to avoid having to rename it again if we decide for something else then consistently using the set_ prefix in #24 (closed).

I think consistently using set everywhere instead of collection is a viable long-term goal (from what I understand, that means less renaming than alternative of using collection everywhere).

added 42 commits

• 3d3b6401...17f8c792 - 34 commits from branch master
• 17ab3cd6 - Consistently use `set_` prefix.
• f3c0d3fd - Better names for convertion functions from `gset` and `coPset`.
• f9388e88 - Function `map_seq` to turn a list into a finite map of consequentive elements.
• 3f57311f - Make `set_seq` lemmas for consistent w.r.t. those of maps.
• 3f0bf48f - Relation between `map_seq` and `set_seq`.
• d5133dac - Support `set_seq` in `set_solver`.
• 22efedf0 - Relation between `set_seq` and `seq`.
• 44ec0438 - `set_seq` is finite.

Compare with previous version

I have updated this MR. It's based on top of !44 (merged) now.

changed the description

It's based on top of !44 (merged) now.

Could you provide a link showing just the relevant diff (using the GitLab feature to compare two branches)? I have no idea what to look at here.

changed target branch from master to robbert/set_rename

I have changed the target branch, the diff should show something sensible now.

added 8 commits

• 44ec0438...a3ac6324 - 2 commits from branch robbert/set_rename
• 2b4682f1 - Function `map_seq` to turn a list into a finite map of consequentive elements.
• 41ad2850 - Make `set_seq` lemmas for consistent w.r.t. those of maps.
• 1cbc09b0 - Relation between `map_seq` and `set_seq`.
• 244b4334 - Support `set_seq` in `set_solver`.
• af8da479 - Relation between `set_seq` and `seq`.
• 4d1a385f - `set_seq` is finite.

Compare with previous version

added 12 commits

• 4d1a385f...f5da0c1a - 6 commits from branch robbert/set_rename
• ec57aeab - Function `map_seq` to turn a list into a finite map of consequentive elements.
• 0884415c - Make `set_seq` lemmas for consistent w.r.t. those of maps.
• e5f3e805 - Relation between `map_seq` and `set_seq`.
• c5d7d4d2 - Support `set_seq` in `set_solver`.
• 581cc38d - Relation between `set_seq` and `seq`.
• 9449ec92 - `set_seq` is finite.

Compare with previous version

I have to say I find the name somewhat unintuitive. map_seq sounds like mapping some operation over a seq.

But I also don't have good suggestions. seq_to_map? map_{of,from}_seq?

The name is mainly analogue to:

seq : nat -> nat -> list nat
set_seq : nat -> nat -> C    (* where C is some set of nats *)

Since we are already renaming set_seq, we could all of them into something else. Any propositions?

seq is fine IMO, it's called like that in bash as well... though maybe that's not a good argument.^^

In Python and Rust, this would be called a "range".

So, that means set_seq is also fine to you? But you have doubts about map_seq?

Well, the matching names for seq_seq would be seq_to_set or set_of_seq, I guess.

I find these names pretty weird. The to and of infixes, are typically used in combination with a type. However, seq is not a type, so set_to_seq and set_of_seq make less sense to me.