Stream: Coq users

Topic: Floating point computations


view this post on Zulip Cody Roux (Aug 05 2020 at 22:04):

Hi all, I'd like to verify some floating point computations by using either the Coq built-in formalization, or Flocq. Unfortunately, I can't seem to get any computations on concrete binary_floats to even terminate! Any ideas of what I'm doing wrong?

view this post on Zulip Pierre Roux (Aug 17 2020 at 09:49):

I guess you are talking about the binary_float type of module IEEE754.Binary of Flocq. This type contains proofs and is rather meant for specification than actual computations. For actual computations inside proofs, you may want to use the PrimFloat.float type in Coq standard lybrary (since 8.11). There are indeed many float types around even in Flocq, the one to use highly depends on your use case. Pinging @Erik Martin-Dorel and @Guillaume Melquiond who may be interested in the discussion (if you haven't solved your problem already).

view this post on Zulip Guillaume Melquiond (Aug 25 2020 at 09:39):

Here are some additional details. Type binary_float is meant for effective computations (e.g., it is used in CompCert to do constant propagations). But there are two things to keep in mind. First, these computations are quite heavy, so the default reduction machinery of Coq might be pushed to its limits. In that case, better use vm_compute than compute (or use the native support for floating-point computations, as mentioned by Pierre). Second, a floating-point value carries a proof term, which can grow out of control if thousands of floating-point computations are performed in a row, thus slowing computations by sheer memory overhead. You can use the erase function to drop the proof terms from time to time, at the cost of a bit of computations. The erase function is also useful if you want to display a computed floating-point value, otherwise Coq will die just trying to display the proof term.

view this post on Zulip Delta (Sep 05 2022 at 03:27):

Hi channel, I'm hoping someone can help me out with a beginner question (please)!

I'm attempting to do some work with floating points and there appears to be some kind of clash happening with float and nat notation.

The error I'm receiving is:

In environment
x11 : float
x12 : float
x21 : float
x22 : float
a : float
b : float
The term "a" has type "float" while it is expected to have type "nat".

The code in concern:

Require Import Floats.
Open Scope float_scope.

Definition semidef_pos_22 (x11 x12 x21 x22: float) :=
    forall (a b: float),
    a <> 0 /\ b <> 0 ->
        (
            a * (a * x11 + b * x12)
            +
            b * (a * x21 + b * x22)
        ) >= 0.

Any help is appreciated!

view this post on Zulip abab9579 (Sep 05 2022 at 03:43):

In coq default, number literals are of nat type, so you cannot use 0 - it seems zero is provided for this.
Also definitions like+, >=, * would be clashing with nat counterpart, so I think you need to delimit scope using %float.

So, it would become

Definition semidef_pos_22 (x11 x12 x21 x22: float) :=
    forall (a b: float),
    a <> zero /\ b <> zero -> (
        (
            a * (a * x11 + b * x12)
            +
            b * (a * x21 + b * x22)
        ) >= zero)%float.

EDIT: forgot some

view this post on Zulip Delta (Sep 05 2022 at 03:46):

Thanks @abab9579, that makes sense. I've changed it to this

Require Import Floats.
Open Scope float_scope.

Definition semidef_pos_22 (x11 x12 x21 x22: float) :=
    forall (a b: float),
    a <> zero /\ b <> zero -> (
        (
            a * (a * x11 + b * x12)
            +
            b * (a * x21 + b * x22)
        ) >= zero)%float.

But I'm still getting the same error as before. You are probably onto something though

view this post on Zulip Delta (Sep 05 2022 at 03:51):

It might actually be the >= operation. It doesn't look like it's defined for floats. This might be what I'm after, although much uglier to work with

Definition semidef_pos_22 (x11 x12 x21 x22: float) :=
    forall (a b: float),
    a <> 0 /\ b <> 0 -> (
        (
            a * (a * x11 + b * x12)
            +
            b * (a * x21 + b * x22)
        ) <? 0) = false.

view this post on Zulip abab9579 (Sep 05 2022 at 03:55):

Looking into PrimFloat, it does seem like there is only <? and <=?. Quite underwhelming, yeah.

view this post on Zulip Notification Bot (Sep 05 2022 at 03:56):

Delta has marked this topic as resolved.

view this post on Zulip Notification Bot (Sep 05 2022 at 03:57):

Delta has marked this topic as unresolved.

view this post on Zulip Delta (Sep 05 2022 at 03:57):

Yea, ah well. Thanks again!

view this post on Zulip Pierre Roux (Sep 05 2022 at 07:11):

Note that a >= b is nothing else than b <= a. Also note that primitive floats are designed for effective computations in reflexive tactics and there is only the minimum required things in the standard lib. If you are interested in formalizations of floating-point numbers, you should rather look at the Flocq library.

view this post on Zulip Delta (Sep 05 2022 at 07:13):

Thank you for the pointers! I'll check Flocq out

view this post on Zulip Karl Palmskog (Sep 05 2022 at 08:54):

for beginners of Flocq this tutorial might be useful: https://github.com/thery/FlocqLecture

view this post on Zulip Delta (Sep 05 2022 at 09:39):

Thank you @Karl Palmskog !


Last updated: Feb 01 2023 at 11:04 UTC