diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-08 14:06:23 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-08 14:06:23 -0400 |
| commit | fc29d571cbb25ffd0ba448eda007340e2f4ae87c (patch) | |
| tree | b0f974ccf3fa14549124a211db3f3aff564c7d84 /src/Util/ZUtil.v | |
| parent | 3c674d6d86483bf6e0647c5662b63581c3777011 (diff) | |
Add some le proper flip lemmas
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 91c350d9f..acdab1a06 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -278,6 +278,18 @@ Module Z. Proof. intros ???; apply Z.pow_le_mono_r; try reflexivity; try assumption. Qed. Lemma le_Proper_ge_le_flip_impl : Proper (Z.le ==> Z.ge ==> Basics.flip Basics.impl) Z.le. Proof. intros ???????; omega. Qed. + Lemma add_le_Proper_flip : Proper (Basics.flip Z.le ==> Basics.flip Z.le ==> Basics.flip Z.le) Z.add. + Proof. unfold Basics.flip; repeat (omega || intro). Qed. + Lemma sub_le_ge_Proper_flip : Proper (Basics.flip Z.le ==> Basics.flip Z.ge ==> Basics.flip Z.le) Z.sub. + Proof. unfold Basics.flip; repeat (omega || intro). Qed. + Lemma sub_le_eq_Proper_flip : Proper (Basics.flip Z.le ==> Logic.eq ==> Basics.flip Z.le) Z.sub. + Proof. unfold Basics.flip; repeat (omega || intro). Qed. + Lemma log2_up_le_Proper_flip : Proper (Basics.flip Z.le ==> Basics.flip Z.le) Z.log2_up. + Proof. intros ???; apply Z.log2_up_le_mono; assumption. Qed. + Lemma log2_le_Proper_flip : Proper (Basics.flip Z.le ==> Basics.flip Z.le) Z.log2. + Proof. intros ???; apply Z.log2_le_mono; assumption. Qed. + Lemma pow_Zpos_le_Proper_flip x : Proper (Basics.flip Z.le ==> Basics.flip Z.le) (Z.pow (Z.pos x)). + Proof. intros ???; apply Z.pow_le_mono_r; try reflexivity; try assumption. Qed. End proper. Definition pow2_mod n i := (n &' (Z.ones i)). |