diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-03 13:19:32 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-03 13:19:32 -0500 |
| commit | 650a343b64072d2972c2c3d360e112e2ba9a9811 (patch) | |
| tree | 8ee2e382be7d6fa98efe7d447b18d15e1096fd9c /src/Util/ZUtil.v | |
| parent | c7548a11ed6083a188f68e18d10f3c059120e585 (diff) | |
Add log2_up_le_full
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index ec9d6f78a..950809b2c 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2111,6 +2111,13 @@ Module Z. Qed. Hint Rewrite log2_pred_pow2_full : zsimplify. + Lemma log2_up_le_full a : a <= 2^Z.log2_up a. + Proof. + destruct (Z_dec 1 a) as [ [ ? | ? ] | ? ]; + first [ apply Z.log2_up_spec; assumption + | rewrite Z.log2_up_eqn0 by omega; simpl; omega ]. + Qed. + Lemma ones_lt_pow2 x y : 0 <= x <= y -> Z.ones x < 2^y. Proof. rewrite Z.ones_equiv, Z.lt_pred_le. |