diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-02 00:01:35 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2017-06-05 18:47:35 -0400 |
commit | 7488682db4cf259e0bb0c886e13301c32a2eeaa2 (patch) | |
tree | 9baf80699c9f00b01d3180504d58351b6ecc0f33 /src/Util/ZUtil | |
parent | c4a0d1fdde22dbd2faaa1753e973ee9602076ee8 (diff) |
Don't rely on autogenerated names
This fixes all of the private-names warnings emitted by
compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus
the ones in coqprime, which I didn't touch).
Diffstat (limited to 'src/Util/ZUtil')
-rw-r--r-- | src/Util/ZUtil/Land.v | 2 | ||||
-rw-r--r-- | src/Util/ZUtil/Modulo.v | 28 | ||||
-rw-r--r-- | src/Util/ZUtil/Testbit.v | 8 |
3 files changed, 19 insertions, 19 deletions
diff --git a/src/Util/ZUtil/Land.v b/src/Util/ZUtil/Land.v index b3d3f3727..f46d541e9 100644 --- a/src/Util/ZUtil/Land.v +++ b/src/Util/ZUtil/Land.v @@ -5,7 +5,7 @@ Local Open Scope Z_scope. Module Z. Lemma land_same_r : forall a b, (a &' b) &' b = a &' b. Proof. - intros; apply Z.bits_inj'; intros. + intros a b; apply Z.bits_inj'; intros n H. rewrite !Z.land_spec. case_eq (Z.testbit b n); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; reflexivity. 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. diff --git a/src/Util/ZUtil/Testbit.v b/src/Util/ZUtil/Testbit.v index a315f7e4b..175d07b02 100644 --- a/src/Util/ZUtil/Testbit.v +++ b/src/Util/ZUtil/Testbit.v @@ -22,7 +22,7 @@ Module Z. then true else if Z_lt_dec m n then true else false. Proof. - intros. + intros n m. repeat (break_match || autorewrite with Ztestbit); try reflexivity; try omega. unfold Z.ones. rewrite <- Z.shiftr_opp_r, Z.shiftr_eq_0 by (simpl; omega); simpl. @@ -34,7 +34,7 @@ Module Z. Lemma testbit_pow2_mod : forall a n i, 0 <= n -> Z.testbit (Z.pow2_mod a n) i = if Z_lt_dec i n then Z.testbit a i else false. Proof. - cbv [Z.pow2_mod]; intros; destruct (Z_le_dec 0 i); + cbv [Z.pow2_mod]; intros a n i H; destruct (Z_le_dec 0 i); repeat match goal with | |- _ => rewrite Z.testbit_neg_r by omega | |- _ => break_innermost_match_step @@ -50,7 +50,7 @@ Module Z. then if Z_lt_dec i 0 then false else Z.testbit a i else if Z_lt_dec i n then Z.testbit a i else false. Proof. - intros; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ]. + intros a n i; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ]. unfold Z.pow2_mod. autorewrite with Ztestbit_full; repeat break_match; @@ -80,7 +80,7 @@ Module Z. Lemma testbit_add_shiftl_low : forall i, (0 <= i) -> forall a b n, (i < n) -> Z.testbit (a + Z.shiftl b n) i = Z.testbit a i. Proof. - intros. + intros i H a b n H0. erewrite Z.testbit_low; eauto. rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega. rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega). |