diff options
| -rw-r--r-- | src/Util/NumTheoryUtil.v | 16 | ||||
| -rw-r--r-- | src/Util/ZUtil.v | 35 |
2 files changed, 43 insertions, 8 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. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 3ebbbece1..1c3efbdac 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -154,6 +154,39 @@ Proof. pose proof (prime_ge_2 p prime_p); omega. Qed. +Lemma mul_div_eq : (forall a m, m > 0 -> m * (a / m) = (a - a mod m))%Z. +Proof. + intros. + rewrite (Z_div_mod_eq a m) at 2 by auto. + ring. +Qed. + Ltac prime_bound := match goal with | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega -end.
\ No newline at end of file +end. + +Lemma Zlt_minus_lt_0 : forall n m, m < n -> 0 < n - m. +Proof. + intros; omega. +Qed. + +(* prove that known nonnegative numbers are nonnegative *) +Ltac zero_bounds' := + repeat match goal with + | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg + | [ |- 0 <= _ - _] => apply Zle_minus_le_0 + | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg + | [ |- 0 <= _ / _] => apply Z.div_pos + | [ |- 0 < _ + _] => apply Z.add_pos_nonneg + (* TODO : this apply is not good: it can make a true goal false. Actually, + * we would want this tactic to explore two branches: + * - apply Z.add_pos_nonneg and continue + * - apply Z.add_nonneg_pos and continue + * Keep whichever one solves all subgoals. If neither does, don't apply. *) + + | [ |- 0 < _ - _] => apply Zlt_minus_lt_0 + | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split + | [ |- 0 < _ / _] => apply Z.div_str_pos + end; try omega; try prime_bound; auto. + +Ltac zero_bounds := try omega; try prime_bound; zero_bounds'. |