From b1bdefa45c0fa9786a8f916981a67ac5a4961eb0 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 12 Mar 2019 13:06:56 -0400 Subject: Move some lemmas to appropriate places --- src/Util/ZUtil/Divide.v | 7 +++++++ src/Util/ZUtil/Pow.v | 24 ++++++++++++++++++++++++ 2 files changed, 31 insertions(+) (limited to 'src/Util') 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. -- cgit v1.2.3