# More canonical maps

requested to merge robbert/new_gmap into master

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`/`gmap`s (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`/`gmap`s (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.