diff options
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index d06477d3c..1758f1496 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -19,7 +19,7 @@ Hint Extern 1 => lia : lia. Hint Extern 1 => lra : lra. Hint Extern 1 => nia : nia. Hint Extern 1 => omega : omega. -Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg Z.div_lt_upper_bound : zarith. +Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg Z.div_lt_upper_bound Z.div_pos : zarith. Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) (fun a b pf => proj1 (Z.pow_gt_1 a b pf)) : zarith. Ltac zutil_arith := solve [ omega | lia | auto with nocore ]. @@ -324,15 +324,27 @@ 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. + 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. + 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. + 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. + 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. - Hint Rewrite mod_add_l using zutil_arith : zsimplify. 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. 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. - Hint Rewrite mod_add' mod_add_l' using zutil_arith : zsimplify. Lemma pos_pow_nat_pos : forall x n, Z.pos x ^ Z.of_nat n > 0. |