1 files changed, 23 insertions, 7 deletions
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
index 7d9b24c40..c73b991e8 100644
--- a/src/Util/ZRange/Operations.v
+++ b/src/Util/ZRange/Operations.v
@@ -7,21 +7,38 @@ Module ZRange.
 
   Local Notation eta v := r[ lower v ~> upper v ].
 
+  Definition flip (v : zrange) : zrange
+    := r[ upper v ~> lower v ].
+
+  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 normalize (v : zrange) : zrange
-    := r[ Z.min (lower v) (upper v) ~> Z.max (lower v) (upper v) ].
+    := r[ Z.min (lower v) (upper v) ~> Z.max (upper v) (lower v) ].
+
+  Definition normalize' (v : zrange) : zrange
+    := union v (flip v).
+
+  Lemma normalize'_eq : normalize = normalize'. Proof. reflexivity. Defined.
 
   Definition abs (v : zrange) : zrange
     := let (l, u) := eta v in
        r[ 0 ~> Z.max (Z.abs l) (Z.abs u) ].
 
+  Definition map (f : Z -> Z) (v : zrange) : zrange
+    := let (l, u) := eta v in
+       r[ f l ~> f 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) ].
+       r[ Z.min (f l) (f u) ~> Z.max (f u) (f l) ].
 
-  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 two_corners' (f : Z -> Z) (v : zrange) : zrange
+    := normalize' (map f v).
+
+  Lemma two_corners'_eq : two_corners = two_corners'. Proof. reflexivity. Defined.
 
   Definition four_corners (f : Z -> Z -> Z) (x y : zrange) : zrange
     := let (lx, ux) := eta x in
@@ -32,5 +49,4 @@ Module ZRange.
     := let (lx, ux) := eta x in
        union (four_corners (f lx) y z)
              (four_corners (f ux) y z).
-
 End ZRange.