More canonical maps
This MR:
- Provides new implementations of
gmap
/gset
,Pmap
/Pset
,Nmap
/Nset
andZmap
/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 theFinMap
, and derivemap_to_list
from it. (Beforemap_fold
was derived frommap_to_list
.) This makes it possible to usemap_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
andpmap
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 smallpmap
/gmap
s (size 1000), showing that the even with Coq's naive reduction computation is reasonable (<1 second). - More tests for
simpl
/cbn
forPmap
(and a fix akin toOpaque gmap_empty
to make those work). We also should have such tests forPset
, but I leave that for a future MR.
/cc @amintimany since we were chatting about this during the PKVM meeting in Aarhus.