diff options
Diffstat (limited to 'src/Util/ZUtil/Modulo.v')
| -rw-r--r-- | src/Util/ZUtil/Modulo.v | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v index 511898b48..4e14907e8 100644 --- a/src/Util/ZUtil/Modulo.v +++ b/src/Util/ZUtil/Modulo.v @@ -14,38 +14,38 @@ Module Z. Hint Resolve elim_mod : zarith. Lemma mod_add_full : forall a b c, (a + b * c) mod c = a mod c. - Proof. intros; destruct (Z_zerop c); try subst; autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c; destruct (Z_zerop c); try subst; autorewrite with zsimplify; reflexivity. Qed. Hint Rewrite mod_add_full : zsimplify. Lemma mod_add_l_full : forall a b c, (a * b + c) mod b = c mod b. - Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. Hint Rewrite mod_add_l_full : zsimplify. Lemma mod_add'_full : forall a b c, (a + b * c) mod b = a mod b. - Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. Lemma mod_add_l'_full : forall a b c, (a * b + c) mod a = c mod a. - Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. Hint Rewrite mod_add'_full mod_add_l'_full : zsimplify. Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b. - Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c H; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b. - Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c H; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a. - Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. + Proof. intros a b c H; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. Lemma add_pow_mod_l : forall a b c, a <> 0 -> 0 < b -> ((a ^ b) + c) mod a = c mod a. Proof. - intros; replace b with (b - 1 + 1) by ring; + intros a b c H H0; replace b with (b - 1 + 1) by ring; rewrite Z.pow_add_r, Z.pow_1_r by omega; auto using Z.mod_add_l. Qed. Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 -> a ^ x mod m = 0. Proof. - intros. + intros a x m H H0 H1. replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega). induction (Z.to_nat x). { simpl in *; omega. @@ -70,8 +70,8 @@ Module Z. Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) -> a ^ b mod m = (a mod m) ^ b mod m. Proof. - intros; rewrite <- (Z2Nat.id b) by auto. - induction (Z.to_nat b); auto. + intros a m b H H0; rewrite <- (Z2Nat.id b) by auto. + induction (Z.to_nat b) as [|n IHn]; auto. rewrite Nat2Z.inj_succ. do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg. rewrite Z.mul_mod by auto. @@ -90,7 +90,7 @@ Module Z. Lemma mul_div_eq_full : forall a m, m <> 0 -> m * (a / m) = (a - a mod m). Proof. - intros. rewrite (Z_div_mod_eq_full a m) at 2 by auto. ring. + intros a m H. rewrite (Z_div_mod_eq_full a m) at 2 by auto. ring. Qed. Hint Rewrite mul_div_eq_full using zutil_arith : zdiv_to_mod. @@ -126,14 +126,14 @@ Module Z. Lemma mul_div_eq : forall a m, m > 0 -> m * (a / m) = (a - a mod m). Proof. - intros. + intros a m H. rewrite (Z_div_mod_eq a m) at 2 by auto. ring. Qed. Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z. Proof. - intros. + intros a m H. rewrite (Z_div_mod_eq a m) at 2 by auto. ring. Qed. |