diff options
Diffstat (limited to 'src/Util/ZUtil/Morphisms.v')
| -rw-r--r-- | src/Util/ZUtil/Morphisms.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Morphisms.v b/src/Util/ZUtil/Morphisms.v index 285fa5261..d58b89c91 100644 --- a/src/Util/ZUtil/Morphisms.v +++ b/src/Util/ZUtil/Morphisms.v @@ -1,5 +1,6 @@ (** * [Proper] morphisms for ℤ constants *) Require Import Coq.omega.Omega. +Require Import Coq.micromega.Lia. Require Import Coq.ZArith.ZArith. Require Import Coq.Classes.Morphisms. Require Import Coq.Classes.RelationPairs. @@ -11,14 +12,20 @@ Module Z. instances; making them instances would slow typeclass search unacceptably. In files where we use these, we add them with [Local Existing Instances]. *) + Lemma succ_le_Proper : Proper (Z.le ==> Z.le) Z.succ. + Proof. repeat (omega || intro). Qed. Lemma add_le_Proper : Proper (Z.le ==> Z.le ==> Z.le) Z.add. Proof. repeat (omega || intro). Qed. + Lemma add_le_Proper' x : Proper (Z.le ==> Z.le) (Z.add x). + Proof. repeat (omega || intro). Qed. Lemma sub_le_ge_Proper : Proper (Z.le ==> Z.ge ==> Z.le) Z.sub. Proof. repeat (omega || intro). Qed. Lemma sub_le_flip_le_Proper : Proper (Z.le ==> Basics.flip Z.le ==> Z.le) Z.sub. Proof. unfold Basics.flip; repeat (omega || intro). Qed. Lemma sub_le_eq_Proper : Proper (Z.le ==> Logic.eq ==> Z.le) Z.sub. Proof. repeat (omega || intro). Qed. + Lemma mul_Zpos_le_Proper p : Proper (Z.le ==> Z.le) (Z.mul (Z.pos p)). + Proof. repeat (nia || intro). Qed. Lemma log2_up_le_Proper : Proper (Z.le ==> Z.le) Z.log2_up. Proof. intros ???; apply Z.log2_up_le_mono; assumption. Qed. Lemma log2_le_Proper : Proper (Z.le ==> Z.le) Z.log2. |