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_float`

s to even terminate! Any ideas of what I'm doing wrong?

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

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.

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!

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

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

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

Looking into PrimFloat, it does seem like there is only `<?`

and `<=?`

. Quite underwhelming, yeah.

Delta has marked this topic as resolved.

Delta has marked this topic as unresolved.

Yea, ah well. Thanks again!

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.

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

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

Thank you @Karl Palmskog !

Last updated: Feb 01 2023 at 11:04 UTC