Hi, I was trying to compute in Coq with the finmaps from math-comp but I immediatly ran into a performance problem.

Is it generally possible to compute with them and does anyone have experience with it, maybe I'm doing something totally wrong? Using the functor based ones from the coq stdlib works fine, though, so it's not a big problem if I can't use it.

I tested the below code on (coq 8.13.0, coq-mathcomp-ssreflect 1.12.0, coq-mathcomp-finmap 1.5.1) and (coq 8.9.1, coq-mathcomp-ssreflect 1.11.0, coq-mathcomp-finmap 1.5.0)

```
From mathcomp Require Import all_ssreflect finmap.
Section t.
Open Scope fmap.
Definition empty := [fmap of bool_choiceType -> nat].
Check empty.
(* 11 sec on my laptop *)
Time Compute (empty.[? true]).
Definition mymap := [fmap].[true <- 1].
Check mymap.
(* OOM after quite some time *)
Time Compute (mymap.[? true]).
```

As far as I know you cannot indeed compute them easily, in particular the definition uses choice to make the map extensional which is not going to work.

The usual approach is to refine the fmap to an efficient map and compute with it, there are some other libraries such as the one by @Arthur Azevedo de Amorim which do compute better, at the expense of requiring you base type to implement an order operation

Last updated: Jul 15 2024 at 21:02 UTC