More canonical maps

This MR:

• Provides new implementations of gmap/gset, Pmap/Pset, Nmap/Nset and Zmap/Zset based on the "canonical" version of binary tries by Appel and Leroy (see https://inria.hal.science/hal-03372247) that avoid the use of Sigma types and enjoy:
  • More definitional equalities, because maps are no longer equipped with a proof of canonicity. This means more equalities can be proved by reflexivity or even by conversion as part of unification. For example, {[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]} and {[ 1 ]} ∖ {[ 1 ]} = ∅ hold definitionally.
  • The use in nested recursive definitions. For example, Inductive gtest := GTest : gmap nat gtest → gtest. (The old map types would violate Coq's strict positivity condition due to the Sigma type.)
• Makes map_fold a primitive of the FinMap, and derive map_to_list from it. (Before map_fold was derived from map_to_list.) This makes it possible to use map_fold in nested-recursive definitions on maps. For example, Fixpoint f (t : gtest) := let 'GTest ts := t in map_fold (λ _ t', plus (f t')) 1 ts.

This MR contains a bunch of tests:

• To show that we indeed have more definitional equalities that can be proved by reflexivity.
• We can use gmap and pmap in nested recursive definitions.
• Computations with vm_compute on "big" pmap/gmaps (size >100.000), which would only terminate if the complexity is n-log-n.
• Compared to the old versions, the computations with vm_compute are slightly faster.
• Computations with reflexivity on small pmap/gmaps (size 1000), showing that the even with Coq's naive reduction computation is reasonable (<1 second).
• More tests for simpl/cbn for Pmap (and a fix akin to Opaque gmap_empty to make those work). We also should have such tests for Pset, but I leave that for a future MR.

/cc @amintimany since we were chatting about this during the PKVM meeting in Aarhus.

This MR only changes implementation details, so should be backwards compatible. (Unless people crafted their own map implementations, or rely on internals of the maps representations.) I tested it on Iris and Iris-examples, which both go through without changes.

@jung Could you run CI that this is the case for all reverse dependencies? Preferably with timing, so that we can see that it does not accidentally make anything slower. (While I do not expect that, we had some unexpected issues in !309 (merged)).

added 5 commits

• c25c071e - Change implementation of `Pmap` and replace `map_to_list` with `map_fold`.
• 229dcd00 - New `gmap`.
• 317b9b2d - Make `Pmap_empty` opaque, similar to `gmap_empty`.
• 3b527d89 - Add tests.
• 18fd8b75 - CHANGELOG.

Compare with previous version

added 3 commits

• 8701db95 - Add tests.
• df29b980 - CHANGELOG.
• bde5f728 - A more complicated test.

Compare with previous version

added 1 commit

• 4c879a79 - A more complicated test.

Compare with previous version

I added a new test, proving:

Inductive gtest K `{Countable K} := GTest : gmap K (gtest K) → gtest K.
Global Program Instance gtest_countable `{Countable K} : Countable (gtest K).
Goal {[ GTest {[ 1 := GTest ∅ ]} ]} ≠@{gset (gtest nat)} {[ GTest ∅ ]}.
Proof. discriminate. Qed.
Goal GTest {[ GTest {[ 1 := GTest ∅ ]} := GTest ∅ ]} ≠@{gtest (gtest nat)} GTest ∅.
Proof. discriminate. Qed.

The statements might look trivial, but they are not.

• gtest is parametric in any countable type K, and Coq accepts it.
• proving gtest_countable requires some tricky nested recursive definitions (for encode/decode) and inductive proofs (for showing that they are inverses), which are also accepted by Coq.
• we can thus use types such as gset (gtest nat) and gtest (gtest nat)
• and have proper definitional equalities for these types!

Makes map_fold a primitive of the FinMap, and derive map_to_list from it. (Before map_fold was derived from map_to_list.) This makes it possible to use map_fold in nested-recursive definitions on maps. For example, Fixpoint f (t : gtest) := let 'GTest ts := t in map_fold (λ _ t', plus (f t')) 1 ts.

Is this an either-or tradeoff? As in, if I wanted to use map_to_list in nested-recursive definitions, does the new arrangement become a problem?

Could you run CI that this is the case for all reverse dependencies? Preferably with timing, so that we can see that it does not accidentally make anything slower. (While I do not expect that, we had some unexpected issues in !309 (merged)).

I have triggered the check builds.

Timing runs are not automated for std++ MRs, unfortunately. You'd have to generate an opam release with this version, and then make an Iris MR that switches to that std++, and then I can benchmark that Iris MR.

added 9 commits

• 4c879a79...52a72f29 - 3 commits from branch master
• e8b81d7f - Change implementation of `Pmap` and replace `map_to_list` with `map_fold`.
• 18e937a2 - New `gmap`.
• f76bf714 - Make `Pmap_empty` opaque, similar to `gmap_empty`.
• a818693f - Add tests.
• 317b16be - CHANGELOG.
• 760c1840 - A more complicated test.

Compare with previous version

Two build failures came back:

• https://gitlab.mpi-sws.org/iris/lambda-rust/-/pipelines/80889
• https://gitlab.mpi-sws.org/iris/simuliris/-/pipelines/80897

added 14 commits

• 760c1840...2febd0b9 - 6 commits from branch master
• e72bee6f - Change implementation of `Pmap` and replace `map_to_list` with `map_fold`.
• 9c7afdc8 - New `gmap`.
• e1677409 - Make `Pmap_empty` opaque, similar to `gmap_empty`.
• 169035cd - Add tests.
• 3002ace9 - CHANGELOG.
• 2f936b6f - A more complicated test.
• 08a41ce8 - Add `Strategy` for `map_fold` to avoid eager unfolding.
• e390786f - Tweak comments.

Compare with previous version

added 1 commit

• 8038fc37 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

added 1 commit

• 74510021 - Apply 3 suggestion(s) to 2 file(s)

Compare with previous version

added 38 commits

• 74510021...385d29dd - 30 commits from branch master
• e8b9997c - Change implementation of `Pmap` and replace `map_to_list` with `map_fold`.
• 570272d4 - New `gmap`.
• 789bb0e1 - Make `Pmap_empty` opaque, similar to `gmap_empty`.
• 7fc78a01 - Add tests.
• ea8d1cca - Add `Strategy` for `map_fold` to avoid eager unfolding.
• aaae0be8 - CHANGELOG.
• b3c193c1 - Tweak comments.
• 9d444a80 - Ralf's comments.

Compare with previous version