diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-20 22:48:28 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-20 22:48:28 -0400 |
| commit | 68d5af36ba4dad08064f985a03976e697032b1a2 (patch) | |
| tree | dfcc5d7c059cfaa02f53ef0e35e034ceb2c66b8d /src/Util/ZRange.v | |
| parent | 5575668a47e9a83b1ead069630409d46c911aaea (diff) | |
Add is_bounded_by_None_repeat_In_iff_lt
Diffstat (limited to 'src/Util/ZRange.v')
| -rw-r--r-- | src/Util/ZRange.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v index 2cbd309f0..daf2ed8cf 100644 --- a/src/Util/ZRange.v +++ b/src/Util/ZRange.v @@ -55,6 +55,14 @@ Proof. split; intro H; intros; repeat split; apply H; assumption. Qed. +Lemma is_bounded_by_None_repeat_In_iff_lt {n} vs l u + : is_bounded_by None (Tuple.repeat {| lower := l ; upper := u - 1 |} n) vs + <-> (forall x, List.In x (Tuple.to_list _ vs) -> l <= x < u). +Proof. + rewrite is_bounded_by_None_repeat_In_iff. + split; intro H; (repeat let x := fresh in intro x; specialize (H x)); omega. +Qed. + Definition is_tighter_than_bool (x y : zrange) : bool := ((lower y <=? lower x) && (upper x <=? upper y))%bool%Z. |