Hi. Why is it that Coq can't compute the following?

```
From mathcomp Require Import all_ssreflect finmap.
Local Open Scope fset.
Local Open Scope fmap.
Compute (domf (fmap0 + fmap0.[0 <- 0])).
```

math-comp often isn't designed for computation; sealing tends to get in the way

Is there a way to make it compute? Can it be unsealed? Is it extractable to OCaml or Haskell?

People always mention CoqEAL.

Paolo Giarrusso said:

People always mention CoqEAL.

As an example of code based in mathcomp that computes or is extractable?

https://github.com/coq-community/coqeal links to https://hal.inria.fr/hal-00734505/document among others

We describe a step-by-step approach to the implementation and formal verification of efficient algebraic algorithms. Formal specifications are expressed on rich data types which are suitable for deriving essential theoretical properties. These specifications are then refined to concrete implementations on more efficient data structures and linked to their abstract counterparts. We illustrate this methodology on key applications: matrix rank computation, Winograd’s fast matrix product, Karatsuba’s polynomial multiplication, and the gcd of multivariate polynomials.

A good work-around is often to have an adhoc rewrite simplifier.

```
From mathcomp Require Import all_ssreflect finmap.
Local Open Scope fset.
Local Open Scope fmap.
Definition my_simpl := (cat0f, domf0, fsetU0, dom_setf).
Goal forall x, (domf ([fmap] + [fmap].[0 <- 0])) = x.
move=> x; rewrite !my_simpl.
```

```
```

Last updated: Jul 23 2024 at 21:01 UTC