Coq: real built-ins for AArch64

1 files changed, 18 insertions, 0 deletions

diff --git a/lib/coq/Sail2_real.v b/lib/coq/Sail2_real.v
new file mode 100644
index 00000000..49023d4c
--- /dev/null
+++ b/lib/coq/Sail2_real.v
@@ -0,0 +1,18 @@
+Require Export Rbase.
+Require Import Reals.
+Require Export ROrderedType.
+
+Definition realFromFrac (num denom : Z) : R := Rdiv (IZR num) (IZR denom).
+
+Definition gteq_real (x y : R) : bool := if Rge_dec x y then true else false.
+Definition lteq_real (x y : R) : bool := if Rle_dec x y then true else false.
+Definition gt_real (x y : R) : bool := if Rgt_dec x y then true else false.
+Definition lt_real (x y : R) : bool := if Rlt_dec x y then true else false.
+
+(* Export select definitions from outside of Rbase *)
+Definition powerRZ := powerRZ.
+Definition Rabs := Rabs.
+
+(* Use flocq definitions, but without making the whole library a dependency. *)
+Definition Zfloor (x : R) := (up x - 1)%Z.
+Definition Zceil (x : R) := (- Zfloor (- x))%Z.