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?
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
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
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
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
<=?. Quite underwhelming, yeah.
Delta has marked this topic as resolved.
Delta has marked this topic as unresolved.
Yea, ah well. Thanks again!
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