From c92678ddbbbc0c2bcfe8ee211cbdf1908e6beeab Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Mon, 15 Feb 2016 14:31:06 -0500 Subject: tweaks to util files, including automation for proving positivity/nonnegativity in Z --- src/Util/NumTheoryUtil.v | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'src/Util/NumTheoryUtil.v') 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. -- cgit v1.2.3