Reynald Affeldt (May 27 2020 at 15:22): Reynald Affeldt (May 27 2020 at 15:22):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.
Hugo Herbelin (May 30 2020 at 13:48):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).
Reynald Affeldt (May 30 2020 at 16:16):This looks like a bug... I suggest you report it.
Thank you for your feeback, I opened an issue.
Reynald Affeldt (May 30 2020 at 16:27):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.
Reynald Affeldt (May 30 2020 at 16:28):How do you intend to implement the (classical) "decidability" of equality on R?
With the equality on floats provided by OCaml.
Reynald Affeldt (May 30 2020 at 16:30):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.
Reynald Affeldt (May 30 2020 at 16:34):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).
Reynald Affeldt (May 30 2020 at 16:39):(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).)
Reynald Affeldt (May 30 2020 at 16:41):If this fix is right, that makes for a bit more complicated extraction process, which surely must be documented somewhere.
Hugo Herbelin (May 31 2020 at 08:30):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).
Hugo Herbelin (May 31 2020 at 08:32):affeldt-aist said:
I must add that Jacques Garrigue seems to have found a solution by introducing conversions as implemented by
RbaseSymbolsImpl.coq_RabstandRbaseSymbolsImpl.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).
Hugo Herbelin (May 31 2020 at 08:39):And if so, for Rabst and Rrepr, I suspect that you can assert false.
Hugo Herbelin (May 31 2020 at 08:40):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: Sep 26 2023 at 11:01 UTC