diff options
-rw-r--r-- | src/Util/NatUtil.v | 8 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 11 |
2 files changed, 19 insertions, 0 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index afed2a231..256654df7 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,4 +1,7 @@ Require Import NPeano Omega. +Require Import Bedrock.Word. + +Local Open Scope nat_scope. Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1. Proof. @@ -54,3 +57,8 @@ Proof. rewrite <- nat_compare_lt; auto. } Qed. + +Lemma pow2_id : forall n, pow2 n = 2 ^ n. +Proof. + induction n; intros; simpl; auto. +Qed. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 1c3efbdac..ac1c47152 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -65,6 +65,17 @@ Proof. auto. Qed. +Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> + ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. +Proof. + intros; induction n; try reflexivity. + rewrite Nat2Z.inj_succ. + rewrite pow_succ_r by apply le_0_n. + rewrite Z.pow_succ_r by apply Zle_0_nat. + rewrite IHn. + rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg. +Qed. + Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 -> a ^ x mod m = 0. Proof. |