blob: 7d9b24c409220bc9060af5404355be7055af5f60 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
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.
|
