## Stream: math-comp users

### Topic: Coq not computing catf

#### Ricardo (Feb 23 2023 at 19:42):

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

#### Paolo Giarrusso (Feb 23 2023 at 19:48):

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

#### Ricardo (Feb 23 2023 at 19:52):

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

#### Paolo Giarrusso (Feb 23 2023 at 19:57):

People always mention CoqEAL.

#### Ricardo (Feb 23 2023 at 20:09):

Paolo Giarrusso said:

People always mention CoqEAL.

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

#### Paolo Giarrusso (Feb 23 2023 at 20:24):

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.

#### Laurent Théry (Feb 23 2023 at 21:58):

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