diff options
author | Jason Gross <jgross@mit.edu> | 2017-05-12 23:41:12 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-05-12 23:41:12 -0400 |
commit | e86587b3f0590e3cc4aa005bf4577a9f84cc1056 (patch) | |
tree | 91a9e28e64f1227f9093e075b374af6aa81825d1 /src | |
parent | c78dc3e16d9e41b7dba5d55ca019f03f697b31e5 (diff) |
Split off Proper ZUtil lemmas
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/ZUtil.v | 41 | ||||
-rw-r--r-- | src/Util/ZUtil/Morphisms.v | 45 |
2 files changed, 46 insertions, 40 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 54ab65115..7dec68884 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -13,6 +13,7 @@ Require Import Coq.Lists.List. Require Export Crypto.Util.FixCoqMistakes. Require Export Crypto.Util.ZUtil.Notations. Require Export Crypto.Util.ZUtil.Definitions. +Require Export Crypto.Util.ZUtil.Morphisms. Import Nat. Local Open Scope Z. @@ -241,46 +242,6 @@ Hint Rewrite Bool.andb_true_r Bool.andb_false_r Bool.orb_true_r Bool.orb_false_r Bool.andb_true_l Bool.andb_false_l Bool.orb_true_l Bool.orb_false_l : Ztestbit. Module Z. - Section proper. - (** We prove a bunch of [Proper] lemmas, but do not make them - instances; making them instances would slow typeclass search - unacceptably. In files where we use these, we add them with - [Local Existing Instances]. *) - Lemma add_le_Proper : Proper (Z.le ==> Z.le ==> Z.le) Z.add. - 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 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. - Proof. intros ???; apply Z.log2_le_mono; assumption. Qed. - Lemma pow_Zpos_le_Proper x : Proper (Z.le ==> Z.le) (Z.pow (Z.pos x)). - Proof. intros ???; apply Z.pow_le_mono_r; try reflexivity; try assumption. Qed. - Lemma lt_le_flip_Proper_flip_impl - : Proper (Z.le ==> Basics.flip Z.le ==> Basics.flip Basics.impl) Z.lt. - Proof. unfold Basics.flip; repeat (omega || intro). 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_flip_le_le_Proper_flip : Proper (Basics.flip Z.le ==> Z.le ==> 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. - Ltac peel_le_step := match goal with | [ |- ?x + _ <= ?x + _ ] diff --git a/src/Util/ZUtil/Morphisms.v b/src/Util/ZUtil/Morphisms.v new file mode 100644 index 000000000..bb708ab8a --- /dev/null +++ b/src/Util/ZUtil/Morphisms.v @@ -0,0 +1,45 @@ +(** * [Proper] morphisms for ℤ constants *) +Require Import Coq.omega.Omega. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Classes.Morphisms. +Local Open Scope Z_scope. + +Module Z. + (** We prove a bunch of [Proper] lemmas, but do not make them + instances; making them instances would slow typeclass search + unacceptably. In files where we use these, we add them with + [Local Existing Instances]. *) + Lemma add_le_Proper : Proper (Z.le ==> Z.le ==> Z.le) Z.add. + 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 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. + Proof. intros ???; apply Z.log2_le_mono; assumption. Qed. + Lemma pow_Zpos_le_Proper x : Proper (Z.le ==> Z.le) (Z.pow (Z.pos x)). + Proof. intros ???; apply Z.pow_le_mono_r; try reflexivity; try assumption. Qed. + Lemma lt_le_flip_Proper_flip_impl + : Proper (Z.le ==> Basics.flip Z.le ==> Basics.flip Basics.impl) Z.lt. + Proof. unfold Basics.flip; repeat (omega || intro). 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_flip_le_le_Proper_flip : Proper (Basics.flip Z.le ==> Z.le ==> 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 Z. |