Stream: math-comp users

Topic: Performance when computing with finmap

view this post on Zulip Adrian Dapprich (Feb 24 2021 at 15:07):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 24 2021 at 16:32):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 24 2021 at 16:33):

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: Feb 08 2023 at 08:02 UTC