The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

The canonical answer to your question would be: a FAQ. It happens that Coq has a FAQ but it is mostly useless because it is very outdated. For mostly historical reasons, it is particularly hard to contribute to, and thus to maintain. I proposed in this issue to move the FAQ to the wiki to make it easier to maintain by users themselves: https://github.com/coq/coq/issues/6180

(I would do this migration myself if I had an unlimited amount of time in my hands. If anyone - you don't need to be a regular Coq contributor - wants to help with this, it would be definitely welcome: post a comment on the issue, some guidance can be provided.)

Once the migration is done, we can start updating the FAQ and making it better. Some questions can probably be removed, other added, when a good answer exists on StackOverflow, on Coq-Club or elsewhere on the internet we can link to it, etc.

Théo

Le ven. 1 déc. 2017 à 00:29, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> a écrit :

On 16/08/2017 15:33, Guillaume Melquiond wrote:
 > On 15/08/2017 08:05, karsar wrote:
 >> What would be a natural choice of float number library if you want to do
 >> some
 >> computations with floats inside Coq (like it's done for integers and
nats,
 >> I know it could be slow) , as well as reason about their properties?
 >> It would be nice to provide a minimal example script showing how you
 >> import the library
 >> and example of the addition of two floats as a demonstration.
 >
 > Both the Flocq and Interval libraries contain computationally effective
 > floating-point components. Which one to use and how to use it depend on
 > your use case. Do you need the floating-point numbers to be compliant
 > with the IEEE-754 standard? What kind of reasoning do you want to
 > perform on them? How efficient do you want the computations to be?
 >
 > Best regards,
 >
 > Guillaume
 >

To all: if this is a question which tends to come up regularly is there
some way we could make the answer easier to find?

Gaëtan Gilbert

On 01/12/2017 00:23, Kevin Sullivan wrote:
> What library or libraries should I consider as I need to represent
> concrete floating point numbers, do calculations with them, and prove
> properties about them using the current version of Coq?