tweaks to util files, including automation for proving positivity/nonnegativity in Z

1 files changed, 9 insertions, 7 deletions

diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index 157cdbdfb..eee651bc9 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -83,7 +83,7 @@ Lemma fermat_little: forall a (a_nonzero : a mod p <> 0),
 Proof.
   intros.
   assert (rel_prime a p). {
-    apply rel_prime_mod_rev; prime_bound.
+    apply rel_prime_mod_rev; try prime_bound.
     assert (0 < p) as p_pos by prime_bound.
     apply rel_prime_le_prime; auto; pose proof (Z.mod_pos_bound a p p_pos).
     omega.
@@ -106,7 +106,7 @@ Proof.
 Qed.
 
 Lemma euler_criterion_square_reverse : forall a (a_nonzero : a mod p <> 0),
-  (exists b, b * b mod p = a mod p) -> (a ^ x mod p = 1).
+  (exists b, b * b mod p = a) -> (a ^ x mod p = 1).
 Proof.
   intros ? ? a_square.
   destruct a_square as [b a_square].
@@ -114,11 +114,13 @@ Proof.
     intuition.
     rewrite <- Z.pow_2_r in a_square.
     rewrite mod_exp_0 in a_square by prime_bound.
+    rewrite <- a_square in a_nonzero.
     auto.
   }
   pose proof (squared_fermat_little b b_nonzero).
   rewrite mod_pow in * by prime_bound.
-  rewrite <- a_square; auto.
+  rewrite <- a_square.
+  rewrite Z.mod_mod; prime_bound.
 Qed.
 
 Lemma exists_primitive_root_power :
@@ -154,7 +156,7 @@ Ltac ereplace x := match type of x with ?t =>
   let e := fresh "e" in evar (e:t); replace x with e; subst e end.
 
 Lemma euler_criterion_square : forall a (a_range : 1 <= a <= p - 1)
-  (pow_a_x : a ^ x mod p = 1), exists b, b * b mod p = a mod p.
+  (pow_a_x : a ^ x mod p = 1), exists b, b * b mod p = a.
 Proof.
   intros.
   destruct (exists_primitive_root_power) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto.
@@ -184,13 +186,14 @@ Proof.
     try (apply prime_pred_divide2 || prime_bound); auto.
   rewrite <- Zdivide_Zdiv_eq by (auto || omega).
   rewrite Zplus_diag_eq_mult_2.
+  replace (a mod p) with a in pow_y_j by (symmetry; apply Z.mod_small; omega).
   rewrite Z_div_mult by omega; auto.
   apply divide2_even_iff.
   apply prime_pred_even.
 Qed.
 
 Lemma euler_criterion : forall a (a_range : 1 <= a <= p - 1),
-  (a ^ x mod p = 1) <-> exists b, b * b mod p = a mod p.
+  (a ^ x mod p = 1) <-> exists b, b * b mod p = a.
 Proof.
   intros; split. {
     exact (euler_criterion_square _ a_range).
@@ -202,7 +205,7 @@ Proof.
 Qed.
 
 Lemma euler_criterion_nonsquare : forall a (a_range : 1 <= a <= p - 1),
-  (a ^ x mod p <> 1) <-> ~ (exists b, b * b mod p = a mod p).
+  (a ^ x mod p <> 1) <-> ~ (exists b, b * b mod p = a).
 Proof.
   split; intros A B; apply (euler_criterion a a_range) in B; congruence.
 Qed.
@@ -276,7 +279,6 @@ Lemma minus1_square_1mod4 : forall (p : Z) (prime_p : prime p),
   (p mod 4 = 1)%Z -> exists b : Z, (b * b mod p = p - 1)%Z.
 Proof.
   intros.
-  replace (p - 1) with ((p - 1) mod p) by (apply Zmod_small; split; prime_bound).
   assert (p <> 2) as neq_p_2 by (apply prime_1mod4_neq2; auto).
   apply (euler_criterion (p / 2) p prime_p).
   + auto.