diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-20 12:41:10 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-20 12:41:10 -0400 |
| commit | b325bd95a14ff4c1df4f8b045da76d80e59bcefa (patch) | |
| tree | f0ca10b0cf87b31025db0968507c3c5d3e9d174a /src/Util/ZRange.v | |
| parent | a42c33268b58cbcc60aaee7ef3ab8a4a801a8f42 (diff) | |
Add is_bounded_by_None_repeat_In_iff
Diffstat (limited to 'src/Util/ZRange.v')
| -rw-r--r-- | src/Util/ZRange.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v index b6381f421..2cbd309f0 100644 --- a/src/Util/ZRange.v +++ b/src/Util/ZRange.v @@ -41,8 +41,20 @@ Section with_bitwidth. Definition is_bounded_by {n} : Tuple.tuple zrange n -> Tuple.tuple Z n -> Prop := Tuple.fieldwise is_bounded_by'. + + Lemma is_bounded_by_repeat_In_iff {n} vs bound + : is_bounded_by (Tuple.repeat bound n) vs <-> (forall x, List.In x (Tuple.to_list _ vs) -> is_bounded_by' bound x). + Proof. apply fieldwise_In_to_list_repeat_l_iff. Qed. End with_bitwidth. +Lemma is_bounded_by_None_repeat_In_iff {n} vs l u + : is_bounded_by None (Tuple.repeat {| lower := l ; upper := u |} n) vs + <-> (forall x, List.In x (Tuple.to_list _ vs) -> l <= x <= u). +Proof. + rewrite is_bounded_by_repeat_In_iff; unfold is_bounded_by'; simpl. + split; intro H; intros; repeat split; apply H; assumption. +Qed. + Definition is_tighter_than_bool (x y : zrange) : bool := ((lower y <=? lower x) && (upper x <=? upper y))%bool%Z. |