Add some ZRange operations

1 files changed, 36 insertions, 0 deletions

diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
new file mode 100644
index 000000000..7d9b24c40
--- /dev/null
+++ b/src/Util/ZRange/Operations.v
@@ -0,0 +1,36 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.Notations.
+
+Module ZRange.
+  Local Open Scope zrange_scope.
+
+  Local Notation eta v := r[ lower v ~> upper v ].
+
+  Definition normalize (v : zrange) : zrange
+    := r[ Z.min (lower v) (upper v) ~> Z.max (lower v) (upper v) ].
+
+  Definition abs (v : zrange) : zrange
+    := let (l, u) := eta v in
+       r[ 0 ~> Z.max (Z.abs l) (Z.abs u) ].
+
+  Definition two_corners (f : Z -> Z) (v : zrange) : zrange
+    := let (l, u) := eta v in
+       r[ Z.min (f l) (f u) ~> Z.max (f l) (f u) ].
+
+  Definition union (x y : zrange) : zrange
+    := let (lx, ux) := eta x in
+       let (ly, uy) := eta y in
+       r[ Z.min lx ly ~> Z.max ux uy ].
+
+  Definition four_corners (f : Z -> Z -> Z) (x y : zrange) : zrange
+    := let (lx, ux) := eta x in
+       union (two_corners (f lx) y)
+             (two_corners (f ux) y).
+
+  Definition eight_corners (f : Z -> Z -> Z -> Z) (x y z : zrange) : zrange
+    := let (lx, ux) := eta x in
+       union (four_corners (f lx) y z)
+             (four_corners (f ux) y z).
+
+End ZRange.