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.

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.

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

@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.

@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)
```

this means that the `Float64`

module will be available inside your project to `open`

or use otherwise

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

Thank you @Karl Palmskog

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

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

that sounds really helpful.

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?

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

okay, thanks! :)

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.

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