Stream: Coq users

Topic: extracting coq floats to ocaml


view this post on Zulip Mohit Tekriwal (Jan 03 2024 at 01:24):

Hello, I am trying to extract coq floats to ocaml floats. I have been following the following documentation: https://coq.inria.fr/doc/master/stdlib/Coq.extraction.ExtrOCamlFloats.html which lays down guidelines to extract primitive floats to ocaml floats. However, I am having issues doing so. In particular, I am not completely able to understand what the following instruction says "Note: the extraction of primitive floats relies on Coq's internal file kernel/float64.ml, so make sure the corresponding binary is available when linking the extracted OCaml code." Could some one please help me understanding it.

Concrete example, I have been working with:

From Flocq Require Import PrimFloat Binary BinarySingleNaN.
From Coq Require Import Floats.

Check Compat.ldexp.

Check Prim2B.
Print Prim2B.

Check abs_equiv.

Lemma floats_equiv (x: float) :
  Prim2B (abs x) = Babs (Prim2B x).
Proof. apply abs_equiv. Qed.

Definition two := 2.0 : float.

Lemma two_abs : Prim2B (abs two) = Babs (Prim2B two).
Proof. apply abs_equiv. Qed.

Definition two_add := PrimFloat.add two two.

which is stored in a file exp10.v
and I have the following extract.v file:

From Coq Require Extraction ExtrOCamlFloats.
Extraction Language OCaml.

Require Import exp10.
Separate Extraction exp10.

when I run the extraction, I get the following output in an mli file:

open PrimFloat

val two : Float64.t

val two_add : Float64.t

I was expecting the type float in OCaml.

view this post on Zulip Karl Palmskog (Jan 03 2024 at 08:00):

see here for the runtime for primitive floats: https://github.com/palmskog/coq-primitive

you can see that it's a wrapper for OCaml float in the end, but quite a lot of indirection.

view this post on Zulip Mohit Tekriwal (Jan 03 2024 at 16:57):

Thank you @Karl Palmskog . I will take a look at this.

view this post on Zulip Mohit Tekriwal (Jan 03 2024 at 17:13):

@Karl Palmskog I have a question regarding the usage of files you shared. How do I use it with the extracted ocaml code? The repo does not provide instructions regarding the usage. Could you please help me with it? Thanks.

view this post on Zulip Karl Palmskog (Jan 03 2024 at 17:42):

@Mohit Tekriwal the repo contains an OCaml library. Depending on what build system and/or packaging for your project is, installation and usage is done differently. If you use opam, you can install the library directly from the repo:

opam pin add --kind git https://github.com/palmskog/coq-primitive.git

Then if you are using Dune to compile your OCaml project, you need to add something like this to your dune file:

(libraries coq-primitive.float64)

view this post on Zulip Karl Palmskog (Jan 03 2024 at 17:44):

this means that the Float64 module will be available inside your project to open or use otherwise

view this post on Zulip Karl Palmskog (Jan 03 2024 at 17:46):

see also this issue: https://github.com/coq/coq/issues/15936

view this post on Zulip Mohit Tekriwal (Jan 03 2024 at 18:02):

Thank you @Karl Palmskog

view this post on Zulip Mohit Tekriwal (Jan 03 2024 at 18:20):

I was able to use the coq-primitive development successfully. Thank you for the help.

view this post on Zulip Karl Palmskog (Jan 03 2024 at 19:00):

great that it worked, the plan is to get the package into Coq for the 8.20 cycle

view this post on Zulip Mohit Tekriwal (Jan 03 2024 at 19:04):

that sounds really helpful.

view this post on Zulip Mohit Tekriwal (Jan 03 2024 at 19:06):

one more question though: looking at the coq-primitive, it seems that there is no extraction for transcendental functions from coq to ocaml. Are you aware of any works on that?

view this post on Zulip Karl Palmskog (Jan 03 2024 at 19:07):

Not aware of any work in that direction. My repo is basically just a repackaging of what is already in Coq. I guess you can always add your own extraction directives

view this post on Zulip Mohit Tekriwal (Jan 03 2024 at 19:08):

okay, thanks! :)

view this post on Zulip Pierre Roux (Jan 08 2024 at 12:30):

There is a fundamental reason for the absence of transcendental functions in the kernel. Making correctly rounded such functions is very hard (exhaustive testing can work with binary32 but no way such a naive solution would get you binary64). AFAIK, major implementations are only believed to be correct up to the last few bits, so assuming anything about those functions would be akin to assume False (if one could obtain different results on different platforms, they could be combined in a proof of False). This is known as the tablemaker dillema but I'm no expert on the subject, @Erik Martin-Dorel and @Guillaume Melquiond would know better.

view this post on Zulip Julio Di Egidio (Jan 08 2024 at 13:01):

At least one correct (semi-)formalization exists that I know of:
https://books.google.it/books/about/Global_Optimization_Using_Interval_Analy.html?id=tY2wAkb-zLcC

<< Provided [definitions then] algorithms are guaranteed to find and bound all solutions to these problems despite bounded errors in data, in approximations, and from use of rounded arithmetic. >>

If of interest, I could expand on that a little bit, with few more references plus I do have studied those numbers at least at the level of aiming for an implementation (indeed, FWIW, I still have to see a better solution than that if a solution at all).


Last updated: Jun 23 2024 at 05:02 UTC