diff options
author | Jason Gross <jgross@mit.edu> | 2018-02-10 15:25:59 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-02-10 15:25:59 -0500 |
commit | b0dca8dbd9bc959c5ccb5355e419b03714483668 (patch) | |
tree | 85f957ef811d94d8bcdca9683d3dec0aeab38da8 | |
parent | 5157dd8d86dc6d5cd3eb2430f5e67b5601f2ed76 (diff) |
Add some ZRange operations
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Util/ZRange/Operations.v | 36 |
2 files changed, 37 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 743a0a3a3..fa0dcff31 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6543,6 +6543,7 @@ src/Util/Tactics/UnfoldArg.v src/Util/Tactics/UnifyAbstractReflexivity.v src/Util/Tactics/UniquePose.v src/Util/Tactics/VM.v +src/Util/ZRange/Operations.v src/Util/ZUtil/AddGetCarry.v src/Util/ZUtil/CPS.v src/Util/ZUtil/Definitions.v 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. |