# 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.)

- More definitional equalities, because maps are no longer equipped with a
proof of canonicity. This means more equalities can be proved by
- 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.

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