Merge PR #9867: Add primitive floats (binary64 floating-point numbers)

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl

50 files changed, 1369 insertions, 2 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index d9c89d7a8a..1744138d29 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -102,7 +102,7 @@ INTERACTIVE := interactive
 UNIT_TESTS := unit-tests
 VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \
   output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
-  coqdoc ssr arithmetic ltac2
+  coqdoc ssr primitive/uint63 primitive/float ltac2
 
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
@@ -175,6 +175,7 @@ summary:
 	  $(call summary_dir, "Miscellaneous tests", misc); \
 	  $(call summary_dir, "Complexity tests", complexity); \
 	  $(call summary_dir, "Module tests", modules); \
+	  $(call summary_dir, "Primitive tests", primitive); \
 	  $(call summary_dir, "STM tests", stm); \
 	  $(call summary_dir, "SSR tests", ssr); \
 	  $(call summary_dir, "IDE tests", ide); \
@@ -330,7 +331,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	} > "$@"
 
 ssr: $(wildcard ssr/*.v:%.v=%.v.log)
-$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG)
+$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v primitive/*/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods)"; \
diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out
new file mode 100644
index 0000000000..cfd6633752
--- /dev/null
+++ b/test-suite/output/FloatExtraction.out
@@ -0,0 +1,67 @@
+
+(** val infinity : Float64.t **)
+
+let infinity =
+  (Float64.of_float (infinity))
+
+(** val neg_infinity : Float64.t **)
+
+let neg_infinity =
+  (Float64.of_float (neg_infinity))
+
+(** val nan : Float64.t **)
+
+let nan =
+  (Float64.of_float (nan))
+
+(** val one : Float64.t **)
+
+let one =
+  (Float64.of_float (0x1p+0))
+
+(** val zero : Float64.t **)
+
+let zero =
+  (Float64.of_float (0x0p+0))
+
+(** val two : Float64.t **)
+
+let two =
+  (Float64.of_float (0x1p+1))
+
+(** val list_floats : Float64.t list **)
+
+let list_floats =
+  nan :: (infinity :: (neg_infinity :: (zero :: (one :: (two :: ((Float64.of_float (0x1p-1)) :: ((Float64.of_float (0x1.47ae147ae147bp-7)) :: ((Float64.of_float (-0x1p-1)) :: ((Float64.of_float (-0x1.47ae147ae147bp-7)) :: ((Float64.of_float (0x1.e42d130773b76p+1023)) :: ((Float64.of_float (-0x0.c396c98f8d899p-1022)) :: [])))))))))))
+
+
+(** val sqrt : Float64.t -> Float64.t **)
+
+let sqrt = Float64.sqrt
+
+(** val opp : Float64.t -> Float64.t **)
+
+let opp = Float64.opp
+
+(** val mul : Float64.t -> Float64.t -> Float64.t **)
+
+let mul = Float64.mul
+
+(** val sub : Float64.t -> Float64.t -> Float64.t **)
+
+let sub = Float64.sub
+
+(** val div : Float64.t -> Float64.t -> Float64.t **)
+
+let div = Float64.div
+
+(** val discr : Float64.t -> Float64.t -> Float64.t -> Float64.t **)
+
+let discr a b c =
+  sub (mul b b) (mul (mul (Float64.of_float (0x1p+2)) a) c)
+
+(** val x1 : Float64.t -> Float64.t -> Float64.t -> Float64.t **)
+
+let x1 a b c =
+  div (sub (opp b) (sqrt (discr a b c))) (mul (Float64.of_float (0x1p+1)) a)
+
diff --git a/test-suite/output/FloatExtraction.v b/test-suite/output/FloatExtraction.v
new file mode 100644
index 0000000000..f296e8e871
--- /dev/null
+++ b/test-suite/output/FloatExtraction.v
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import Floats ExtrOCamlFloats.
+
+Require Import List. Import ListNotations.
+
+(* from Require Import ExtrOcamlBasic. *)
+Extract Inductive list => list [ "[]" "( :: )" ].
+
+Local Open Scope float_scope.
+
+(* Avoid exponents with less than three digits as they are usually
+   displayed with two digits (1e7 is displayed 1e+07) except on
+   Windows where three digits are used (1e+007). *)
+Definition list_floats :=
+  [nan; infinity; neg_infinity; zero; one; two;
+   0.5; 0.01; -0.5; -0.01; 1.7e+308; -1.7e-308].
+
+Recursive Extraction list_floats.
+
+Definition discr a b c := b * b - 4.0 * a * c.
+
+Definition x1 a b c := (- b - sqrt (discr a b c)) / (2.0 * a).
+
+Recursive Extraction x1.
diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
new file mode 100644
index 0000000000..668a55977d
--- /dev/null
+++ b/test-suite/output/FloatSyntax.out
@@ -0,0 +1,40 @@
+2%float
+     : float
+2.5%float
+     : float
+(-2.5)%float
+     : float
+2.4999999999999999e+123%float
+     : float
+(-2.5000000000000001e-123)%float
+     : float
+(2 + 2)%float
+     : float
+(2.5 + 2.5)%float
+     : float
+2
+     : float
+2.5
+     : float
+-2.5
+     : float
+2.4999999999999999e+123
+     : float
+-2.5000000000000001e-123
+     : float
+2 + 2
+     : float
+2.5 + 2.5
+     : float
+2
+     : nat
+2%float
+     : float
+t = 2%flt
+     : float
+t = 2%flt
+     : float
+2
+     : nat
+2
+     : float
diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
new file mode 100644
index 0000000000..85f611352c
--- /dev/null
+++ b/test-suite/output/FloatSyntax.v
@@ -0,0 +1,37 @@
+Require Import Floats.
+
+Check 2%float.
+Check 2.5%float.
+Check (-2.5)%float.
+(* Avoid exponents with less than three digits as they are usually
+   displayed with two digits (1e7 is displayed 1e+07) except on
+   Windows where three digits are used (1e+007). *)
+Check 2.5e123%float.
+Check (-2.5e-123)%float.
+Check (2 + 2)%float.
+Check (2.5 + 2.5)%float.
+
+Open Scope float_scope.
+
+Check 2.
+Check 2.5.
+Check (-2.5).
+Check 2.5e123.
+Check (-2.5e-123).
+Check (2 + 2).
+Check (2.5 + 2.5).
+
+Open Scope nat_scope.
+
+Check 2.
+Check 2%float.
+
+Delimit Scope float_scope with flt.
+Definition t := 2%float.
+Print t.
+Delimit Scope nat_scope with float.
+Print t.
+Check 2.
+Close Scope nat_scope.
+Check 2.
+Close Scope float_scope.
diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v
new file mode 100644
index 0000000000..f8c5939d0a
--- /dev/null
+++ b/test-suite/primitive/float/add.v
@@ -0,0 +1,63 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+Definition five := Eval compute in of_int63 5%int63.
+
+Check (eq_refl : two + three = five).
+Check (eq_refl five <: two + three = five).
+Check (eq_refl five <<: two + three = five).
+Definition compute1 := Eval compute in two + three.
+Check (eq_refl compute1 : five = five).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge + tiny = huge).
+Check (eq_refl huge <: huge + tiny = huge).
+Check (eq_refl huge <<: huge + tiny = huge).
+Definition compute2 := Eval compute in huge + tiny.
+Check (eq_refl compute2 : huge = huge).
+
+Check (eq_refl : huge + huge = infinity).
+Check (eq_refl infinity <: huge + huge = infinity).
+Check (eq_refl infinity <<: huge + huge = infinity).
+Definition compute3 := Eval compute in huge + huge.
+Check (eq_refl compute3 : infinity = infinity).
+
+Check (eq_refl : one + nan = nan).
+Check (eq_refl nan <: one + nan = nan).
+Check (eq_refl nan <<: one + nan = nan).
+Definition compute4 := Eval compute in one + nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity + infinity = infinity).
+Check (eq_refl infinity <: infinity + infinity = infinity).
+Check (eq_refl infinity <<: infinity + infinity = infinity).
+Definition compute5 := Eval compute in infinity + infinity.
+Check (eq_refl compute5 : infinity = infinity).
+
+Check (eq_refl : infinity + neg_infinity = nan).
+Check (eq_refl nan <: infinity + neg_infinity = nan).
+Check (eq_refl nan <<: infinity + neg_infinity = nan).
+Definition compute6 := Eval compute in infinity + neg_infinity.
+Check (eq_refl compute6 : nan = nan).
+
+Check (eq_refl : zero + zero = zero).
+Check (eq_refl zero <: zero + zero = zero).
+Check (eq_refl zero <<: zero + zero = zero).
+Check (eq_refl : neg_zero + zero = zero).
+Check (eq_refl zero <: neg_zero + zero = zero).
+Check (eq_refl zero <<: neg_zero + zero = zero).
+Check (eq_refl : neg_zero + neg_zero = neg_zero).
+Check (eq_refl neg_zero <: neg_zero + neg_zero = neg_zero).
+Check (eq_refl neg_zero <<: neg_zero + neg_zero = neg_zero).
+Check (eq_refl : zero + neg_zero = zero).
+Check (eq_refl zero <: zero + neg_zero = zero).
+Check (eq_refl zero <<: zero + neg_zero = zero).
+
+Check (eq_refl : huge + neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <: huge + neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <<: huge + neg_infinity = neg_infinity).
diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v
new file mode 100644
index 0000000000..22e3fca844
--- /dev/null
+++ b/test-suite/primitive/float/classify.v
@@ -0,0 +1,33 @@
+Require Import ZArith Floats.
+
+Definition epsilon := Eval compute in ldexp one (-1024)%Z.
+
+Check (eq_refl : classify one = PNormal).
+Check (eq_refl : classify (- one)%float = NNormal).
+Check (eq_refl : classify epsilon = PSubn).
+Check (eq_refl : classify (- epsilon)%float = NSubn).
+Check (eq_refl : classify zero = PZero).
+Check (eq_refl : classify neg_zero = NZero).
+Check (eq_refl : classify infinity = PInf).
+Check (eq_refl : classify neg_infinity = NInf).
+Check (eq_refl : classify nan = NaN).
+
+Check (eq_refl PNormal <: classify one = PNormal).
+Check (eq_refl NNormal <: classify (- one)%float = NNormal).
+Check (eq_refl PSubn <: classify epsilon = PSubn).
+Check (eq_refl NSubn <: classify (- epsilon)%float = NSubn).
+Check (eq_refl PZero <: classify zero = PZero).
+Check (eq_refl NZero <: classify neg_zero = NZero).
+Check (eq_refl PInf <: classify infinity = PInf).
+Check (eq_refl NInf <: classify neg_infinity = NInf).
+Check (eq_refl NaN <: classify nan = NaN).
+
+Check (eq_refl PNormal <<: classify one = PNormal).
+Check (eq_refl NNormal <<: classify (- one)%float = NNormal).
+Check (eq_refl PSubn <<: classify epsilon = PSubn).
+Check (eq_refl NSubn <<: classify (- epsilon)%float = NSubn).
+Check (eq_refl PZero <<: classify zero = PZero).
+Check (eq_refl NZero <<: classify neg_zero = NZero).
+Check (eq_refl PInf <<: classify infinity = PInf).
+Check (eq_refl NInf <<: classify neg_infinity = NInf).
+Check (eq_refl NaN <<: classify nan = NaN).
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/coq_env_double_array.v b/test-suite/primitive/float/coq_env_double_array.v
new file mode 100644
index 0000000000..754ccb69aa
--- /dev/null
+++ b/test-suite/primitive/float/coq_env_double_array.v
@@ -0,0 +1,13 @@
+Require Import Floats.
+
+Goal True.
+pose (f := one).
+pose (f' := (-f)%float).
+
+(* this used to segfault when the coq_env array given to the
+   coq_interprete C function was an unboxed OCaml Double_array
+   (created by Array.map in csymtable.ml just before calling
+   eval_tcode) *)
+vm_compute in f'.
+
+Abort.
diff --git a/test-suite/primitive/float/div.v b/test-suite/primitive/float/div.v
new file mode 100644
index 0000000000..8e971f575b
--- /dev/null
+++ b/test-suite/primitive/float/div.v
@@ -0,0 +1,87 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+Definition six := Eval compute in of_int63 6%int63.
+
+Check (eq_refl : six / three = two).
+Check (eq_refl two <: six / three = two).
+Check (eq_refl two <<: six / three = two).
+Definition compute1 := Eval compute in six / three.
+Check (eq_refl compute1 : two = two).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge / tiny = infinity).
+Check (eq_refl infinity <: huge / tiny = infinity).
+Check (eq_refl infinity <<: huge / tiny = infinity).
+Definition compute2 := Eval compute in huge / tiny.
+Check (eq_refl compute2 : infinity = infinity).
+
+Check (eq_refl : huge / huge = one).
+Check (eq_refl one <: huge / huge = one).
+Check (eq_refl one <<: huge / huge = one).
+Definition compute3 := Eval compute in huge / huge.
+Check (eq_refl compute3 : one = one).
+
+Check (eq_refl : one / nan = nan).
+Check (eq_refl nan <: one / nan = nan).
+Check (eq_refl nan <<: one / nan = nan).
+Definition compute4 := Eval compute in one / nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity / infinity = nan).
+Check (eq_refl nan <: infinity / infinity = nan).
+Check (eq_refl nan <<: infinity / infinity = nan).
+Definition compute5 := Eval compute in infinity / infinity.
+Check (eq_refl compute5 : nan = nan).
+
+Check (eq_refl : infinity / neg_infinity = nan).
+Check (eq_refl nan <: infinity / neg_infinity = nan).
+Check (eq_refl nan <<: infinity / neg_infinity = nan).
+Definition compute6 := Eval compute in infinity / neg_infinity.
+Check (eq_refl compute6 : nan = nan).
+
+Check (eq_refl : zero / zero = nan).
+Check (eq_refl nan <: zero / zero = nan).
+Check (eq_refl nan <<: zero / zero = nan).
+Check (eq_refl : neg_zero / zero = nan).
+Check (eq_refl nan <: neg_zero / zero = nan).
+Check (eq_refl nan <<: neg_zero / zero = nan).
+
+Check (eq_refl : huge / neg_infinity = neg_zero).
+Check (eq_refl neg_zero <: huge / neg_infinity = neg_zero).
+Check (eq_refl neg_zero <<: huge / neg_infinity = neg_zero).
+
+Check (eq_refl : one / tiny = huge).
+Check (eq_refl huge <: one / tiny = huge).
+Check (eq_refl huge <<: one / tiny = huge).
+Check (eq_refl : one / huge = tiny).
+Check (eq_refl tiny <: one / huge = tiny).
+Check (eq_refl tiny <<: one / huge = tiny).
+Check (eq_refl : zero / huge = zero).
+Check (eq_refl zero <: zero / huge = zero).
+Check (eq_refl zero <<: zero / huge = zero).
+Check (eq_refl : zero / (-huge) = neg_zero).
+Check (eq_refl neg_zero <: zero / (-huge) = neg_zero).
+Check (eq_refl neg_zero <<: zero / (-huge) = neg_zero).
+
+Check (eq_refl : tiny / one = tiny).
+Check (eq_refl tiny <: tiny / one = tiny).
+Check (eq_refl tiny <<: tiny / one = tiny).
+Check (eq_refl : huge / one = huge).
+Check (eq_refl huge <: huge / one = huge).
+Check (eq_refl huge <<: huge / one = huge).
+Check (eq_refl : infinity / one = infinity).
+Check (eq_refl infinity <: infinity / one = infinity).
+Check (eq_refl infinity <<: infinity / one = infinity).
+
+Check (eq_refl : zero / infinity = zero).
+Check (eq_refl zero <: zero / infinity = zero).
+Check (eq_refl zero <<: zero / infinity = zero).
+Check (eq_refl : infinity / zero = infinity).
+Check (eq_refl infinity <: infinity / zero = infinity).
+Check (eq_refl infinity <<: infinity / zero = infinity).
diff --git a/test-suite/primitive/float/double_rounding.v b/test-suite/primitive/float/double_rounding.v
new file mode 100644
index 0000000000..e2356cdd7b
--- /dev/null
+++ b/test-suite/primitive/float/double_rounding.v
@@ -0,0 +1,38 @@
+Require Import Floats ZArith.
+
+(* This test check that there is no double rounding with 80 bits registers inside float computations *)
+
+Definition big_cbn := Eval cbn in ldexp one (53)%Z.
+Definition small_cbn := Eval cbn in (one + ldexp one (-52)%Z)%float.
+Definition result_cbn := Eval cbn in (big_cbn + small_cbn)%float.
+Definition check_cbn := Eval cbn in (big_cbn + one)%float.
+
+Check (eq_refl : (result_cbn ?= big_cbn)%float = FGt).
+Check (eq_refl : (check_cbn ?= big_cbn)%float = FEq).
+
+
+Definition big_cbv := Eval cbv in ldexp one (53)%Z.
+Definition small_cbv := Eval cbv in (one + ldexp one (-52)%Z)%float.
+Definition result_cbv := Eval cbv in (big_cbv + small_cbv)%float.
+Definition check_cbv := Eval cbv in (big_cbv + one)%float.
+
+Check (eq_refl : (result_cbv ?= big_cbv)%float = FGt).
+Check (eq_refl : (check_cbv ?= big_cbv)%float = FEq).
+
+
+Definition big_vm := Eval vm_compute in ldexp one (53)%Z.
+Definition small_vm := Eval vm_compute in (one + ldexp one (-52)%Z)%float.
+Definition result_vm := Eval vm_compute in (big_vm + small_vm)%float.
+Definition check_vm := Eval vm_compute in (big_vm + one)%float.
+
+Check (eq_refl : (result_vm ?= big_vm)%float = FGt).
+Check (eq_refl : (check_vm ?= big_vm)%float = FEq).
+
+
+Definition big_native := Eval native_compute in ldexp one (53)%Z.
+Definition small_native := Eval native_compute in (one + ldexp one (-52)%Z)%float.
+Definition result_native := Eval native_compute in (big_native + small_native)%float.
+Definition check_native := Eval native_compute in (big_native + one)%float.
+
+Check (eq_refl : (result_native ?= big_native)%float = FGt).
+Check (eq_refl : (check_native ?= big_native)%float = FEq).
diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v
new file mode 100644
index 0000000000..2a600429b1
--- /dev/null
+++ b/test-suite/primitive/float/frexp.v
@@ -0,0 +1,28 @@
+Require Import ZArith Floats.
+
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+Definition neg_one := Eval compute in (-one)%float.
+
+Check (eq_refl : let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <: let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <<: let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
+
+Check (eq_refl : let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <: let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <<: let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
+
+Check (eq_refl : let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <: let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <<: let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
+
+Check (eq_refl : let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <: let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <<: let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
+
+Check (eq_refl : let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF neg_one)) <: let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF neg_one)) <<: let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)).
+
+Check (eq_refl : let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <: let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <<: let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
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/test-suite/primitive/float/ldexp.v b/test-suite/primitive/float/ldexp.v
new file mode 100644
index 0000000000..a725deeeca
--- /dev/null
+++ b/test-suite/primitive/float/ldexp.v
@@ -0,0 +1,21 @@
+Require Import ZArith Int63 Floats.
+
+Check (eq_refl : ldexp one 9223372036854773807%Z = infinity).
+Check (eq_refl infinity <: ldexp one 9223372036854773807%Z = infinity).
+Check (eq_refl infinity <<: ldexp one 9223372036854773807%Z = infinity).
+
+Check (eq_refl : ldshiftexp one 9223372036854775807 = infinity).
+Check (eq_refl infinity <: ldshiftexp one 9223372036854775807 = infinity).
+Check (eq_refl infinity <<: ldshiftexp one 9223372036854775807 = infinity).
+
+Check (eq_refl : ldexp one (-2102) = 0%float).
+Check (eq_refl 0%float <: ldexp one (-2102) = 0%float).
+Check (eq_refl 0%float <<: ldexp one (-2102) = 0%float).
+
+Check (eq_refl : ldexp one (-3) = 0.125%float).
+Check (eq_refl 0.125%float <: ldexp one (-3) = 0.125%float).
+Check (eq_refl 0.125%float <<: ldexp one (-3) = 0.125%float).
+
+Check (eq_refl : ldexp one 3 = 8%float).
+Check (eq_refl 8%float <: ldexp one 3 = 8%float).
+Check (eq_refl 8%float <<: ldexp one 3 = 8%float).
diff --git a/test-suite/primitive/float/mul.v b/test-suite/primitive/float/mul.v
new file mode 100644
index 0000000000..91fe7e9791
--- /dev/null
+++ b/test-suite/primitive/float/mul.v
@@ -0,0 +1,83 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+Definition six := Eval compute in of_int63 6%int63.
+
+Check (eq_refl : three * two = six).
+Check (eq_refl six <: three * two = six).
+Check (eq_refl six <<: three * two = six).
+Definition compute1 := Eval compute in three * two.
+Check (eq_refl compute1 : six = six).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge * tiny = one).
+Check (eq_refl one <: huge * tiny = one).
+Check (eq_refl one <<: huge * tiny = one).
+Definition compute2 := Eval compute in huge * tiny.
+Check (eq_refl compute2 : one = one).
+
+Check (eq_refl : huge * huge = infinity).
+Check (eq_refl infinity <: huge * huge = infinity).
+Check (eq_refl infinity <<: huge * huge = infinity).
+Definition compute3 := Eval compute in huge * huge.
+Check (eq_refl compute3 : infinity = infinity).
+
+Check (eq_refl : one * nan = nan).
+Check (eq_refl nan <: one * nan = nan).
+Check (eq_refl nan <<: one * nan = nan).
+Definition compute4 := Eval compute in one * nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity * infinity = infinity).
+Check (eq_refl infinity <: infinity * infinity = infinity).
+Check (eq_refl infinity <<: infinity * infinity = infinity).
+Definition compute5 := Eval compute in infinity * infinity.
+Check (eq_refl compute5 : infinity = infinity).
+
+Check (eq_refl : infinity * neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <: infinity * neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <<: infinity * neg_infinity = neg_infinity).
+Definition compute6 := Eval compute in infinity * neg_infinity.
+Check (eq_refl compute6 : neg_infinity = neg_infinity).
+
+Check (eq_refl : zero * zero = zero).
+Check (eq_refl zero <: zero * zero = zero).
+Check (eq_refl zero <<: zero * zero = zero).
+Check (eq_refl : neg_zero * zero = neg_zero).
+Check (eq_refl neg_zero <: neg_zero * zero = neg_zero).
+Check (eq_refl neg_zero <<: neg_zero * zero = neg_zero).
+Check (eq_refl : neg_zero * neg_zero = zero).
+Check (eq_refl zero <: neg_zero * neg_zero = zero).
+Check (eq_refl zero <<: neg_zero * neg_zero = zero).
+Check (eq_refl : zero * neg_zero = neg_zero).
+Check (eq_refl neg_zero <: zero * neg_zero = neg_zero).
+Check (eq_refl neg_zero <<: zero * neg_zero = neg_zero).
+
+Check (eq_refl : huge * neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <: huge * neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <<: huge * neg_infinity = neg_infinity).
+
+Check (eq_refl : one * tiny = tiny).
+Check (eq_refl tiny <: one * tiny = tiny).
+Check (eq_refl tiny <<: one * tiny = tiny).
+Check (eq_refl : one * huge = huge).
+Check (eq_refl huge <: one * huge = huge).
+Check (eq_refl huge <<: one * huge = huge).
+Check (eq_refl : zero * huge = zero).
+Check (eq_refl zero <: zero * huge = zero).
+Check (eq_refl zero <<: zero * huge = zero).
+Check (eq_refl : zero * (-huge) = neg_zero).
+Check (eq_refl neg_zero <: zero * (-huge) = neg_zero).
+Check (eq_refl neg_zero <<: zero * (-huge) = neg_zero).
+
+Check (eq_refl : zero * infinity = nan).
+Check (eq_refl nan <: zero * infinity = nan).
+Check (eq_refl nan <<: zero * infinity = nan).
+Check (eq_refl : neg_infinity * zero = nan).
+Check (eq_refl nan <: neg_infinity * zero = nan).
+Check (eq_refl nan <<: neg_infinity * zero = nan).
diff --git a/test-suite/primitive/float/next_up_down.v b/test-suite/primitive/float/next_up_down.v
new file mode 100644
index 0000000000..4f8427dc5b
--- /dev/null
+++ b/test-suite/primitive/float/next_up_down.v
@@ -0,0 +1,122 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition f0 := zero.
+Definition f1 := neg_zero.
+Definition f2 := Eval compute in ldexp one 0.
+Definition f3 := Eval compute in -f1.
+(* smallest positive float *)
+Definition f4 := Eval compute in ldexp one (-1074).
+Definition f5 := Eval compute in -f3.
+Definition f6 := infinity.
+Definition f7 := neg_infinity.
+Definition f8 := Eval compute in ldexp one (-1).
+Definition f9 := Eval compute in -f8.
+Definition f10 := Eval compute in of_int63 42.
+Definition f11 := Eval compute in -f10.
+(* max float *)
+Definition f12 := Eval compute in ldexp (of_int63 9007199254740991) 1024.
+Definition f13 := Eval compute in -f12.
+(* smallest positive normalized float *)
+Definition f14 := Eval compute in ldexp one (-1022).
+Definition f15 := Eval compute in -f14.
+
+Check (eq_refl : Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
+Check (eq_refl : Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
+Check (eq_refl : Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
+Check (eq_refl : Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
+Check (eq_refl : Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
+Check (eq_refl : Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
+Check (eq_refl : Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
+Check (eq_refl : Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
+Check (eq_refl : Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
+Check (eq_refl : Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
+Check (eq_refl : Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
+Check (eq_refl : Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
+Check (eq_refl : Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
+Check (eq_refl : Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
+Check (eq_refl : Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
+Check (eq_refl : Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
+Check (eq_refl : Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
+Check (eq_refl : Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
+Check (eq_refl : Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
+Check (eq_refl : Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
+Check (eq_refl : Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
+Check (eq_refl : Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
+Check (eq_refl : Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
+Check (eq_refl : Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
+Check (eq_refl : Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
+Check (eq_refl : Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
+Check (eq_refl : Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
+Check (eq_refl : Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
+Check (eq_refl : Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
+Check (eq_refl : Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
+Check (eq_refl : Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
+Check (eq_refl : Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
+
+Check (eq_refl (SF64succ (Prim2SF f0)) <: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
+Check (eq_refl (SF64pred (Prim2SF f0)) <: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
+Check (eq_refl (SF64succ (Prim2SF f1)) <: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
+Check (eq_refl (SF64pred (Prim2SF f1)) <: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
+Check (eq_refl (SF64succ (Prim2SF f2)) <: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
+Check (eq_refl (SF64pred (Prim2SF f2)) <: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
+Check (eq_refl (SF64succ (Prim2SF f3)) <: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
+Check (eq_refl (SF64pred (Prim2SF f3)) <: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
+Check (eq_refl (SF64succ (Prim2SF f4)) <: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
+Check (eq_refl (SF64pred (Prim2SF f4)) <: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
+Check (eq_refl (SF64succ (Prim2SF f5)) <: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
+Check (eq_refl (SF64pred (Prim2SF f5)) <: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
+Check (eq_refl (SF64succ (Prim2SF f6)) <: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
+Check (eq_refl (SF64pred (Prim2SF f6)) <: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
+Check (eq_refl (SF64succ (Prim2SF f7)) <: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
+Check (eq_refl (SF64pred (Prim2SF f7)) <: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
+Check (eq_refl (SF64succ (Prim2SF f8)) <: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
+Check (eq_refl (SF64pred (Prim2SF f8)) <: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
+Check (eq_refl (SF64succ (Prim2SF f9)) <: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
+Check (eq_refl (SF64pred (Prim2SF f9)) <: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
+Check (eq_refl (SF64succ (Prim2SF f10)) <: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
+Check (eq_refl (SF64pred (Prim2SF f10)) <: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
+Check (eq_refl (SF64succ (Prim2SF f11)) <: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
+Check (eq_refl (SF64pred (Prim2SF f11)) <: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
+Check (eq_refl (SF64succ (Prim2SF f12)) <: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
+Check (eq_refl (SF64pred (Prim2SF f12)) <: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
+Check (eq_refl (SF64succ (Prim2SF f13)) <: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
+Check (eq_refl (SF64pred (Prim2SF f13)) <: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
+Check (eq_refl (SF64succ (Prim2SF f14)) <: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
+Check (eq_refl (SF64pred (Prim2SF f14)) <: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
+Check (eq_refl (SF64succ (Prim2SF f15)) <: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
+Check (eq_refl (SF64pred (Prim2SF f15)) <: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
+
+Check (eq_refl (SF64succ (Prim2SF f0)) <<: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
+Check (eq_refl (SF64pred (Prim2SF f0)) <<: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
+Check (eq_refl (SF64succ (Prim2SF f1)) <<: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
+Check (eq_refl (SF64pred (Prim2SF f1)) <<: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
+Check (eq_refl (SF64succ (Prim2SF f2)) <<: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
+Check (eq_refl (SF64pred (Prim2SF f2)) <<: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
+Check (eq_refl (SF64succ (Prim2SF f3)) <<: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
+Check (eq_refl (SF64pred (Prim2SF f3)) <<: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
+Check (eq_refl (SF64succ (Prim2SF f4)) <<: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
+Check (eq_refl (SF64pred (Prim2SF f4)) <<: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
+Check (eq_refl (SF64succ (Prim2SF f5)) <<: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
+Check (eq_refl (SF64pred (Prim2SF f5)) <<: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
+Check (eq_refl (SF64succ (Prim2SF f6)) <<: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
+Check (eq_refl (SF64pred (Prim2SF f6)) <<: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
+Check (eq_refl (SF64succ (Prim2SF f7)) <<: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
+Check (eq_refl (SF64pred (Prim2SF f7)) <<: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
+Check (eq_refl (SF64succ (Prim2SF f8)) <<: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
+Check (eq_refl (SF64pred (Prim2SF f8)) <<: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
+Check (eq_refl (SF64succ (Prim2SF f9)) <<: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
+Check (eq_refl (SF64pred (Prim2SF f9)) <<: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
+Check (eq_refl (SF64succ (Prim2SF f10)) <<: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
+Check (eq_refl (SF64pred (Prim2SF f10)) <<: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
+Check (eq_refl (SF64succ (Prim2SF f11)) <<: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
+Check (eq_refl (SF64pred (Prim2SF f11)) <<: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
+Check (eq_refl (SF64succ (Prim2SF f12)) <<: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
+Check (eq_refl (SF64pred (Prim2SF f12)) <<: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
+Check (eq_refl (SF64succ (Prim2SF f13)) <<: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
+Check (eq_refl (SF64pred (Prim2SF f13)) <<: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
+Check (eq_refl (SF64succ (Prim2SF f14)) <<: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
+Check (eq_refl (SF64pred (Prim2SF f14)) <<: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
+Check (eq_refl (SF64succ (Prim2SF f15)) <<: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
+Check (eq_refl (SF64pred (Prim2SF f15)) <<: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
diff --git a/test-suite/primitive/float/normfr_mantissa.v b/test-suite/primitive/float/normfr_mantissa.v
new file mode 100644
index 0000000000..28bd1c03f5
--- /dev/null
+++ b/test-suite/primitive/float/normfr_mantissa.v
@@ -0,0 +1,28 @@
+Require Import Int63 ZArith Floats.
+
+Definition half := ldexp one (-1)%Z.
+Definition three_quarters := (half + (ldexp one (-2)%Z))%float.
+
+Check (eq_refl : normfr_mantissa one = 0%int63).
+Check (eq_refl : normfr_mantissa half = (1 << 52)%int63).
+Check (eq_refl : normfr_mantissa (-half) = (1 << 52)%int63).
+Check (eq_refl : normfr_mantissa (-one) = 0%int63).
+Check (eq_refl : normfr_mantissa zero = 0%int63).
+Check (eq_refl : normfr_mantissa nan = 0%int63).
+Check (eq_refl : normfr_mantissa three_quarters = (3 << 51)%int63).
+
+Check (eq_refl 0%int63 <: normfr_mantissa one = 0%int63).
+Check (eq_refl (1 << 52)%int63 <: normfr_mantissa half = (1 << 52)%int63).
+Check (eq_refl (1 << 52)%int63 <: normfr_mantissa (-half) = (1 << 52)%int63).
+Check (eq_refl 0%int63 <: normfr_mantissa (-one) = 0%int63).
+Check (eq_refl 0%int63 <: normfr_mantissa zero = 0%int63).
+Check (eq_refl 0%int63 <: normfr_mantissa nan = 0%int63).
+Check (eq_refl (3 << 51)%int63 <: normfr_mantissa three_quarters = (3 << 51)%int63).
+
+Check (eq_refl 0%int63 <<: normfr_mantissa one = 0%int63).
+Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa half = (1 << 52)%int63).
+Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa (-half) = (1 << 52)%int63).
+Check (eq_refl 0%int63 <<: normfr_mantissa (-one) = 0%int63).
+Check (eq_refl 0%int63 <<: normfr_mantissa zero = 0%int63).
+Check (eq_refl 0%int63 <<: normfr_mantissa nan = 0%int63).
+Check (eq_refl (3 << 51)%int63 <<: normfr_mantissa three_quarters = (3 << 51)%int63).
diff --git a/test-suite/primitive/float/spec_conv.v b/test-suite/primitive/float/spec_conv.v
new file mode 100644
index 0000000000..a610d39671
--- /dev/null
+++ b/test-suite/primitive/float/spec_conv.v
@@ -0,0 +1,46 @@
+Require Import ZArith Floats.
+
+Definition two := Eval compute in (one + one)%float.
+Definition half := Eval compute in (one / two)%float.
+Definition huge := Eval compute in ldexp one (1023)%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+
+Check (eq_refl : SF2Prim (Prim2SF zero) = zero).
+Check (eq_refl : SF2Prim (Prim2SF neg_zero) = neg_zero).
+Check (eq_refl : SF2Prim (Prim2SF one) = one).
+Check (eq_refl : SF2Prim (Prim2SF (-one)) = (-one)%float).
+Check (eq_refl : SF2Prim (Prim2SF infinity) = infinity).
+Check (eq_refl : SF2Prim (Prim2SF neg_infinity) = neg_infinity).
+Check (eq_refl : SF2Prim (Prim2SF huge) = huge).
+Check (eq_refl : SF2Prim (Prim2SF tiny) = tiny).
+Check (eq_refl : SF2Prim (Prim2SF denorm) = denorm).
+Check (eq_refl : SF2Prim (Prim2SF nan) = nan).
+Check (eq_refl : SF2Prim (Prim2SF two) = two).
+Check (eq_refl : SF2Prim (Prim2SF half) = half).
+
+Check (eq_refl zero <: SF2Prim (Prim2SF zero) = zero).
+Check (eq_refl neg_zero <: SF2Prim (Prim2SF neg_zero) = neg_zero).
+Check (eq_refl one <: SF2Prim (Prim2SF one) = one).
+Check (eq_refl (-one)%float <: SF2Prim (Prim2SF (-one)) = (-one)%float).
+Check (eq_refl infinity <: SF2Prim (Prim2SF infinity) = infinity).
+Check (eq_refl neg_infinity <: SF2Prim (Prim2SF neg_infinity) = neg_infinity).
+Check (eq_refl huge <: SF2Prim (Prim2SF huge) = huge).
+Check (eq_refl tiny <: SF2Prim (Prim2SF tiny) = tiny).
+Check (eq_refl denorm <: SF2Prim (Prim2SF denorm) = denorm).
+Check (eq_refl nan <: SF2Prim (Prim2SF nan) = nan).
+Check (eq_refl two <: SF2Prim (Prim2SF two) = two).
+Check (eq_refl half <: SF2Prim (Prim2SF half) = half).
+
+Check (eq_refl zero <<: SF2Prim (Prim2SF zero) = zero).
+Check (eq_refl neg_zero <<: SF2Prim (Prim2SF neg_zero) = neg_zero).
+Check (eq_refl one <<: SF2Prim (Prim2SF one) = one).
+Check (eq_refl (-one)%float <<: SF2Prim (Prim2SF (-one)) = (-one)%float).
+Check (eq_refl infinity <<: SF2Prim (Prim2SF infinity) = infinity).
+Check (eq_refl neg_infinity <<: SF2Prim (Prim2SF neg_infinity) = neg_infinity).
+Check (eq_refl huge <<: SF2Prim (Prim2SF huge) = huge).
+Check (eq_refl tiny <<: SF2Prim (Prim2SF tiny) = tiny).
+Check (eq_refl denorm <<: SF2Prim (Prim2SF denorm) = denorm).
+Check (eq_refl nan <<: SF2Prim (Prim2SF nan) = nan).
+Check (eq_refl two <<: SF2Prim (Prim2SF two) = two).
+Check (eq_refl half <<: SF2Prim (Prim2SF half) = half).
diff --git a/test-suite/primitive/float/sqrt.v b/test-suite/primitive/float/sqrt.v
new file mode 100644
index 0000000000..04c8ab035d
--- /dev/null
+++ b/test-suite/primitive/float/sqrt.v
@@ -0,0 +1,49 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition three := Eval compute in of_int63 3%int63.
+Definition nine := Eval compute in of_int63 9%int63.
+
+Check (eq_refl : sqrt nine = three).
+Check (eq_refl three <: sqrt nine = three).
+Definition compute1 := Eval compute in sqrt nine.
+Check (eq_refl : three = three).
+
+Definition huge := Eval compute in ldexp one (1023)%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+
+Goal (Prim2SF (sqrt huge) = SF64sqrt (Prim2SF huge)).
+  now compute. Undo. now vm_compute.
+Qed.
+
+Goal (Prim2SF (sqrt tiny) = SF64sqrt (Prim2SF tiny)).
+  now compute. Undo. now vm_compute.
+Qed.
+
+Goal (Prim2SF (sqrt denorm) = SF64sqrt (Prim2SF denorm)).
+  now compute. Undo. now vm_compute.
+Qed.
+
+Check (eq_refl : sqrt neg_zero = neg_zero).
+Check (eq_refl neg_zero <: sqrt neg_zero = neg_zero).
+Check (eq_refl neg_zero <<: sqrt neg_zero = neg_zero).
+Check (eq_refl : sqrt zero = zero).
+Check (eq_refl zero <: sqrt zero = zero).
+Check (eq_refl zero <<: sqrt zero = zero).
+Check (eq_refl : sqrt one = one).
+Check (eq_refl one <: sqrt one = one).
+Check (eq_refl one <<: sqrt one = one).
+Check (eq_refl : sqrt (-one) = nan).
+Check (eq_refl nan <: sqrt (-one) = nan).
+Check (eq_refl nan <<: sqrt (-one) = nan).
+Check (eq_refl : sqrt infinity = infinity).
+Check (eq_refl infinity <: sqrt infinity = infinity).
+Check (eq_refl infinity <<: sqrt infinity = infinity).
+Check (eq_refl : sqrt neg_infinity = nan).
+Check (eq_refl nan <: sqrt neg_infinity = nan).
+Check (eq_refl nan <<: sqrt neg_infinity = nan).
+Check (eq_refl : sqrt infinity = infinity).
+Check (eq_refl infinity <: sqrt infinity = infinity).
+Check (eq_refl infinity <<: sqrt infinity = infinity).
diff --git a/test-suite/primitive/float/sub.v b/test-suite/primitive/float/sub.v
new file mode 100644
index 0000000000..fc068cb585
--- /dev/null
+++ b/test-suite/primitive/float/sub.v
@@ -0,0 +1,62 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+
+Check (eq_refl : three - two = one).
+Check (eq_refl one <: three - two = one).
+Check (eq_refl one <<: three - two = one).
+Definition compute1 := Eval compute in three - two.
+Check (eq_refl compute1 : one = one).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge - tiny = huge).
+Check (eq_refl huge <: huge - tiny = huge).
+Check (eq_refl huge <<: huge - tiny = huge).
+Definition compute2 := Eval compute in huge - tiny.
+Check (eq_refl compute2 : huge = huge).
+
+Check (eq_refl : huge - huge = zero).
+Check (eq_refl zero <: huge - huge = zero).
+Check (eq_refl zero <<: huge - huge = zero).
+Definition compute3 := Eval compute in huge - huge.
+Check (eq_refl compute3 : zero = zero).
+
+Check (eq_refl : one - nan = nan).
+Check (eq_refl nan <: one - nan = nan).
+Check (eq_refl nan <<: one - nan = nan).
+Definition compute4 := Eval compute in one - nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity - infinity = nan).
+Check (eq_refl nan <: infinity - infinity = nan).
+Check (eq_refl nan <<: infinity - infinity = nan).
+Definition compute5 := Eval compute in infinity - infinity.
+Check (eq_refl compute5 : nan = nan).
+
+Check (eq_refl : infinity - neg_infinity = infinity).
+Check (eq_refl infinity <: infinity - neg_infinity = infinity).
+Check (eq_refl infinity <<: infinity - neg_infinity = infinity).
+Definition compute6 := Eval compute in infinity - neg_infinity.
+Check (eq_refl compute6 : infinity = infinity).
+
+Check (eq_refl : zero - zero = zero).
+Check (eq_refl zero <: zero - zero = zero).
+Check (eq_refl zero <<: zero - zero = zero).
+Check (eq_refl : neg_zero - zero = neg_zero).
+Check (eq_refl neg_zero <: neg_zero - zero = neg_zero).
+Check (eq_refl neg_zero <<: neg_zero - zero = neg_zero).
+Check (eq_refl : neg_zero - neg_zero = zero).
+Check (eq_refl zero <: neg_zero - neg_zero = zero).
+Check (eq_refl zero <<: neg_zero - neg_zero = zero).
+Check (eq_refl : zero - neg_zero = zero).
+Check (eq_refl zero <: zero - neg_zero = zero).
+Check (eq_refl zero <<: zero - neg_zero = zero).
+
+Check (eq_refl : huge - neg_infinity = infinity).
+Check (eq_refl infinity <: huge - neg_infinity = infinity).
+Check (eq_refl infinity <<: huge - neg_infinity = infinity).
diff --git a/test-suite/primitive/float/syntax.v b/test-suite/primitive/float/syntax.v
new file mode 100644
index 0000000000..cc0bbcf628
--- /dev/null
+++ b/test-suite/primitive/float/syntax.v
@@ -0,0 +1,13 @@
+Require Import Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in one + one.
+Definition half := Eval compute in one / two.
+
+Check (eq_refl : 1.5 = one + half).
+Check (eq_refl : 15e-1 = one + half).
+Check (eq_refl : 150e-2 = one + half).
+Check (eq_refl : 0.15e+1 = one + half).
+Check (eq_refl : 0.15e1 = one + half).
+Check (eq_refl : 0.0015e3 = one + half).
diff --git a/test-suite/primitive/float/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v
new file mode 100644
index 0000000000..82e00b8532
--- /dev/null
+++ b/test-suite/primitive/float/valid_binary_conv.v
@@ -0,0 +1,46 @@
+Require Import ZArith Floats.
+
+Definition two := Eval compute in (one + one)%float.
+Definition half := Eval compute in (one / two)%float.
+Definition huge := Eval compute in ldexp one (1023)%Z.
+Definition tiny := Eval compute in ldexp one (-1022)%Z.
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+
+Check (eq_refl : valid_binary (Prim2SF zero) = true).
+Check (eq_refl : valid_binary (Prim2SF neg_zero) = true).
+Check (eq_refl : valid_binary (Prim2SF one) = true).
+Check (eq_refl : valid_binary (Prim2SF (-one)) = true).
+Check (eq_refl : valid_binary (Prim2SF infinity) = true).
+Check (eq_refl : valid_binary (Prim2SF neg_infinity) = true).
+Check (eq_refl : valid_binary (Prim2SF huge) = true).
+Check (eq_refl : valid_binary (Prim2SF tiny) = true).
+Check (eq_refl : valid_binary (Prim2SF denorm) = true).
+Check (eq_refl : valid_binary (Prim2SF nan) = true).
+Check (eq_refl : valid_binary (Prim2SF two) = true).
+Check (eq_refl : valid_binary (Prim2SF half) = true).
+
+Check (eq_refl true <: valid_binary (Prim2SF zero) = true).
+Check (eq_refl true <: valid_binary (Prim2SF neg_zero) = true).
+Check (eq_refl true <: valid_binary (Prim2SF one) = true).
+Check (eq_refl true <: valid_binary (Prim2SF (-one)) = true).
+Check (eq_refl true <: valid_binary (Prim2SF infinity) = true).
+Check (eq_refl true <: valid_binary (Prim2SF neg_infinity) = true).
+Check (eq_refl true <: valid_binary (Prim2SF huge) = true).
+Check (eq_refl true <: valid_binary (Prim2SF tiny) = true).
+Check (eq_refl true <: valid_binary (Prim2SF denorm) = true).
+Check (eq_refl true <: valid_binary (Prim2SF nan) = true).
+Check (eq_refl true <: valid_binary (Prim2SF two) = true).
+Check (eq_refl true <: valid_binary (Prim2SF half) = true).
+
+Check (eq_refl true <<: valid_binary (Prim2SF zero) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF neg_zero) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF one) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF (-one)) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF infinity) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF neg_infinity) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF huge) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF tiny) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF denorm) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF nan) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF two) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF half) = true).
diff --git a/test-suite/primitive/float/zero.v b/test-suite/primitive/float/zero.v
new file mode 100644
index 0000000000..75348d4657
--- /dev/null
+++ b/test-suite/primitive/float/zero.v
@@ -0,0 +1,7 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Fail Check (eq_refl : zero = neg_zero).
+Fail Check (eq_refl <: zero = neg_zero).
+Fail Check (eq_refl <<: zero = neg_zero).
diff --git a/test-suite/arithmetic/add.v b/test-suite/primitive/uint63/add.v
index fb7eb1d53c..fb7eb1d53c 100644
--- a/test-suite/arithmetic/add.v
+++ b/test-suite/primitive/uint63/add.v
diff --git a/test-suite/arithmetic/addc.v b/test-suite/primitive/uint63/addc.v
index 432aec0291..432aec0291 100644
--- a/test-suite/arithmetic/addc.v
+++ b/test-suite/primitive/uint63/addc.v
diff --git a/test-suite/arithmetic/addcarryc.v b/test-suite/primitive/uint63/addcarryc.v
index a4430769ca..a4430769ca 100644
--- a/test-suite/arithmetic/addcarryc.v
+++ b/test-suite/primitive/uint63/addcarryc.v
diff --git a/test-suite/arithmetic/addmuldiv.v b/test-suite/primitive/uint63/addmuldiv.v
index 72b0164b49..72b0164b49 100644
--- a/test-suite/arithmetic/addmuldiv.v
+++ b/test-suite/primitive/uint63/addmuldiv.v
diff --git a/test-suite/arithmetic/compare.v b/test-suite/primitive/uint63/compare.v
index a8d1ea1226..a8d1ea1226 100644
--- a/test-suite/arithmetic/compare.v
+++ b/test-suite/primitive/uint63/compare.v
diff --git a/test-suite/arithmetic/div.v b/test-suite/primitive/uint63/div.v
index 0ee0b91580..0ee0b91580 100644
--- a/test-suite/arithmetic/div.v
+++ b/test-suite/primitive/uint63/div.v
diff --git a/test-suite/arithmetic/diveucl.v b/test-suite/primitive/uint63/diveucl.v
index 8f88a0f356..8f88a0f356 100644
--- a/test-suite/arithmetic/diveucl.v
+++ b/test-suite/primitive/uint63/diveucl.v
diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/primitive/uint63/diveucl_21.v
index b12dba429c..b12dba429c 100644
--- a/test-suite/arithmetic/diveucl_21.v
+++ b/test-suite/primitive/uint63/diveucl_21.v
diff --git a/test-suite/arithmetic/eqb.v b/test-suite/primitive/uint63/eqb.v
index dcc0b71f6d..dcc0b71f6d 100644
--- a/test-suite/arithmetic/eqb.v
+++ b/test-suite/primitive/uint63/eqb.v
diff --git a/test-suite/arithmetic/head0.v b/test-suite/primitive/uint63/head0.v
index f4234d2605..f4234d2605 100644
--- a/test-suite/arithmetic/head0.v
+++ b/test-suite/primitive/uint63/head0.v
diff --git a/test-suite/arithmetic/isint.v b/test-suite/primitive/uint63/isint.v
index c215caa878..c215caa878 100644
--- a/test-suite/arithmetic/isint.v
+++ b/test-suite/primitive/uint63/isint.v
diff --git a/test-suite/arithmetic/land.v b/test-suite/primitive/uint63/land.v
index 0ea6fd90b6..0ea6fd90b6 100644
--- a/test-suite/arithmetic/land.v
+++ b/test-suite/primitive/uint63/land.v
diff --git a/test-suite/arithmetic/leb.v b/test-suite/primitive/uint63/leb.v
index 5354919978..5354919978 100644
--- a/test-suite/arithmetic/leb.v
+++ b/test-suite/primitive/uint63/leb.v
diff --git a/test-suite/arithmetic/lor.v b/test-suite/primitive/uint63/lor.v
index 9c3b85c054..9c3b85c054 100644
--- a/test-suite/arithmetic/lor.v
+++ b/test-suite/primitive/uint63/lor.v
diff --git a/test-suite/arithmetic/lsl.v b/test-suite/primitive/uint63/lsl.v
index 70f3b90140..70f3b90140 100644
--- a/test-suite/arithmetic/lsl.v
+++ b/test-suite/primitive/uint63/lsl.v
diff --git a/test-suite/arithmetic/lsr.v b/test-suite/primitive/uint63/lsr.v
index c36c24e237..c36c24e237 100644
--- a/test-suite/arithmetic/lsr.v
+++ b/test-suite/primitive/uint63/lsr.v
diff --git a/test-suite/arithmetic/ltb.v b/test-suite/primitive/uint63/ltb.v
index 7ae5ac6493..7ae5ac6493 100644
--- a/test-suite/arithmetic/ltb.v
+++ b/test-suite/primitive/uint63/ltb.v
diff --git a/test-suite/arithmetic/lxor.v b/test-suite/primitive/uint63/lxor.v
index b453fc7697..b453fc7697 100644
--- a/test-suite/arithmetic/lxor.v
+++ b/test-suite/primitive/uint63/lxor.v
diff --git a/test-suite/arithmetic/mod.v b/test-suite/primitive/uint63/mod.v
index 5307eed493..5307eed493 100644
--- a/test-suite/arithmetic/mod.v
+++ b/test-suite/primitive/uint63/mod.v
diff --git a/test-suite/arithmetic/mul.v b/test-suite/primitive/uint63/mul.v
index 9480e8cd46..9480e8cd46 100644
--- a/test-suite/arithmetic/mul.v
+++ b/test-suite/primitive/uint63/mul.v
diff --git a/test-suite/arithmetic/mulc.v b/test-suite/primitive/uint63/mulc.v
index e10855bafa..e10855bafa 100644
--- a/test-suite/arithmetic/mulc.v
+++ b/test-suite/primitive/uint63/mulc.v
diff --git a/test-suite/arithmetic/reduction.v b/test-suite/primitive/uint63/reduction.v
index 00e067ac5a..00e067ac5a 100644
--- a/test-suite/arithmetic/reduction.v
+++ b/test-suite/primitive/uint63/reduction.v
diff --git a/test-suite/arithmetic/sub.v b/test-suite/primitive/uint63/sub.v
index 1606fd2aa1..1606fd2aa1 100644
--- a/test-suite/arithmetic/sub.v
+++ b/test-suite/primitive/uint63/sub.v
diff --git a/test-suite/arithmetic/subc.v b/test-suite/primitive/uint63/subc.v
index fc4067e48b..fc4067e48b 100644
--- a/test-suite/arithmetic/subc.v
+++ b/test-suite/primitive/uint63/subc.v
diff --git a/test-suite/arithmetic/subcarryc.v b/test-suite/primitive/uint63/subcarryc.v
index e81b6536b2..e81b6536b2 100644
--- a/test-suite/arithmetic/subcarryc.v
+++ b/test-suite/primitive/uint63/subcarryc.v
diff --git a/test-suite/arithmetic/tail0.v b/test-suite/primitive/uint63/tail0.v
index c9d426087a..c9d426087a 100644
--- a/test-suite/arithmetic/tail0.v
+++ b/test-suite/primitive/uint63/tail0.v
diff --git a/test-suite/arithmetic/unsigned.v b/test-suite/primitive/uint63/unsigned.v
index 82920bd201..82920bd201 100644
--- a/test-suite/arithmetic/unsigned.v
+++ b/test-suite/primitive/uint63/unsigned.v