aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/ZUtil')
-rw-r--r--src/Util/ZUtil/Land.v2
-rw-r--r--src/Util/ZUtil/Modulo.v28
-rw-r--r--src/Util/ZUtil/Testbit.v8
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).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 12:57:38 +0000