diff options
| -rw-r--r-- | src/Galois/GaloisTheory.v | 87 | ||||
| -rw-r--r-- | src/Util/NumTheoryUtil.v | 37 |
2 files changed, 117 insertions, 7 deletions
diff --git a/src/Galois/GaloisTheory.v b/src/Galois/GaloisTheory.v index bef7fbe03..6bf0621eb 100644 --- a/src/Galois/GaloisTheory.v +++ b/src/Galois/GaloisTheory.v @@ -298,5 +298,90 @@ Module GaloisTheory (M: Modulus). constructor; auto. Qed. -End GaloisTheory. + Ltac modulus_bound := + pose proof (prime_ge_2 (primeToZ modulus) (proj2_sig modulus)); omega. + Lemma GFexp_Zpow : forall (a : GF) (a_nonzero : a <> 0) + (k : Z) (k_nonneg : (0 <= k)%Z), + a ^ (Z.to_N k) = ((GFToZ a) ^ k)%Z. + Proof. + intros a a_nonzero. + apply natlike_ind; [ galois; symmetry; apply Z.mod_small; modulus_bound | ]. + intros k k_nonneg IHk. + rewrite Z2N.inj_succ by auto. + rewrite GFexp_pred by (auto; apply N.neq_succ_0). + rewrite N.pred_succ. + rewrite IHk. + rewrite Z.pow_succ_r by auto. + galois. + Qed. + + Lemma GFToZ_inject : forall x, GFToZ (inject x) = (x mod primeToZ modulus)%Z. + Proof. + intros; unfold GFToZ, proj1_sig, inject; reflexivity. + Qed. + + Lemma GF_Zmod : forall x, ((GFToZ x) mod primeToZ modulus = GFToZ x)%Z. + Proof. + intros. + pose proof (inject_eq x) as inject_eq_x. + apply gf_eq in inject_eq_x. + rewrite <- inject_eq_x. + rewrite inject_mod_eq. + rewrite GFToZ_inject. + apply Z.mod_mod. + modulus_bound. + Qed. + + Lemma square_Zmod_GF : forall (a : GF) (a_nonzero : a <> 0), + (exists b : Z, ((b * b) mod modulus)%Z = (a mod modulus)%Z) <-> (exists b, b * b = a). + Proof. + split; intros A; destruct A as [b b_id]. { + exists (inject b). + galois. + } { + exists (GFToZ b). + rewrite GF_Zmod. + rewrite <- b_id. + rewrite <- (inject_eq b) at 3 4. + rewrite <- inject_distr_mul. + rewrite GFToZ_inject. + auto. + } + Qed. + + Lemma GFexp_0 : forall e : N, e <> 0%N -> 0 ^ e = 0. + Proof. + Admitted. + + Lemma nonzero_Zmod_GF : forall a, + (inject a <> 0) <-> (a mod primeToZ modulus <> 0)%Z. + Proof. + split; intros A B; unfold not in A. { + rewrite inject_mod_eq in A. + rewrite B in A. + apply A. + apply gf_eq. + rewrite GFToZ_inject. + rewrite Z.mod_0_l by modulus_bound. + auto. + } { + apply A. + apply gf_eq in B. + rewrite GFToZ_inject in B. + auto. + } + Qed. + + Lemma nonzero_range : forall (a : GF), (a <> 0) -> (1 <= a <= primeToZ modulus - 1)%Z. + Proof. + intros a a_nonzero. + assert (a mod primeToZ modulus <> 0)%Z by (apply nonzero_Zmod_GF; rewrite inject_eq; auto). + replace (GFToZ a) with (a mod primeToZ modulus)%Z by (symmetry; apply (proj2_sig a)). + assert (0 < primeToZ modulus)%Z as modulus_pos by + (pose proof (prime_ge_2 (primeToZ modulus) (proj2_sig modulus)); omega). + pose proof (Z.mod_pos_bound a (primeToZ modulus) modulus_pos). + omega. + Qed. + +End GaloisTheory.
\ No newline at end of file diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index c1dc9c14e..157cdbdfb 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -105,7 +105,7 @@ Proof. apply fermat_little; auto. Qed. -Lemma euler_criterion_reverse : forall a (a_nonzero : a mod p <> 0), +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). Proof. intros ? ? a_square. @@ -153,8 +153,8 @@ Qed. 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 : forall a (a_range : 1 <= a <= p - 1) - (pow_a_x : a ^ x mod p = 1), exists b : Z, b * b mod p = a mod p. +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. Proof. intros. destruct (exists_primitive_root_power) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto. @@ -189,6 +189,24 @@ Proof. 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. +Proof. + intros; split. { + exact (euler_criterion_square _ a_range). + } { + apply euler_criterion_square_reverse; auto. + replace (a mod p) with a by (symmetry; apply Zmod_small; omega). + omega. + } +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). +Proof. + split; intros A B; apply (euler_criterion a a_range) in B; congruence. +Qed. + End EulerCriterion. Lemma divide2_1mod4 : forall x (x_1mod4 : x mod 4 = 1) (x_nonneg : 0 <= x), (2 | x / 2). @@ -245,6 +263,15 @@ Proof. omega. Qed. +Lemma div2_p_1mod4 : forall (p : Z) (prime_p : prime p) (neq_p_2: p <> 2), + (p / 2) * 2 + 1 = p. +Proof. + intros. + destruct (prime_odd_or_2 p prime_p); intuition. + rewrite <- Zdiv2_div. + pose proof (Zdiv2_odd_eqn p); break_if; congruence || omega. +Qed. + 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. @@ -253,9 +280,7 @@ Proof. assert (p <> 2) as neq_p_2 by (apply prime_1mod4_neq2; auto). apply (euler_criterion (p / 2) p prime_p). + auto. - + destruct (prime_odd_or_2 p prime_p); intuition. - rewrite <- Zdiv2_div. - pose proof (Zdiv2_odd_eqn p); break_if; congruence || omega. + + apply div2_p_1mod4; auto. + prime_bound. + apply minus1_even_pow; [apply divide2_1mod4 | | apply Z_div_pos]; prime_bound. Qed. |