aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
authorGravatar jadep <jadep@mit.edu>2019-03-12 13:06:56 -0400
committerGravatar jadephilipoom <jade.philipoom@gmail.com>2019-03-25 06:13:45 -0400
commitb1bdefa45c0fa9786a8f916981a67ac5a4961eb0 (patch)
tree3258749dd759d170d1133458afe7fce11ccfa5b7 /src/Util
parent684d356bcb81ca36314cd7864c62a1d97af4ea99 (diff)
Move some lemmas to appropriate places
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/ZUtil/Divide.v7
-rw-r--r--src/Util/ZUtil/Pow.v24
2 files changed, 31 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Divide.v b/src/Util/ZUtil/Divide.v
index 8609db5ad..b49530194 100644
--- a/src/Util/ZUtil/Divide.v
+++ b/src/Util/ZUtil/Divide.v
@@ -33,4 +33,11 @@ Module Z.
apply Zmod_divide; omega || auto.
}
Qed.
+
+ Lemma divide_pow_le b n m : 0 <= n <= m -> (b ^ n | b ^ m).
+ Proof.
+ intros. replace m with (n + (m - n)) by ring.
+ rewrite Z.pow_add_r by lia.
+ apply Z.divide_factor_l.
+ Qed.
End Z.
diff --git a/src/Util/ZUtil/Pow.v b/src/Util/ZUtil/Pow.v
index 06ce2187b..f07709614 100644
--- a/src/Util/ZUtil/Pow.v
+++ b/src/Util/ZUtil/Pow.v
@@ -41,4 +41,28 @@ Module Z.
Lemma two_p_two_eq_four : 2^(2) = 4.
Proof. reflexivity. Qed.
Hint Rewrite <- two_p_two_eq_four : push_Zpow.
+
+ Lemma pow_pos_le a b : 0 < a -> 0 < b -> a <= a ^ b.
+ Proof.
+ intros; transitivity (a ^ 1).
+ { rewrite Z.pow_1_r; reflexivity. }
+ { apply Z.pow_le_mono; auto with zarith. }
+ Qed.
+ Hint Resolve pow_pos_le : zarith.
+
+ Lemma pow_pos_lt a b : 1 < a -> 1 < b -> a < a ^ b.
+ Proof.
+ intros; eapply Z.le_lt_trans with (m:=a ^ 1).
+ { rewrite Z.pow_1_r; reflexivity. }
+ { apply Z.pow_lt_mono_r; auto with zarith. }
+ Qed.
+ Hint Resolve pow_pos_lt : zarith.
+
+ Lemma pow_div_base a b : a <> 0 -> 0 < b -> a ^ b / a = a ^ (b - 1).
+ Proof. intros; rewrite Z.pow_sub_r, Z.pow_1_r; lia. Qed.
+ Hint Rewrite pow_div_base using zutil_arith : pull_Zpow.
+
+ Lemma pow_mul_base a b : 0 <= b -> a * a ^ b = a ^ (b + 1).
+ Proof. intros; rewrite <-Z.pow_succ_r, <-Z.add_1_r by lia; reflexivity. Qed.
+ Hint Rewrite pow_mul_base using zutil_arith : pull_Zpow.
End Z.