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>

19 files changed, 613 insertions, 29 deletions

diff --git a/checker/values.ml b/checker/values.ml
index 0cd63566d7..3882f88391 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -228,7 +228,7 @@ let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
 
 let v_primitive =
-  v_enum "primitive" 41 (* Number of "Primitive" in Int63.v and PrimFloat.v *)
+  v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *)
 
 let v_cst_def =
   v_sum "constant_def" 0
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 3fe77afc2d..931b509f48 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -44,6 +44,7 @@ void init_arity () {
     arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
     arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 
     arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
+    arity[LTFLOAT]=arity[LEFLOAT]=
     arity[ISINT]=arity[AREINT2]=0;
   /* instruction with one operand */
   arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
@@ -64,6 +65,7 @@ void init_arity () {
     arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]=
     arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
     arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=
+    arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]=
     arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]=
     arity[CHECKCLASSIFYFLOAT]=
     arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]=
diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h
index 9fc390bd33..c41079c8ff 100644
--- a/kernel/byterun/coq_float64.h
+++ b/kernel/byterun/coq_float64.h
@@ -3,6 +3,15 @@
 
 #include <math.h>
 
+#define DECLARE_FREL(name, e)                                           \
+  int coq_##name(double x, double y) {                                  \
+    return e;                                                           \
+  }                                                                     \
+                                                                        \
+  value coq_##name##_byte(value x, value y) {                           \
+    return coq_##name(Double_val(x), Double_val(y));                    \
+  }
+
 #define DECLARE_FBINOP(name, e)                                         \
   double coq_##name(double x, double y) {                               \
     return e;                                                           \
@@ -21,6 +30,9 @@
     return caml_copy_double(coq_##name(Double_val(x)));                 \
   }
 
+DECLARE_FREL(feq, x == y)
+DECLARE_FREL(flt, x < y)
+DECLARE_FREL(fle, x <= y)
 DECLARE_FBINOP(fmul, x * y)
 DECLARE_FBINOP(fadd, x + y)
 DECLARE_FBINOP(fsub, x - y)
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 6e6adb1293..c21aeecb16 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1545,6 +1545,33 @@ value coq_interprete
         Next;
       }
 
+      Instruct (CHECKEQFLOAT) {
+        print_instr("CHECKEQFLOAT");
+        CheckFloat2();
+        accu = coq_feq(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+        Next;
+      }
+
+      Instruct (CHECKLTFLOAT) {
+        print_instr("CHECKLTFLOAT");
+        CheckFloat2();
+      }
+      Instruct (LTFLOAT) {
+        print_instr("LTFLOAT");
+        accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+        Next;
+      }
+
+      Instruct (CHECKLEFLOAT) {
+        print_instr("CHECKLEFLOAT");
+        CheckFloat2();
+      }
+      Instruct (LEFLOAT) {
+        print_instr("LEFLOAT");
+        accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+        Next;
+      }
+
       Instruct (CHECKCOMPAREFLOAT) {
         double x, y;
         print_instr("CHECKCOMPAREFLOAT");
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 342cc29a22..9ff7f69203 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -35,6 +35,9 @@ type t =
   | Int63compare
   | Float64opp
   | Float64abs
+  | Float64eq
+  | Float64lt
+  | Float64le
   | Float64compare
   | Float64classify
   | Float64add
@@ -92,6 +95,9 @@ let hash = function
   | Float64ldshiftexp -> 37
   | Float64next_up -> 38
   | Float64next_down -> 39
+  | Float64eq -> 40
+  | Float64lt -> 41
+  | Float64le -> 42
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -121,6 +127,9 @@ let to_string = function
   | Int63compare -> "compare"
   | Float64opp -> "fopp"
   | Float64abs -> "fabs"
+  | Float64eq -> "feq"
+  | Float64lt -> "flt"
+  | Float64le -> "fle"
   | Float64compare -> "fcompare"
   | Float64classify -> "fclassify"
   | Float64add -> "fadd"
@@ -176,6 +185,7 @@ let types =
   | Float64ofInt63 -> [int_ty; float_ty]
   | Float64normfr_mantissa -> [float_ty; int_ty]
   | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
+  | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())]
   | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
   | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())]
   | Float64add | Float64sub | Float64mul
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 3cb210233d..be65ba5305 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -35,6 +35,9 @@ type t =
   | Int63compare
   | Float64opp
   | Float64abs
+  | Float64eq
+  | Float64lt
+  | Float64le
   | Float64compare
   | Float64classify
   | Float64add
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 908f84293c..5e82cef810 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -236,6 +236,9 @@ let check_prim_op = function
   | Int63compare   -> opCHECKCOMPAREINT63
   | Float64opp     -> opCHECKOPPFLOAT
   | Float64abs     -> opCHECKABSFLOAT
+  | Float64eq      -> opCHECKEQFLOAT
+  | Float64lt      -> opCHECKLTFLOAT
+  | Float64le      -> opCHECKLEFLOAT
   | Float64compare -> opCHECKCOMPAREFLOAT
   | Float64classify -> opCHECKCLASSIFYFLOAT
   | Float64add     -> opCHECKADDFLOAT
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 55ad472ea9..86b14c5cd2 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -42,6 +42,15 @@ let abs = abs_float
 
 type float_comparison = FEq | FLt | FGt | FNotComparable
 
+let eq x y = x = y
+[@@ocaml.inline always]
+
+let lt x y = x < y
+[@@ocaml.inline always]
+
+let le x y = x <= y
+[@@ocaml.inline always]
+
 (* inspired by lib/util.ml; see also #10471 *)
 let pervasives_compare = compare
 
diff --git a/kernel/float64.mli b/kernel/float64.mli
index 78dc1a7bd7..2aa9796526 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -34,6 +34,12 @@ val abs : t -> t
 
 type float_comparison = FEq | FLt | FGt | FNotComparable
 
+val eq : t -> t -> bool
+
+val lt : t -> t -> bool
+
+val le : t -> t -> bool
+
 (** The IEEE 754 float comparison.
  * NotComparable is returned if there is a NaN in the arguments *)
 val compare : t -> t -> float_comparison
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 52b7a822e3..82bb2b584d 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -139,6 +139,11 @@ let opcodes =
     "AREINT2";
     "CHECKOPPFLOAT";
     "CHECKABSFLOAT";
+    "CHECKEQFLOAT";
+    "CHECKLTFLOAT";
+    "LTFLOAT";
+    "CHECKLEFLOAT";
+    "LEFLOAT";
     "CHECKCOMPAREFLOAT";
     "CHECKCLASSIFYFLOAT";
     "CHECKADDFLOAT";
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 6b9d49052d..e4a8344eaf 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -539,6 +539,27 @@ let fabs accu x =
   if is_float x then no_check_fabs x
   else accu x
 
+let no_check_feq x y =
+  mk_bool (Float64.eq (to_float x) (to_float y))
+
+let feq accu x y =
+  if is_float x && is_float y then no_check_feq x y
+  else accu x y
+
+let no_check_flt x y =
+  mk_bool (Float64.lt (to_float x) (to_float y))
+
+let flt accu x y =
+  if is_float x && is_float y then no_check_flt x y
+  else accu x y
+
+let no_check_fle x y =
+  mk_bool (Float64.le (to_float x) (to_float y))
+
+let fle accu x y =
+  if is_float x && is_float y then no_check_fle x y
+  else accu x y
+
 type coq_fcmp =
   | CFcmpAccu of t
   | CFcmpEq
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index d19877c121..815ef3e98e 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -261,6 +261,9 @@ val is_float : t -> bool
 
 val fopp : t -> t -> t
 val fabs : t -> t -> t
+val feq : t -> t -> t -> t
+val flt : t -> t -> t -> t
+val fle : t -> t -> t -> t
 val fcompare : t -> t -> t -> t
 val fclassify : t -> t -> t
 val fadd : t -> t -> t -> t
@@ -282,6 +285,15 @@ val no_check_fopp : t -> t
 val no_check_fabs : t -> t
 [@@ocaml.inline always]
 
+val no_check_feq : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_flt : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fle : t -> t -> t
+[@@ocaml.inline always]
+
 val no_check_fcompare : t -> t -> t
 [@@ocaml.inline always]
 
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 2766793005..c475828cb3 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -261,6 +261,15 @@ struct
       let f = get_float1 evd args in E.mkFloat env (Float64.opp f)
     | Float64abs ->
       let f = get_float1 evd args in E.mkFloat env (Float64.abs f)
+    | Float64eq ->
+      let i1, i2 = get_float2 evd args in
+      E.mkBool env (Float64.eq i1 i2)
+    | Float64lt ->
+      let i1, i2 = get_float2 evd args in
+      E.mkBool env (Float64.lt i1 i2)
+    | Float64le ->
+      let i1, i2 = get_float2 evd args in
+      E.mkBool env (Float64.le i1 i2)
     | Float64compare ->
       let f1, f2 = get_float2 evd args in
       (match Float64.compare f1 f2 with
diff --git a/test-suite/primitive/float/compare.v b/test-suite/primitive/float/compare.v
new file mode 100644
index 0000000000..23d1e5bbae
--- /dev/null
+++ b/test-suite/primitive/float/compare.v
@@ -0,0 +1,385 @@
+(* DO NOT EDIT THIS FILE: automatically generated by ./gen_compare.sh *)
+Require Import ZArith Floats.
+Local Open Scope float_scope.
+
+Definition min_denorm := Eval compute in ldexp one (-1074)%Z.
+
+Definition min_norm := Eval compute in ldexp one (-1024)%Z.
+
+Check (eq_refl false : nan == nan = false).
+Check (eq_refl false : nan == nan = false).
+Check (eq_refl false : nan < nan = false).
+Check (eq_refl false : nan < nan = false).
+Check (eq_refl false : nan <= nan = false).
+Check (eq_refl false : nan <= nan = false).
+Check (eq_refl FNotComparable : nan ?= nan = FNotComparable).
+Check (eq_refl FNotComparable : nan ?= nan = FNotComparable).
+
+Check (eq_refl false <: nan == nan = false).
+Check (eq_refl false <: nan == nan = false).
+Check (eq_refl false <: nan < nan = false).
+Check (eq_refl false <: nan < nan = false).
+Check (eq_refl false <: nan <= nan = false).
+Check (eq_refl false <: nan <= nan = false).
+Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable).
+Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable).
+
+Check (eq_refl false <<: nan == nan = false).
+Check (eq_refl false <<: nan == nan = false).
+Check (eq_refl false <<: nan < nan = false).
+Check (eq_refl false <<: nan < nan = false).
+Check (eq_refl false <<: nan <= nan = false).
+Check (eq_refl false <<: nan <= nan = false).
+Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable).
+Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable).
+
+Check (eq_refl false : nan == - nan = false).
+Check (eq_refl false : - nan == nan = false).
+Check (eq_refl false : nan < - nan = false).
+Check (eq_refl false : - nan < nan = false).
+Check (eq_refl false : nan <= - nan = false).
+Check (eq_refl false : - nan <= nan = false).
+Check (eq_refl FNotComparable : nan ?= - nan = FNotComparable).
+Check (eq_refl FNotComparable : - nan ?= nan = FNotComparable).
+
+Check (eq_refl false <: nan == - nan = false).
+Check (eq_refl false <: - nan == nan = false).
+Check (eq_refl false <: nan < - nan = false).
+Check (eq_refl false <: - nan < nan = false).
+Check (eq_refl false <: nan <= - nan = false).
+Check (eq_refl false <: - nan <= nan = false).
+Check (eq_refl FNotComparable <: nan ?= - nan = FNotComparable).
+Check (eq_refl FNotComparable <: - nan ?= nan = FNotComparable).
+
+Check (eq_refl false <<: nan == - nan = false).
+Check (eq_refl false <<: - nan == nan = false).
+Check (eq_refl false <<: nan < - nan = false).
+Check (eq_refl false <<: - nan < nan = false).
+Check (eq_refl false <<: nan <= - nan = false).
+Check (eq_refl false <<: - nan <= nan = false).
+Check (eq_refl FNotComparable <<: nan ?= - nan = FNotComparable).
+Check (eq_refl FNotComparable <<: - nan ?= nan = FNotComparable).
+
+Check (eq_refl true : one == one = true).
+Check (eq_refl true : one == one = true).
+Check (eq_refl false : one < one = false).
+Check (eq_refl false : one < one = false).
+Check (eq_refl true : one <= one = true).
+Check (eq_refl true : one <= one = true).
+Check (eq_refl FEq : one ?= one = FEq).
+Check (eq_refl FEq : one ?= one = FEq).
+
+Check (eq_refl true <: one == one = true).
+Check (eq_refl true <: one == one = true).
+Check (eq_refl false <: one < one = false).
+Check (eq_refl false <: one < one = false).
+Check (eq_refl true <: one <= one = true).
+Check (eq_refl true <: one <= one = true).
+Check (eq_refl FEq <: one ?= one = FEq).
+Check (eq_refl FEq <: one ?= one = FEq).
+
+Check (eq_refl true <<: one == one = true).
+Check (eq_refl true <<: one == one = true).
+Check (eq_refl false <<: one < one = false).
+Check (eq_refl false <<: one < one = false).
+Check (eq_refl true <<: one <= one = true).
+Check (eq_refl true <<: one <= one = true).
+Check (eq_refl FEq <<: one ?= one = FEq).
+Check (eq_refl FEq <<: one ?= one = FEq).
+
+Check (eq_refl true : zero == zero = true).
+Check (eq_refl true : zero == zero = true).
+Check (eq_refl false : zero < zero = false).
+Check (eq_refl false : zero < zero = false).
+Check (eq_refl true : zero <= zero = true).
+Check (eq_refl true : zero <= zero = true).
+Check (eq_refl FEq : zero ?= zero = FEq).
+Check (eq_refl FEq : zero ?= zero = FEq).
+
+Check (eq_refl true <: zero == zero = true).
+Check (eq_refl true <: zero == zero = true).
+Check (eq_refl false <: zero < zero = false).
+Check (eq_refl false <: zero < zero = false).
+Check (eq_refl true <: zero <= zero = true).
+Check (eq_refl true <: zero <= zero = true).
+Check (eq_refl FEq <: zero ?= zero = FEq).
+Check (eq_refl FEq <: zero ?= zero = FEq).
+
+Check (eq_refl true <<: zero == zero = true).
+Check (eq_refl true <<: zero == zero = true).
+Check (eq_refl false <<: zero < zero = false).
+Check (eq_refl false <<: zero < zero = false).
+Check (eq_refl true <<: zero <= zero = true).
+Check (eq_refl true <<: zero <= zero = true).
+Check (eq_refl FEq <<: zero ?= zero = FEq).
+Check (eq_refl FEq <<: zero ?= zero = FEq).
+
+Check (eq_refl true : zero == - zero = true).
+Check (eq_refl true : - zero == zero = true).
+Check (eq_refl false : zero < - zero = false).
+Check (eq_refl false : - zero < zero = false).
+Check (eq_refl true : zero <= - zero = true).
+Check (eq_refl true : - zero <= zero = true).
+Check (eq_refl FEq : zero ?= - zero = FEq).
+Check (eq_refl FEq : - zero ?= zero = FEq).
+
+Check (eq_refl true <: zero == - zero = true).
+Check (eq_refl true <: - zero == zero = true).
+Check (eq_refl false <: zero < - zero = false).
+Check (eq_refl false <: - zero < zero = false).
+Check (eq_refl true <: zero <= - zero = true).
+Check (eq_refl true <: - zero <= zero = true).
+Check (eq_refl FEq <: zero ?= - zero = FEq).
+Check (eq_refl FEq <: - zero ?= zero = FEq).
+
+Check (eq_refl true <<: zero == - zero = true).
+Check (eq_refl true <<: - zero == zero = true).
+Check (eq_refl false <<: zero < - zero = false).
+Check (eq_refl false <<: - zero < zero = false).
+Check (eq_refl true <<: zero <= - zero = true).
+Check (eq_refl true <<: - zero <= zero = true).
+Check (eq_refl FEq <<: zero ?= - zero = FEq).
+Check (eq_refl FEq <<: - zero ?= zero = FEq).
+
+Check (eq_refl true : - zero == - zero = true).
+Check (eq_refl true : - zero == - zero = true).
+Check (eq_refl false : - zero < - zero = false).
+Check (eq_refl false : - zero < - zero = false).
+Check (eq_refl true : - zero <= - zero = true).
+Check (eq_refl true : - zero <= - zero = true).
+Check (eq_refl FEq : - zero ?= - zero = FEq).
+Check (eq_refl FEq : - zero ?= - zero = FEq).
+
+Check (eq_refl true <: - zero == - zero = true).
+Check (eq_refl true <: - zero == - zero = true).
+Check (eq_refl false <: - zero < - zero = false).
+Check (eq_refl false <: - zero < - zero = false).
+Check (eq_refl true <: - zero <= - zero = true).
+Check (eq_refl true <: - zero <= - zero = true).
+Check (eq_refl FEq <: - zero ?= - zero = FEq).
+Check (eq_refl FEq <: - zero ?= - zero = FEq).
+
+Check (eq_refl true <<: - zero == - zero = true).
+Check (eq_refl true <<: - zero == - zero = true).
+Check (eq_refl false <<: - zero < - zero = false).
+Check (eq_refl false <<: - zero < - zero = false).
+Check (eq_refl true <<: - zero <= - zero = true).
+Check (eq_refl true <<: - zero <= - zero = true).
+Check (eq_refl FEq <<: - zero ?= - zero = FEq).
+Check (eq_refl FEq <<: - zero ?= - zero = FEq).
+
+Check (eq_refl true : infinity == infinity = true).
+Check (eq_refl true : infinity == infinity = true).
+Check (eq_refl false : infinity < infinity = false).
+Check (eq_refl false : infinity < infinity = false).
+Check (eq_refl true : infinity <= infinity = true).
+Check (eq_refl true : infinity <= infinity = true).
+Check (eq_refl FEq : infinity ?= infinity = FEq).
+Check (eq_refl FEq : infinity ?= infinity = FEq).
+
+Check (eq_refl true <: infinity == infinity = true).
+Check (eq_refl true <: infinity == infinity = true).
+Check (eq_refl false <: infinity < infinity = false).
+Check (eq_refl false <: infinity < infinity = false).
+Check (eq_refl true <: infinity <= infinity = true).
+Check (eq_refl true <: infinity <= infinity = true).
+Check (eq_refl FEq <: infinity ?= infinity = FEq).
+Check (eq_refl FEq <: infinity ?= infinity = FEq).
+
+Check (eq_refl true <<: infinity == infinity = true).
+Check (eq_refl true <<: infinity == infinity = true).
+Check (eq_refl false <<: infinity < infinity = false).
+Check (eq_refl false <<: infinity < infinity = false).
+Check (eq_refl true <<: infinity <= infinity = true).
+Check (eq_refl true <<: infinity <= infinity = true).
+Check (eq_refl FEq <<: infinity ?= infinity = FEq).
+Check (eq_refl FEq <<: infinity ?= infinity = FEq).
+
+Check (eq_refl true : - infinity == - infinity = true).
+Check (eq_refl true : - infinity == - infinity = true).
+Check (eq_refl false : - infinity < - infinity = false).
+Check (eq_refl false : - infinity < - infinity = false).
+Check (eq_refl true : - infinity <= - infinity = true).
+Check (eq_refl true : - infinity <= - infinity = true).
+Check (eq_refl FEq : - infinity ?= - infinity = FEq).
+Check (eq_refl FEq : - infinity ?= - infinity = FEq).
+
+Check (eq_refl true <: - infinity == - infinity = true).
+Check (eq_refl true <: - infinity == - infinity = true).
+Check (eq_refl false <: - infinity < - infinity = false).
+Check (eq_refl false <: - infinity < - infinity = false).
+Check (eq_refl true <: - infinity <= - infinity = true).
+Check (eq_refl true <: - infinity <= - infinity = true).
+Check (eq_refl FEq <: - infinity ?= - infinity = FEq).
+Check (eq_refl FEq <: - infinity ?= - infinity = FEq).
+
+Check (eq_refl true <<: - infinity == - infinity = true).
+Check (eq_refl true <<: - infinity == - infinity = true).
+Check (eq_refl false <<: - infinity < - infinity = false).
+Check (eq_refl false <<: - infinity < - infinity = false).
+Check (eq_refl true <<: - infinity <= - infinity = true).
+Check (eq_refl true <<: - infinity <= - infinity = true).
+Check (eq_refl FEq <<: - infinity ?= - infinity = FEq).
+Check (eq_refl FEq <<: - infinity ?= - infinity = FEq).
+
+Check (eq_refl false : min_denorm == min_norm = false).
+Check (eq_refl false : min_norm == min_denorm = false).
+Check (eq_refl true : min_denorm < min_norm = true).
+Check (eq_refl false : min_norm < min_denorm = false).
+Check (eq_refl true : min_denorm <= min_norm = true).
+Check (eq_refl false : min_norm <= min_denorm = false).
+Check (eq_refl FLt : min_denorm ?= min_norm = FLt).
+Check (eq_refl FGt : min_norm ?= min_denorm = FGt).
+
+Check (eq_refl false <: min_denorm == min_norm = false).
+Check (eq_refl false <: min_norm == min_denorm = false).
+Check (eq_refl true <: min_denorm < min_norm = true).
+Check (eq_refl false <: min_norm < min_denorm = false).
+Check (eq_refl true <: min_denorm <= min_norm = true).
+Check (eq_refl false <: min_norm <= min_denorm = false).
+Check (eq_refl FLt <: min_denorm ?= min_norm = FLt).
+Check (eq_refl FGt <: min_norm ?= min_denorm = FGt).
+
+Check (eq_refl false <<: min_denorm == min_norm = false).
+Check (eq_refl false <<: min_norm == min_denorm = false).
+Check (eq_refl true <<: min_denorm < min_norm = true).
+Check (eq_refl false <<: min_norm < min_denorm = false).
+Check (eq_refl true <<: min_denorm <= min_norm = true).
+Check (eq_refl false <<: min_norm <= min_denorm = false).
+Check (eq_refl FLt <<: min_denorm ?= min_norm = FLt).
+Check (eq_refl FGt <<: min_norm ?= min_denorm = FGt).
+
+Check (eq_refl false : min_denorm == one = false).
+Check (eq_refl false : one == min_denorm = false).
+Check (eq_refl true : min_denorm < one = true).
+Check (eq_refl false : one < min_denorm = false).
+Check (eq_refl true : min_denorm <= one = true).
+Check (eq_refl false : one <= min_denorm = false).
+Check (eq_refl FLt : min_denorm ?= one = FLt).
+Check (eq_refl FGt : one ?= min_denorm = FGt).
+
+Check (eq_refl false <: min_denorm == one = false).
+Check (eq_refl false <: one == min_denorm = false).
+Check (eq_refl true <: min_denorm < one = true).
+Check (eq_refl false <: one < min_denorm = false).
+Check (eq_refl true <: min_denorm <= one = true).
+Check (eq_refl false <: one <= min_denorm = false).
+Check (eq_refl FLt <: min_denorm ?= one = FLt).
+Check (eq_refl FGt <: one ?= min_denorm = FGt).
+
+Check (eq_refl false <<: min_denorm == one = false).
+Check (eq_refl false <<: one == min_denorm = false).
+Check (eq_refl true <<: min_denorm < one = true).
+Check (eq_refl false <<: one < min_denorm = false).
+Check (eq_refl true <<: min_denorm <= one = true).
+Check (eq_refl false <<: one <= min_denorm = false).
+Check (eq_refl FLt <<: min_denorm ?= one = FLt).
+Check (eq_refl FGt <<: one ?= min_denorm = FGt).
+
+Check (eq_refl false : min_norm == one = false).
+Check (eq_refl false : one == min_norm = false).
+Check (eq_refl true : min_norm < one = true).
+Check (eq_refl false : one < min_norm = false).
+Check (eq_refl true : min_norm <= one = true).
+Check (eq_refl false : one <= min_norm = false).
+Check (eq_refl FLt : min_norm ?= one = FLt).
+Check (eq_refl FGt : one ?= min_norm = FGt).
+
+Check (eq_refl false <: min_norm == one = false).
+Check (eq_refl false <: one == min_norm = false).
+Check (eq_refl true <: min_norm < one = true).
+Check (eq_refl false <: one < min_norm = false).
+Check (eq_refl true <: min_norm <= one = true).
+Check (eq_refl false <: one <= min_norm = false).
+Check (eq_refl FLt <: min_norm ?= one = FLt).
+Check (eq_refl FGt <: one ?= min_norm = FGt).
+
+Check (eq_refl false <<: min_norm == one = false).
+Check (eq_refl false <<: one == min_norm = false).
+Check (eq_refl true <<: min_norm < one = true).
+Check (eq_refl false <<: one < min_norm = false).
+Check (eq_refl true <<: min_norm <= one = true).
+Check (eq_refl false <<: one <= min_norm = false).
+Check (eq_refl FLt <<: min_norm ?= one = FLt).
+Check (eq_refl FGt <<: one ?= min_norm = FGt).
+
+Check (eq_refl false : one == infinity = false).
+Check (eq_refl false : infinity == one = false).
+Check (eq_refl true : one < infinity = true).
+Check (eq_refl false : infinity < one = false).
+Check (eq_refl true : one <= infinity = true).
+Check (eq_refl false : infinity <= one = false).
+Check (eq_refl FLt : one ?= infinity = FLt).
+Check (eq_refl FGt : infinity ?= one = FGt).
+
+Check (eq_refl false <: one == infinity = false).
+Check (eq_refl false <: infinity == one = false).
+Check (eq_refl true <: one < infinity = true).
+Check (eq_refl false <: infinity < one = false).
+Check (eq_refl true <: one <= infinity = true).
+Check (eq_refl false <: infinity <= one = false).
+Check (eq_refl FLt <: one ?= infinity = FLt).
+Check (eq_refl FGt <: infinity ?= one = FGt).
+
+Check (eq_refl false <<: one == infinity = false).
+Check (eq_refl false <<: infinity == one = false).
+Check (eq_refl true <<: one < infinity = true).
+Check (eq_refl false <<: infinity < one = false).
+Check (eq_refl true <<: one <= infinity = true).
+Check (eq_refl false <<: infinity <= one = false).
+Check (eq_refl FLt <<: one ?= infinity = FLt).
+Check (eq_refl FGt <<: infinity ?= one = FGt).
+
+Check (eq_refl false : - infinity == infinity = false).
+Check (eq_refl false : infinity == - infinity = false).
+Check (eq_refl true : - infinity < infinity = true).
+Check (eq_refl false : infinity < - infinity = false).
+Check (eq_refl true : - infinity <= infinity = true).
+Check (eq_refl false : infinity <= - infinity = false).
+Check (eq_refl FLt : - infinity ?= infinity = FLt).
+Check (eq_refl FGt : infinity ?= - infinity = FGt).
+
+Check (eq_refl false <: - infinity == infinity = false).
+Check (eq_refl false <: infinity == - infinity = false).
+Check (eq_refl true <: - infinity < infinity = true).
+Check (eq_refl false <: infinity < - infinity = false).
+Check (eq_refl true <: - infinity <= infinity = true).
+Check (eq_refl false <: infinity <= - infinity = false).
+Check (eq_refl FLt <: - infinity ?= infinity = FLt).
+Check (eq_refl FGt <: infinity ?= - infinity = FGt).
+
+Check (eq_refl false <<: - infinity == infinity = false).
+Check (eq_refl false <<: infinity == - infinity = false).
+Check (eq_refl true <<: - infinity < infinity = true).
+Check (eq_refl false <<: infinity < - infinity = false).
+Check (eq_refl true <<: - infinity <= infinity = true).
+Check (eq_refl false <<: infinity <= - infinity = false).
+Check (eq_refl FLt <<: - infinity ?= infinity = FLt).
+Check (eq_refl FGt <<: infinity ?= - infinity = FGt).
+
+Check (eq_refl false : - infinity == one = false).
+Check (eq_refl false : one == - infinity = false).
+Check (eq_refl true : - infinity < one = true).
+Check (eq_refl false : one < - infinity = false).
+Check (eq_refl true : - infinity <= one = true).
+Check (eq_refl false : one <= - infinity = false).
+Check (eq_refl FLt : - infinity ?= one = FLt).
+Check (eq_refl FGt : one ?= - infinity = FGt).
+
+Check (eq_refl false <: - infinity == one = false).
+Check (eq_refl false <: one == - infinity = false).
+Check (eq_refl true <: - infinity < one = true).
+Check (eq_refl false <: one < - infinity = false).
+Check (eq_refl true <: - infinity <= one = true).
+Check (eq_refl false <: one <= - infinity = false).
+Check (eq_refl FLt <: - infinity ?= one = FLt).
+Check (eq_refl FGt <: one ?= - infinity = FGt).
+
+Check (eq_refl false <<: - infinity == one = false).
+Check (eq_refl false <<: one == - infinity = false).
+Check (eq_refl true <<: - infinity < one = true).
+Check (eq_refl false <<: one < - infinity = false).
+Check (eq_refl true <<: - infinity <= one = true).
+Check (eq_refl false <<: one <= - infinity = false).
+Check (eq_refl FLt <<: - infinity ?= one = FLt).
+Check (eq_refl FGt <<: one ?= - infinity = FGt).
diff --git a/test-suite/primitive/float/gen_compare.sh b/test-suite/primitive/float/gen_compare.sh
new file mode 100755
index 0000000000..cd87eb4e5b
--- /dev/null
+++ b/test-suite/primitive/float/gen_compare.sh
@@ -0,0 +1,65 @@
+#!/bin/bash
+# -*- compile-command: "mv -f compare.v{,~} && ./gen_compare.sh" -*-
+set -e
+
+exec > compare.v
+
+cat <<EOF
+(* DO NOT EDIT THIS FILE: automatically generated by ./gen_compare.sh *)
+Require Import ZArith Floats.
+Local Open Scope float_scope.
+
+Definition min_denorm := Eval compute in ldexp one (-1074)%Z.
+
+Definition min_norm := Eval compute in ldexp one (-1024)%Z.
+
+EOF
+
+genTest() {
+    if [ $# -ne 10 ]; then
+        echo >&2 "genTest expects 10 arguments"
+    fi
+    TACTICS=(":" "<:" "<<:")
+    OPS=("==" "<" "<=" "?=")
+    x="$1"
+    y="$2"
+    OPS1=("$3" "$4" "$5" "$6")  # for x y
+    OPS2=("$7" "$8" "$9" "${10}") # for y x
+    for tac in "${TACTICS[@]}"; do
+        for i in {0..3}; do
+            op="${OPS[$i]}"
+            op1="${OPS1[$i]}"
+            op2="${OPS2[$i]}"
+            echo "Check (eq_refl $op1 $tac $x $op $y = $op1)."
+            echo "Check (eq_refl $op2 $tac $y $op $x = $op2)."
+        done
+        echo
+    done
+}
+
+genTest nan nan \
+        false false false FNotComparable \
+        false false false FNotComparable
+genTest nan "- nan" \
+        false false false FNotComparable \
+        false false false FNotComparable
+
+EQ=(true false true FEq \
+    true false true FEq)
+
+genTest one one "${EQ[@]}"
+genTest zero zero "${EQ[@]}"
+genTest zero "- zero" "${EQ[@]}"
+genTest "- zero" "- zero" "${EQ[@]}"
+genTest infinity infinity "${EQ[@]}"
+genTest "- infinity" "- infinity" "${EQ[@]}"
+
+LT=(false true true FLt \
+    false false false FGt)
+
+genTest min_denorm min_norm "${LT[@]}"
+genTest min_denorm one "${LT[@]}"
+genTest min_norm one "${LT[@]}"
+genTest one infinity "${LT[@]}"
+genTest "- infinity" infinity "${LT[@]}"
+genTest "- infinity" one "${LT[@]}"
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
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 635b9b2c88..b4c0a33585 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -275,6 +275,9 @@ GRAMMAR EXTEND Gram
        | "#int63_compare" -> { CPrimitives.Int63compare }
        | "#float64_opp" -> { CPrimitives.Float64opp }
        | "#float64_abs" -> { CPrimitives.Float64abs }
+       | "#float64_eq" -> { CPrimitives.Float64eq }
+       | "#float64_lt" -> { CPrimitives.Float64lt }
+       | "#float64_le" -> { CPrimitives.Float64le }
        | "#float64_compare" -> { CPrimitives.Float64compare }
        | "#float64_classify" -> { CPrimitives.Float64classify }
        | "#float64_add" -> { CPrimitives.Float64add }