diff options
Diffstat (limited to 'coqprime-8.4/Coqprime/Zp.v')
| -rw-r--r-- | coqprime-8.4/Coqprime/Zp.v | 411 |
1 files changed, 411 insertions, 0 deletions
diff --git a/coqprime-8.4/Coqprime/Zp.v b/coqprime-8.4/Coqprime/Zp.v new file mode 100644 index 000000000..2f7d28d69 --- /dev/null +++ b/coqprime-8.4/Coqprime/Zp.v @@ -0,0 +1,411 @@ + +(*************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(*************************************************************) +(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) +(*************************************************************) + +(********************************************************************** + Zp.v + + Build the group of the inversible element on {1, 2, .., n-1} + for the multiplication modulo n + + Definition: ZpGroup + **********************************************************************) +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.ZArith.Zpow_facts. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.UList. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.IGroup. +Require Import Coqprime.Cyclic. +Require Import Coqprime.Euler. +Require Import Coqprime.ZProgression. + +Open Scope Z_scope. + +Section Zp. + +Variable n: Z. + +Hypothesis n_pos: 1 < n. + + +(************************************** + mkZp m creates {m, m - 1, ..., 0} + **************************************) + +Fixpoint mkZp_aux (m: nat): list Z:= + Z_of_nat m :: match m with O => nil | (S m1) => mkZp_aux m1 end. + +(************************************** + Some properties of mkZp_aux + **************************************) + +Theorem mkZp_aux_length: forall m, length (mkZp_aux m) = (m + 1)%nat. +intros m; elim m; simpl; auto. +Qed. + +Theorem mkZp_aux_in: forall m p, 0 <= p <= Z_of_nat m -> In p (mkZp_aux m). +intros m; elim m. +simpl; auto with zarith. +intros n1 Rec p (H1, H2); case Zle_lt_or_eq with (1 := H2); clear H2; intro H2. +rewrite inj_S in H2. +simpl; right; apply Rec; split; auto with zarith. +rewrite H2; simpl; auto. +Qed. + +Theorem in_mkZp_aux: forall m p, In p (mkZp_aux m) -> 0 <= p <= Z_of_nat m. +intros m; elim m; clear m. +simpl; intros p H1; case H1; clear H1; intros H1; subst; auto with zarith. +intros m1; generalize (inj_S m1); simpl. +intros H Rec p [H1 | H1]. +rewrite <- H1; rewrite H; auto with zarith. +rewrite H; case (Rec p); auto with zarith. +Qed. + +Theorem mkZp_aux_ulist: forall m, ulist (mkZp_aux m). +intros m; elim m; simpl; auto. +intros m1 H; apply ulist_cons; auto. +change (~ In (Z_of_nat (S m1)) (mkZp_aux m1)). +rewrite inj_S; intros H1. +case in_mkZp_aux with (1 := H1); auto with zarith. +Qed. + +(************************************** + mkZp creates {n - 1, ..., 1, 0} + **************************************) + +Definition mkZp := mkZp_aux (Zabs_nat (n - 1)). + +(************************************** + Some properties of mkZp + **************************************) + +Theorem mkZp_length: length mkZp = Zabs_nat n. +unfold mkZp; rewrite mkZp_aux_length. +apply inj_eq_rev. +rewrite inj_plus. +simpl; repeat rewrite inj_Zabs_nat; auto with zarith. +repeat rewrite Zabs_eq; auto with zarith. +Qed. + +Theorem mkZp_in: forall p, 0 <= p < n -> In p mkZp. +intros p (H1, H2); unfold mkZp; apply mkZp_aux_in. +rewrite inj_Zabs_nat; auto with zarith. +repeat rewrite Zabs_eq; auto with zarith. +Qed. + +Theorem in_mkZp: forall p, In p mkZp -> 0 <= p < n. +intros p H; case (in_mkZp_aux (Zabs_nat (n - 1)) p); auto with zarith. +rewrite inj_Zabs_nat; auto with zarith. +repeat rewrite Zabs_eq; auto with zarith. +Qed. + +Theorem mkZp_ulist: ulist mkZp. +unfold mkZp; apply mkZp_aux_ulist; auto. +Qed. + +(************************************** + Multiplication of two pairs + **************************************) + +Definition pmult (p q: Z) := (p * q) mod n. + +(************************************** + Properties of multiplication + **************************************) + +Theorem pmult_assoc: forall p q r, (pmult p (pmult q r)) = (pmult (pmult p q) r). +assert (Hu: 0 < n); try apply Zlt_trans with 1; auto with zarith. +generalize Zmod_mod; intros H. +intros p q r; unfold pmult. +rewrite (Zmult_mod p); auto. +repeat rewrite Zmod_mod; auto. +rewrite (Zmult_mod q); auto. +rewrite <- Zmult_mod; auto. +rewrite Zmult_assoc. +rewrite (Zmult_mod (p * (q mod n))); auto. +rewrite (Zmult_mod ((p * q) mod n)); auto. +eq_tac; auto. +eq_tac; auto. +rewrite (Zmult_mod p); sauto. +rewrite Zmod_mod; auto. +rewrite <- Zmult_mod; sauto. +Qed. + +Theorem pmult_1_l: forall p, In p mkZp -> pmult 1 p = p. +intros p H; unfold pmult; rewrite Zmult_1_l. +apply Zmod_small. +case (in_mkZp p); auto with zarith. +Qed. + +Theorem pmult_1_r: forall p, In p mkZp -> pmult p 1 = p. +intros p H; unfold pmult; rewrite Zmult_1_r. +apply Zmod_small. +case (in_mkZp p); auto with zarith. +Qed. + +Theorem pmult_comm: forall p q, pmult p q = pmult q p. +intros p q; unfold pmult; rewrite Zmult_comm; auto. +Qed. + +Definition Lrel := isupport_aux _ pmult mkZp 1 Z_eq_dec (progression Zsucc 0 (Zabs_nat n)). + +Theorem rel_prime_is_inv: + forall a, is_inv Z pmult mkZp 1 Z_eq_dec a = if (rel_prime_dec a n) then true else false. +assert (Hu: 0 < n); try apply Zlt_trans with 1; auto with zarith. +intros a; case (rel_prime_dec a n); intros H. +assert (H1: Bezout a n 1); try apply rel_prime_bezout; auto. +inversion H1 as [c d Hcd]; clear H1. +assert (pmult (c mod n) a = 1). +unfold pmult; rewrite Zmult_mod; try rewrite Zmod_mod; auto. +rewrite <- Zmult_mod; auto. +replace (c * a) with (1 + (-d) * n). +rewrite Z_mod_plus; auto with zarith. +rewrite Zmod_small; auto with zarith. +rewrite <- Hcd; ring. +apply is_inv_true with (a := (c mod n)); auto. +apply mkZp_in; auto with zarith. +exact pmult_1_l. +exact pmult_1_r. +rewrite pmult_comm; auto. +apply mkZp_in; auto with zarith. +apply Z_mod_lt; auto with zarith. +apply is_inv_false. +intros c H1; left; intros H2; contradict H. +apply bezout_rel_prime. +apply Bezout_intro with c (- (Zdiv (c * a) n)). +pattern (c * a) at 1; rewrite (Z_div_mod_eq (c * a) n); auto with zarith. +unfold pmult in H2; rewrite (Zmult_comm c); try rewrite H2. +ring. +Qed. + +(************************************** + We are now ready to build our group + **************************************) + +Definition ZPGroup : (FGroup pmult). +apply IGroup with (support := mkZp) (e:= 1). +exact Z_eq_dec. +apply mkZp_ulist. +apply mkZp_in; auto with zarith. +intros a b H1 H2; apply mkZp_in. +unfold pmult; apply Z_mod_lt; auto with zarith. +intros; apply pmult_assoc. +exact pmult_1_l. +exact pmult_1_r. +Defined. + +Theorem in_ZPGroup: forall p, rel_prime p n -> 0 <= p < n -> In p ZPGroup.(s). +intros p H (H1, H2); unfold ZPGroup; simpl. +apply isupport_is_in. +generalize (rel_prime_is_inv p); case (rel_prime_dec p); auto. +apply mkZp_in; auto with zarith. +Qed. + + +Theorem phi_is_length: phi n = Z_of_nat (length Lrel). +assert (Hu: 0 < n); try apply Zlt_trans with 1; auto with zarith. +rewrite phi_def_with_0; auto. +unfold Zsum, Lrel; rewrite Zle_imp_le_bool; auto with zarith. +replace (1 + (n - 1) - 0) with n; auto with zarith. +elim (progression Zsucc 0 (Zabs_nat n)); simpl; auto. +intros a l1 Rec. +rewrite Rec. +rewrite rel_prime_is_inv. +case (rel_prime_dec a n); auto with zarith. +simpl length; rewrite inj_S; auto with zarith. +Qed. + +Theorem phi_is_order: phi n = g_order ZPGroup. +unfold g_order; rewrite phi_is_length. +eq_tac; apply permutation_length. +apply ulist_incl2_permutation. +unfold Lrel; apply isupport_aux_ulist. +apply ulist_Zprogression; auto. +apply ZPGroup.(unique_s). +intros a H; unfold ZPGroup; simpl. +apply isupport_is_in. +unfold Lrel in H; apply isupport_aux_is_inv_true with (1 := H). +apply mkZp_in; auto. +assert (In a (progression Zsucc 0 (Zabs_nat n))). +apply (isupport_aux_incl _ pmult mkZp 1 Z_eq_dec); auto. +split. +apply Zprogression_le_init with (1 := H0). +replace n with (0 + Z_of_nat (Zabs_nat n)). +apply Zprogression_le_end with (1 := H0). +rewrite inj_Zabs_nat; auto with zarith. +rewrite Zabs_eq; auto with zarith. +intros a H; unfold Lrel; simpl. +apply isupport_aux_is_in. +simpl in H; apply isupport_is_inv_true with (1 := H). +apply in_Zprogression. +rewrite Zplus_0_l; rewrite inj_Zabs_nat; auto with zarith. +rewrite Zabs_eq; auto with zarith. +assert (In a mkZp). +apply (isupport_aux_incl _ pmult mkZp 1 Z_eq_dec); auto. +apply in_mkZp; auto. +Qed. + +Theorem Zp_cyclic: prime n -> cyclic Z_eq_dec ZPGroup. +intros H1. +unfold ZPGroup, pmult; +generalize (cyclic_field _ (fun x y => (x + y) mod n) (fun x y => (x * y) mod n) (fun x => (-x) mod n) 0); +unfold IA; intros tmp; apply tmp; clear tmp; auto. +intros; discriminate. +apply mkZp_in; auto with zarith. +intros; apply mkZp_in; auto with zarith. +apply Z_mod_lt; auto with zarith. +intros; rewrite Zplus_0_l; auto. +apply Zmod_small; auto. +apply in_mkZp; auto. +intros; rewrite Zplus_comm; auto. +intros a b c Ha Hb Hc. +pattern a at 1; rewrite <- (Zmod_small a n); auto with zarith. +pattern c at 2; rewrite <- (Zmod_small c n); auto with zarith. +repeat rewrite <- Zplus_mod; auto with zarith. +eq_tac; auto with zarith. +apply in_mkZp; auto. +apply in_mkZp; auto. +intros; eq_tac; auto with zarith. +intros a b c Ha Hb Hc. +pattern a at 1; rewrite <- (Zmod_small a n); auto with zarith. +repeat rewrite <- Zmult_mod; auto with zarith. +repeat rewrite <- Zplus_mod; auto with zarith. +eq_tac; auto with zarith. +apply in_mkZp; auto. +intros; apply mkZp_in; apply Z_mod_lt; auto with zarith. +intros a Ha. +pattern a at 1; rewrite <- (Zmod_small a n); auto with zarith. +repeat rewrite <- Zplus_mod; auto with zarith. +rewrite <- (Zmod_small 0 n); auto with zarith. +eq_tac; auto with zarith. +apply in_mkZp; auto. +intros a b Ha Hb H; case (prime_mult n H1 a b). +apply Zmod_divide; auto with zarith. +intros H2; left. +case (Zle_lt_or_eq 0 a); auto. +case (in_mkZp a); auto. +intros H3; absurd (n <= a). +apply Zlt_not_le. +case (in_mkZp a); auto. +apply Zdivide_le; auto with zarith. +intros H2; right. +case (Zle_lt_or_eq 0 b); auto. +case (in_mkZp b); auto. +intros H3; absurd (n <= b). +apply Zlt_not_le. +case (in_mkZp b); auto. +apply Zdivide_le; auto with zarith. +Qed. + +End Zp. + +(* Definition of the order (0 for q < 1) *) + +Definition Zorder: Z -> Z -> Z. +intros p q; case (Z_le_dec q 1); intros H. +exact 0. +refine (e_order Z_eq_dec (p mod q) (ZPGroup q _)); auto with zarith. +Defined. + +Theorem Zorder_pos: forall p n, 0 <= Zorder p n. +intros p n; unfold Zorder. +case (Z_le_dec n 1); auto with zarith. +intros n1. +apply Zlt_le_weak; apply e_order_pos. +Qed. + +Theorem in_mod_ZPGroup + : forall (n : Z) (n_pos : 1 < n) (p : Z), + rel_prime p n -> In (p mod n) (s (ZPGroup n n_pos)). +intros n H p H1. +apply in_ZPGroup; auto. +apply rel_prime_mod; auto with zarith. +apply Z_mod_lt; auto with zarith. +Qed. + + +Theorem Zpower_mod_is_gpow: + forall p q n (Hn: 1 < n), rel_prime p n -> 0 <= q -> p ^ q mod n = gpow (p mod n) (ZPGroup n Hn) q. +intros p q n H Hp H1; generalize H1; pattern q; apply natlike_ind; simpl; auto. +intros _; apply Zmod_small; auto with zarith. +intros n1 Hn1 Rec _; simpl. +generalize (in_mod_ZPGroup _ H _ Hp); intros Hu. +unfold Zsucc; rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith. +rewrite gpow_add; auto with zarith. +rewrite gpow_1; auto; rewrite <- Rec; auto. +rewrite Zmult_mod; auto. +Qed. + + +Theorem Zorder_div_power: forall p q n, 1 < n -> rel_prime p n -> p ^ q mod n = 1 -> (Zorder p n | q). +intros p q n H H1 H2. +assert (Hq: 0 <= q). +generalize H2; case q; simpl; auto with zarith. +intros p1 H3; contradict H3; rewrite Zmod_small; auto with zarith. +unfold Zorder; case (Z_le_dec n 1). +intros H3; contradict H; auto with zarith. +intros H3; apply e_order_divide_gpow; auto. +apply in_mod_ZPGroup; auto. +rewrite <- Zpower_mod_is_gpow; auto with zarith. +Qed. + +Theorem Zorder_div: forall p n, prime n -> ~(n | p) -> (Zorder p n | n - 1). +intros p n H; unfold Zorder. +case (Z_le_dec n 1); intros H1 H2. +contradict H1; generalize (prime_ge_2 n H); auto with zarith. +rewrite <- prime_phi_n_minus_1; auto. +match goal with |- context[ZPGroup _ ?H2] => rewrite phi_is_order with (n_pos := H2) end. +apply e_order_divide_g_order; auto. +apply in_mod_ZPGroup; auto. +apply rel_prime_sym; apply prime_rel_prime; auto. +Qed. + + +Theorem Zorder_power_is_1: forall p n, 1 < n -> rel_prime p n -> p ^ (Zorder p n) mod n = 1. +intros p n H H1; unfold Zorder. +case (Z_le_dec n 1); intros H2. +contradict H; auto with zarith. +let x := match goal with |- context[ZPGroup _ ?X] => X end in rewrite Zpower_mod_is_gpow with (Hn := x); auto with zarith. +rewrite gpow_e_order_is_e. +reflexivity. +apply in_mod_ZPGroup; auto. +apply Zlt_le_weak; apply e_order_pos. +Qed. + +Theorem Zorder_power_pos: forall p n, 1 < n -> rel_prime p n -> 0 < Zorder p n. +intros p n H H1; unfold Zorder. +case (Z_le_dec n 1); intros H2. +contradict H; auto with zarith. +apply e_order_pos. +Qed. + +Theorem phi_power_is_1: forall p n, 1 < n -> rel_prime p n -> p ^ (phi n) mod n = 1. +intros p n H H1. +assert (V1:= Zorder_power_pos p n H H1). +assert (H2: (Zorder p n | phi n)). +unfold Zorder. +case (Z_le_dec n 1); intros H2. +contradict H; auto with zarith. +match goal with |- context[ZPGroup n ?H] => +rewrite phi_is_order with (n_pos := H) +end. +apply e_order_divide_g_order. +apply in_mod_ZPGroup; auto. +case H2; clear H2; intros q H2; rewrite H2. +rewrite Zmult_comm. +assert (V2 := (phi_pos _ H)). +assert (V3: 0 <= q). +rewrite H2 in V2. +apply Zlt_le_weak; apply Zmult_lt_0_reg_r with (2 := V2); auto with zarith. +rewrite Zpower_mult; auto with zarith. +rewrite Zpower_mod; auto with zarith. +rewrite Zorder_power_is_1; auto. +rewrite Zpower_1_l; auto with zarith. +apply Zmod_small; auto with zarith. +Qed. |