Stream: math-comp users

Topic: Coq not computing catf


view this post on Zulip 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])).

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 19:48):

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

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 19:57):

People always mention CoqEAL.

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 20:24):

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.

view this post on Zulip 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