diff options
author | Jason Gross <jagro@google.com> | 2018-06-26 15:10:24 -0400 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2018-06-26 15:10:24 -0400 |
commit | 78656baa06ed1daeb7ba90c2d429228516dc8475 (patch) | |
tree | dd8423b57e107e8fb2efcb2d22438edc723845f4 /src/Util/ZRange/Operations.v | |
parent | 19fd81bfae1d8fad0b31a8415e4259c11ab80c0a (diff) |
Add a couple of zrange lemmas
Diffstat (limited to 'src/Util/ZRange/Operations.v')
-rw-r--r-- | src/Util/ZRange/Operations.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index 881a28a31..d17785f77 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -78,6 +78,12 @@ Module ZRange. => let (lx, ux) := x in let (ly, uy) := y in {| lower := Z.min 0 (Z.min lx ly) ; upper := Z.max 0 (Z.min ux uy) |}). + Definition lor_bounds : zrange -> zrange -> zrange + := extremization_bounds + (fun x y + => let (lx, ux) := x in + let (ly, uy) := y in + {| lower := Z.max lx ly ; upper := upper_lor_land_bounds ux uy |}). Definition split_bounds (r : zrange) (split_at : BinInt.Z) : zrange * zrange := if upper r <? split_at @@ -87,4 +93,9 @@ Module ZRange. {| lower := lower r / split_at; upper := (upper r / split_at) |} ) else ( {| lower := 0; upper := split_at - 1 |}, {| lower := lower r / split_at; upper := (upper r / split_at) |} ). + + Definition good (r : zrange) : Prop + := lower r <= upper r. + Definition goodb (r : zrange) : bool + := (lower r <=? upper r)%Z. End ZRange. |