Floating point computations · Coq users

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?

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

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.

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.

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

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.

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.

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.

Delta (Sep 05 2022 at 03:46):

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

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.

abab9579 (Sep 05 2022 at 03:55):

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

Notification Bot (Sep 05 2022 at 03:56):

Notification Bot (Sep 05 2022 at 03:57):

Delta (Sep 05 2022 at 03:57):

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.

Stream: Coq users

Topic: Floating point computations

Cody Roux (Aug 05 2020 at 22:04):