Hi. We have been using for some time extraction from Coq to OCaml for an algorithm that uses the reals from the Coq standard library. So far, we could get along with the following commands:

```
Extract Inlined Constant R => "float".
Extract Inlined Constant R0 => "0.".
Extract Inlined Constant R1 => "1.".
Extract Constant Rmult => "( *.)".
...[you get the idea]...
```

Coq 8.11 complains about the following things:

```
In module RbaseSymbolsImpl:
# The value `coq_R1' is required but not provided
```

(which can be dealt with by removing "Inlined" though it is not what we want) and the more puzzling

(but definitely related to the recent changes to the Reals library):

```
In module RbaseSymbolsImpl:
Values do not match:
val coq_Rabst : (nat -> q) -> q -> bool
is not included in
val coq_Rabst : cReal -> coq_R
```

I couldn't figure right away how to deal with these errors properly. Can somebody point me at the documentation? Thanks.

affeldt-aist said:

`In module RbaseSymbolsImpl: # The value `coq_R1' is required but not provided`

This looks like a bug of `Inlined`

when the names start with a capital and that a prefix `coq_`

is added to comply with the OCaml lexical convention. I suggest you report it.

`In module RbaseSymbolsImpl: Values do not match: val coq_Rabst : (nat -> q) -> q -> bool is not included in val coq_Rabst : cReal -> coq_R`

How did you implement `RAbst`

? You have to give it the type `(nat -> q) -> float`

as far as I can judge.

PS1: How do you intend to implement the (classical) "decidability" of equality on `R`

?

PS2: You may be interested in the ongoing work of @MSoegtropIMC and @Vincent Semeria to attach an exact-precision computational layer to `R`

(e.g. PR #12186 as part of it).

This looks like a bug... I suggest you report it.

Thank you for your feeback, I opened an issue.

How did you implement RAbst?

I don't think we have ever implemented `Rabst`

. It seems to come from the standard library: https://coq.inria.fr/stdlib/Coq.Reals.Rdefinitions.html#RbaseSymbolsImpl.Rabst.

How do you intend to implement the (classical) "decidability" of equality on R?

With the equality on floats provided by OCaml.

You may be interested in the ongoing work ... to attach an exact-precision computational layer to R.

Indeed, this is related. Thank you for the pointer.

I must add that Jacques Garrigue seems to have found a solution by introducing conversions as implemented by `RbaseSymbolsImpl.coq_Rabst`

and `RbaseSymbolsImpl.coq_Rrepr`

(https://github.com/affeldt-aist/infotheo/pull/7/commits/48a7983657ced31d8a3d5ba4734a063b71c9b75d).

(Still, this fix comes with a number of `Extract`

commands for definitions that aren't directly manipulated by the user (https://github.com/affeldt-aist/infotheo/pull/7/commits/814ded3424e2b6c8fce564540dae53a71dd6d709).)

If this fix is right, that makes for a bit more complicated extraction process, which surely must be documented somewhere.

affeldt-aist said:

How do you intend to implement the (classical) "decidability" of equality on R?

With the equality on floats provided by OCaml.

Does the approximation with floats produce reasonably correct results? Maybe could your extraction glue be added as an example of `extraction`

in the `theories/extraction/`

repository of the archive (with a large warning about the approximation).

affeldt-aist said:

I must add that Jacques Garrigue seems to have found a solution by introducing conversions as implemented by

`RbaseSymbolsImpl.coq_Rabst`

and`RbaseSymbolsImpl.coq_Rrepr`

(https://github.com/affeldt-aist/infotheo/pull/7/commits/48a7983657ced31d8a3d5ba4734a063b71c9b75d).

Good if you found a solution. My guess is otherwise that if you override all of the `RbaseSymbolsImpl`

module, you don't need to change anything in `ConstructiveCauchyReals.CReal`

and `ClassicalDedekindReals.DReal`

which are sublayers of `RbaseSymbolsImpl`

(but I did not check).

And if so, for `Rabst`

and `Rrepr`

, I suspect that you can `assert false`

.

But since `RbaseSymbolsImpl`

refers to `CReal`

, I don't see how to avoid the `CReal`

code to be extracted, even though it is useless for you.

Last updated: Jun 20 2024 at 11:02 UTC