Add "==", "<", "<=" in PrimFloat.v

* Add a related test-suite in compare.v (generated by a bash script)

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>

3 files changed, 40 insertions, 28 deletions

diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v
index 142883171e..d094032805 100644
--- a/theories/Floats/FloatAxioms.v
+++ b/theories/Floats/FloatAxioms.v
@@ -26,6 +26,10 @@ Qed.
 Axiom opp_spec : forall x, Prim2SF (-x)%float = SFopp (Prim2SF x).
 Axiom abs_spec : forall x, Prim2SF (abs x) = SFabs (Prim2SF x).
 
+Axiom eqb_spec : forall x y, (x == y)%float = SFeqb (Prim2SF x) (Prim2SF y).
+Axiom ltb_spec : forall x y, (x < y)%float = SFltb (Prim2SF x) (Prim2SF y).
+Axiom leb_spec : forall x y, (x <= y)%float = SFleb (Prim2SF x) (Prim2SF y).
+
 Definition flatten_cmp_opt c :=
   match c with
   | None => FNotComparable
diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v
index bdd78ea544..24e4ac2da2 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -18,6 +18,15 @@ Notation "- x" := (opp x) : float_scope.
 
 Primitive abs := #float64_abs.
 
+Primitive eqb := #float64_eq.
+Notation "x == y" := (eqb x y) (at level 70, no associativity) : float_scope.
+
+Primitive ltb := #float64_lt.
+Notation "x < y" := (ltb x y) (at level 70, no associativity) : float_scope.
+
+Primitive leb := #float64_le.
+Notation "x <= y" := (leb x y) (at level 70, no associativity) : float_scope.
+
 Primitive compare := #float64_compare.
 Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope.
 
@@ -72,33 +81,14 @@ Definition zero := Eval compute in (of_int63 0).
 Definition neg_zero := Eval compute in (-zero).
 Definition two := Eval compute in (of_int63 2).
 
-Definition is_nan f :=
-  match f ?= f with
-  | FNotComparable => true
-  | _ => false
-  end.
-
-Definition is_zero f :=
-  match f ?= zero with
-  | FEq => true (* note: 0 == -0 with floats *)
-  | _ => false
-  end.
-
-Definition is_infinity f :=
-  match f ?= infinity with
-  | FEq => true
-  | FLt => match f ?= neg_infinity with
-           | FEq => true
-           | _ => false
-           end
-  | _ => false
-  end.
-
-Definition get_sign f := (* + => false, - => true *)
-  let f := if is_zero f then one / f else f in
-  match f ?= zero with
-  | FGt => false
-  | _ => true
-  end.
+Definition is_nan f := negb (f == f)%float.
+
+Definition is_zero f := (f == zero)%float. (* note: 0 == -0 with floats *)
+
+Definition is_infinity f := (abs f == infinity)%float.
 
 Definition is_finite (x : float) := negb (is_nan x || is_infinity x).
+
+Definition get_sign f :=
+  let f := if is_zero f then (one / f)%float else f in
+  (f < zero)%float.
diff --git a/theories/Floats/SpecFloat.v b/theories/Floats/SpecFloat.v
index 900739812a..8708782e39 100644
--- a/theories/Floats/SpecFloat.v
+++ b/theories/Floats/SpecFloat.v
@@ -183,6 +183,24 @@ Section FloatOps.
       end
     end.
 
+  Definition SFeqb f1 f2 :=
+    match SFcompare f1 f2 with
+    | Some Eq => true
+    | _ => false
+    end.
+
+  Definition SFltb f1 f2 :=
+    match SFcompare f1 f2 with
+    | Some Lt => true
+    | _ => false
+    end.
+
+  Definition SFleb f1 f2 :=
+    match SFcompare f1 f2 with
+    | Some Le => true
+    | _ => false
+    end.
+
   Definition SFclassify f :=
     match f with
     | S754_nan => NaN