From ef92beece3147f8af0764521e22cb7fc9a3f32a3 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 24 Feb 2018 10:17:35 -0500 Subject: coqprime in COQPATH (closes #269) --- src/Util/NumTheoryUtil.v | 64 ++++++++++++++++++++++++------------------------ 1 file changed, 32 insertions(+), 32 deletions(-) (limited to 'src/Util/NumTheoryUtil.v') diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index fd13896de..a59a6bbaa 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -5,38 +5,38 @@ Require Export Crypto.Util.FixCoqMistakes. Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z. -Require Coqprime.Euler Coqprime.Zp Coqprime.IGroup Coqprime.EGroup Coqprime.FGroup Coqprime.UList. +Require Coqprime.PrimalityTest.Euler Coqprime.PrimalityTest.Zp Coqprime.PrimalityTest.IGroup Coqprime.PrimalityTest.EGroup Coqprime.PrimalityTest.FGroup Coqprime.List.UList. -(* TODO: move somewhere else for lemmas about Coqprime? *) +(* TODO: move somewhere else for lemmas about Coqprime.PrimalityTest? *) Lemma in_ZPGroup_range (n : Z) (n_pos : 1 < n) (p : Z) : - List.In p (Coqprime.FGroup.s (Coqprime.Zp.ZPGroup n n_pos)) -> 1 <= p < n. + List.In p (Coqprime.PrimalityTest.FGroup.s (Coqprime.PrimalityTest.Zp.ZPGroup n n_pos)) -> 1 <= p < n. Proof. -unfold Coqprime.Zp.ZPGroup; simpl; intros Hin. -pose proof (Coqprime.IGroup.isupport_incl Z (Coqprime.Zp.pmult n) (Coqprime.Zp.mkZp n) 1 Z.eq_dec) as H. +unfold Coqprime.PrimalityTest.Zp.ZPGroup; simpl; intros Hin. +pose proof (Coqprime.PrimalityTest.IGroup.isupport_incl Z (Coqprime.PrimalityTest.Zp.pmult n) (Coqprime.PrimalityTest.Zp.mkZp n) 1 Z.eq_dec) as H. unfold List.incl in *. specialize (H p Hin). -apply Coqprime.Zp.in_mkZp in H; auto. +apply Coqprime.PrimalityTest.Zp.in_mkZp in H; auto. destruct (Z.eq_dec p 0); try subst. -apply Coqprime.IGroup.isupport_is_inv_true in Hin. -rewrite Coqprime.Zp.rel_prime_is_inv in Hin by auto. +apply Coqprime.PrimalityTest.IGroup.isupport_is_inv_true in Hin. +rewrite Coqprime.PrimalityTest.Zp.rel_prime_is_inv in Hin by auto. pose proof (not_rel_prime_0 n n_pos). destruct (rel_prime_dec 0 n) in Hin; try congruence. omega. Qed. Lemma generator_subgroup_is_group p (lt_1_p : 1 < p): forall y, - (List.In y (Coqprime.FGroup.s (Coqprime.Zp.ZPGroup p lt_1_p)) - /\ Coqprime.EGroup.e_order Z.eq_dec y (Coqprime.Zp.ZPGroup p lt_1_p) = Coqprime.FGroup.g_order (Coqprime.Zp.ZPGroup p lt_1_p)) - -> forall a, List.In a (Coqprime.FGroup.s (Coqprime.Zp.ZPGroup p lt_1_p)) -> - List.In a (Coqprime.EGroup.support Z.eq_dec y (Coqprime.Zp.ZPGroup p lt_1_p)). + (List.In y (Coqprime.PrimalityTest.FGroup.s (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p)) + /\ Coqprime.PrimalityTest.EGroup.e_order Z.eq_dec y (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p) = Coqprime.PrimalityTest.FGroup.g_order (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p)) + -> forall a, List.In a (Coqprime.PrimalityTest.FGroup.s (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p)) -> + List.In a (Coqprime.PrimalityTest.EGroup.support Z.eq_dec y (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p)). Proof. intros y H a H0. destruct H as [in_ZPGroup_y y_order]. - pose proof (Coqprime.EGroup.support_incl_G Z Z.eq_dec (Coqprime.Zp.pmult p) y (Coqprime.Zp.ZPGroup p lt_1_p) in_ZPGroup_y). + pose proof (Coqprime.PrimalityTest.EGroup.support_incl_G Z Z.eq_dec (Coqprime.PrimalityTest.Zp.pmult p) y (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p) in_ZPGroup_y). eapply Permutation.permutation_in; [|eauto]. apply Permutation.permutation_sym. - eapply Coqprime.UList.ulist_eq_permutation; try apply Coqprime.EGroup.support_ulist; eauto. - unfold Coqprime.EGroup.e_order, Coqprime.FGroup.g_order in y_order. + eapply Coqprime.List.UList.ulist_eq_permutation; try apply Coqprime.PrimalityTest.EGroup.support_ulist; eauto. + unfold Coqprime.PrimalityTest.EGroup.e_order, Coqprime.PrimalityTest.FGroup.g_order in y_order. apply Nat2Z.inj in y_order. auto. Qed. @@ -60,10 +60,10 @@ Proof using x_id. ring_simplify in x_id; apply Z.mul_cancel_l in x_id; omega. Qed. -Lemma mod_p_order : Coqprime.FGroup.g_order (Coqprime.Zp.ZPGroup p lt_1_p) = p - 1. +Lemma mod_p_order : Coqprime.PrimalityTest.FGroup.g_order (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p) = p - 1. Proof using Type. - intros; rewrite <- Coqprime.Zp.phi_is_order. - apply Coqprime.Euler.prime_phi_n_minus_1; auto. + intros; rewrite <- Coqprime.PrimalityTest.Zp.phi_is_order. + apply Coqprime.PrimalityTest.Euler.prime_phi_n_minus_1; auto. Qed. Lemma p_odd : Z.odd p = true. @@ -90,10 +90,10 @@ Proof using prime_p. apply rel_prime_le_prime; auto; pose proof (Z.mod_pos_bound a p p_pos). omega. } - rewrite (Coqprime.Zp.Zpower_mod_is_gpow _ _ _ lt_1_p) by (auto || prime_bound). + rewrite (Coqprime.PrimalityTest.Zp.Zpower_mod_is_gpow _ _ _ lt_1_p) by (auto || prime_bound). rewrite <- mod_p_order. - apply Coqprime.EGroup.fermat_gen; try apply Z.eq_dec. - apply Coqprime.Zp.in_mod_ZPGroup; auto. + apply Coqprime.PrimalityTest.EGroup.fermat_gen; try apply Z.eq_dec. + apply Coqprime.PrimalityTest.Zp.in_mod_ZPGroup; auto. Qed. Lemma fermat_inv : forall a, a mod p <> 0 -> ((a^(p-2) mod p) * a) mod p = 1. @@ -137,30 +137,30 @@ Proof using Type*. Qed. Lemma exists_primitive_root_power : - (exists y, List.In y (Coqprime.FGroup.s (Coqprime.Zp.ZPGroup p lt_1_p)) - /\ Coqprime.EGroup.e_order Z.eq_dec y (Coqprime.Zp.ZPGroup p lt_1_p) = Coqprime.FGroup.g_order (Coqprime.Zp.ZPGroup p lt_1_p) + (exists y, List.In y (Coqprime.PrimalityTest.FGroup.s (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p)) + /\ Coqprime.PrimalityTest.EGroup.e_order Z.eq_dec y (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p) = Coqprime.PrimalityTest.FGroup.g_order (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p) /\ (forall a (a_range : 1 <= a <= p - 1), exists j, 0 <= j <= p - 1 /\ y ^ j mod p = a)). Proof using Type. intros. - destruct (Coqprime.Zp.Zp_cyclic p lt_1_p prime_p) as [y [y_in_ZPGroup y_order]]. + destruct (Coqprime.PrimalityTest.Zp.Zp_cyclic p lt_1_p prime_p) as [y [y_in_ZPGroup y_order]]. exists y; repeat split; auto. intros. pose proof (in_ZPGroup_range p lt_1_p y y_in_ZPGroup) as y_range1. assert (0 <= y < p) as y_range0 by omega. assert (rel_prime y p) as rel_prime_y_p by (apply rel_prime_le_prime; omega || auto). assert (rel_prime a p) as rel_prime_a_p by (apply rel_prime_le_prime; omega || auto). - assert (List.In a (Coqprime.FGroup.s (Coqprime.Zp.ZPGroup p lt_1_p))) as a_in_ZPGroup by (apply Coqprime.Zp.in_ZPGroup; omega || auto). - destruct (Coqprime.EGroup.support_gpow Z Z.eq_dec (Coqprime.Zp.pmult p) y (Coqprime.Zp.ZPGroup p lt_1_p) y_in_ZPGroup a) + assert (List.In a (Coqprime.PrimalityTest.FGroup.s (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p))) as a_in_ZPGroup by (apply Coqprime.PrimalityTest.Zp.in_ZPGroup; omega || auto). + destruct (Coqprime.PrimalityTest.EGroup.support_gpow Z Z.eq_dec (Coqprime.PrimalityTest.Zp.pmult p) y (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p) y_in_ZPGroup a) as [k [k_range gpow_y_k]]; [apply generator_subgroup_is_group; auto |]. exists k; split. { - unfold Coqprime.EGroup.e_order in y_order. + unfold Coqprime.PrimalityTest.EGroup.e_order in y_order. rewrite y_order in k_range. rewrite mod_p_order in k_range. omega. } { assert (y mod p = y) as y_small by (apply Z.mod_small; omega). rewrite <- y_small in gpow_y_k. - rewrite <- (Coqprime.Zp.Zpower_mod_is_gpow y k p lt_1_p) in gpow_y_k by (omega || auto). + rewrite <- (Coqprime.PrimalityTest.Zp.Zpower_mod_is_gpow y k p lt_1_p) in gpow_y_k by (omega || auto). auto. } Qed. @@ -180,13 +180,13 @@ Proof using Type*. rewrite <- Z.mod_pow in pow_a_x by prime_bound. rewrite <- Z.pow_mul_r in pow_a_x by omega. assert (p - 1 | j * x) as divide_mul_j_x. { - rewrite <- Coqprime.Zp.phi_is_order in y_order. - rewrite Coqprime.Euler.prime_phi_n_minus_1 in y_order by auto. - ereplace (p-1); try eapply Coqprime.EGroup.e_order_divide_gpow; eauto with zarith. + rewrite <- Coqprime.PrimalityTest.Zp.phi_is_order in y_order. + rewrite Coqprime.PrimalityTest.Euler.prime_phi_n_minus_1 in y_order by auto. + ereplace (p-1); try eapply Coqprime.PrimalityTest.EGroup.e_order_divide_gpow; eauto with zarith. simpl. apply in_ZPGroup_range in in_ZPGroup_y. replace y with (y mod p) by (apply Z.mod_small; omega). - erewrite <- Coqprime.Zp.Zpower_mod_is_gpow; eauto. + erewrite <- Coqprime.PrimalityTest.Zp.Zpower_mod_is_gpow; eauto. apply rel_prime_le_prime; (omega || auto). apply Z.mul_nonneg_nonneg; intuition; omega. } -- cgit v1.2.3