diff options
author | Jason Gross <jgross@mit.edu> | 2018-02-10 16:17:16 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-02-10 16:17:16 -0500 |
commit | 051ccf4d0666e195c0022c1e5948892bbc7aeca0 (patch) | |
tree | b87502c04b2d39bb302ed943ea7c24ee2b66d899 /src/Util/ZRange/Operations.v | |
parent | d62ffb1a68a76cc33c502e1a8351f14104bc7ee2 (diff) |
Split off ZRange lemmas
Diffstat (limited to 'src/Util/ZRange/Operations.v')
-rw-r--r-- | src/Util/ZRange/Operations.v | 30 |
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. |