diff options
Diffstat (limited to 'coqprime-8.4/Coqprime/PGroup.v')
| -rw-r--r-- | coqprime-8.4/Coqprime/PGroup.v | 347 |
1 files changed, 347 insertions, 0 deletions
diff --git a/coqprime-8.4/Coqprime/PGroup.v b/coqprime-8.4/Coqprime/PGroup.v new file mode 100644 index 000000000..19eff5850 --- /dev/null +++ b/coqprime-8.4/Coqprime/PGroup.v @@ -0,0 +1,347 @@ + +(*************************************************************) +(* 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 *) +(*************************************************************) + +(********************************************************************** + PGroup.v + + Build the group of pairs modulo needed for the theorem of + lucas lehmer + + Definition: PGroup + **********************************************************************) +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.ListAux. +Require Import Coqprime.UList. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.IGroup. + +Open Scope Z_scope. + +Definition base := 3. + + +(************************************** + Equality is decidable on pairs + **************************************) + +Definition P_dec: forall p q: Z * Z, {p = q} + {p <> q}. +intros p1 q1; case p1; case q1; intros z t x y; case (Z_eq_dec x z); intros H1. +case (Z_eq_dec y t); intros H2. +left; eq_tac; auto. +right; contradict H2; injection H2; auto. +right; contradict H1; injection H1; auto. +Defined. + + +(************************************** + Addition of two pairs + **************************************) + +Definition pplus (p q: Z * Z) := let (x ,y) := p in let (z,t) := q in (x + z, y + t). + +(************************************** + Properties of addition + **************************************) + +Theorem pplus_assoc: forall p q r, (pplus p (pplus q r)) = (pplus (pplus p q) r). +intros p q r; case p; case q; case r; intros r1 r2 q1 q2 p1 p2; unfold pplus. +eq_tac; ring. +Qed. + +Theorem pplus_comm: forall p q, (pplus p q) = (pplus q p). +intros p q; case p; case q; intros q1 q2 p1 p2; unfold pplus. +eq_tac; ring. +Qed. + +(************************************** + Multiplication of two pairs + **************************************) + +Definition pmult (p q: Z * Z) := let (x ,y) := p in let (z,t) := q in (x * z + base * y * t, x * t + y * z). + +(************************************** + Properties of multiplication + **************************************) + +Theorem pmult_assoc: forall p q r, (pmult p (pmult q r)) = (pmult (pmult p q) r). +intros p q r; case p; case q; case r; intros r1 r2 q1 q2 p1 p2; unfold pmult. +eq_tac; ring. +Qed. + +Theorem pmult_0_l: forall p, (pmult (0, 0) p) = (0, 0). +intros p; case p; intros x y; unfold pmult; eq_tac; ring. +Qed. + +Theorem pmult_0_r: forall p, (pmult p (0, 0)) = (0, 0). +intros p; case p; intros x y; unfold pmult; eq_tac; ring. +Qed. + +Theorem pmult_1_l: forall p, (pmult (1, 0) p) = p. +intros p; case p; intros x y; unfold pmult; eq_tac; ring. +Qed. + +Theorem pmult_1_r: forall p, (pmult p (1, 0)) = p. +intros p; case p; intros x y; unfold pmult; eq_tac; ring. +Qed. + +Theorem pmult_comm: forall p q, (pmult p q) = (pmult q p). +intros p q; case p; case q; intros q1 q2 p1 p2; unfold pmult. +eq_tac; ring. +Qed. + +Theorem pplus_pmult_dist_l: forall p q r, (pmult p (pplus q r)) = (pplus (pmult p q) (pmult p r)). +intros p q r; case p; case q; case r; intros r1 r2 q1 q2 p1 p2; unfold pplus, pmult. +eq_tac; ring. +Qed. + + +Theorem pplus_pmult_dist_r: forall p q r, (pmult (pplus q r) p) = (pplus (pmult q p) (pmult r p)). +intros p q r; case p; case q; case r; intros r1 r2 q1 q2 p1 p2; unfold pplus, pmult. +eq_tac; ring. +Qed. + +(************************************** + In this section we create the group PGroup of inversible elements {(p, q) | 0 <= p < m /\ 0 <= q < m} + **************************************) +Section Mod. + +Variable m : Z. + +Hypothesis m_pos: 1 < m. + +(************************************** + mkLine creates {(a, p) | 0 <= p < n} + **************************************) + +Fixpoint mkLine (a: Z) (n: nat) {struct n} : list (Z * Z) := + (a, Z_of_nat n) :: match n with O => nil | (S n1) => mkLine a n1 end. + +(************************************** + Some properties of mkLine + **************************************) + +Theorem mkLine_length: forall a n, length (mkLine a n) = (n + 1)%nat. +intros a n; elim n; simpl; auto. +Qed. + +Theorem mkLine_in: forall a n p, 0 <= p <= Z_of_nat n -> (In (a, p) (mkLine a n)). +intros a n; elim n. +simpl; auto with zarith. +intros p (H1, H2); replace p with 0; auto with zarith. +intros n1 Rec p (H1, H2). +case (Zle_lt_or_eq p (Z_of_nat (S n1))); auto with zarith. +rewrite inj_S in H2; auto with zarith. +rewrite inj_S; auto with zarith. +intros H3; right; apply Rec; auto with zarith. +intros H3; subst; simpl; auto. +Qed. + +Theorem in_mkLine: forall a n p, In p (mkLine a n) -> exists q, 0 <= q <= Z_of_nat n /\ p = (a, q). +intros a n p; elim n; clear n. +simpl; intros [H1 | H1]; exists 0; auto with zarith; case H1. +simpl; intros n Rec [H1 | H1]; auto. +exists (Z_of_nat (S n)); auto with zarith. +case Rec; auto; intros q ((H2, H3), H4); exists q; repeat split; auto with zarith. +change (q <= Z_of_nat (S n)). +rewrite inj_S; auto with zarith. +Qed. + +Theorem mkLine_ulist: forall a n, ulist (mkLine a n). +intros a n; elim n; simpl; auto. +intros n1 H; apply ulist_cons; auto. +change (~ In (a, Z_of_nat (S n1)) (mkLine a n1)). +rewrite inj_S; intros H1. +case in_mkLine with (1 := H1); auto with zarith. +intros x ((H2, H3), H4); injection H4. +intros H5; subst; auto with zarith. +Qed. + +(************************************** + mkRect creates the list {(p, q) | 0 <= p < n /\ 0 <= q < m} + **************************************) + +Fixpoint mkRect (n m: nat) {struct n} : list (Z * Z) := + (mkLine (Z_of_nat n) m) ++ match n with O => nil | (S n1) => mkRect n1 m end. + +(************************************** + Some properties of mkRect + **************************************) + +Theorem mkRect_length: forall n m, length (mkRect n m) = ((n + 1) * (m + 1))%nat. +intros n; elim n; simpl; auto. +intros n1; rewrite <- app_nil_end; rewrite mkLine_length; rewrite plus_0_r; auto. +intros n1 Rec m1; rewrite length_app; rewrite Rec; rewrite mkLine_length; auto. +Qed. + +Theorem mkRect_in: forall n m p q, 0 <= p <= Z_of_nat n -> 0 <= q <= Z_of_nat m -> (In (p, q) (mkRect n m)). +intros n m1; elim n; simpl. +intros p q (H1, H2) (H3, H4); replace p with 0; auto with zarith. +rewrite <- app_nil_end; apply mkLine_in; auto. +intros n1 Rec p q (H1, H2) (H3, H4). +case (Zle_lt_or_eq p (Z_of_nat (S n1))); auto with zarith; intros H5. +rewrite inj_S in H5; apply in_or_app; auto with zarith. +apply in_or_app; left; subst; apply mkLine_in; auto with zarith. +Qed. + +Theorem in_mkRect: forall n m p, In p (mkRect n m) -> exists p1, exists p2, 0 <= p1 <= Z_of_nat n /\ 0 <= p2 <= Z_of_nat m /\ p = (p1, p2). +intros n m1 p; elim n; clear n; simpl. +rewrite <- app_nil_end; intros H1. +case in_mkLine with (1 := H1). +intros p2 (H2, H3); exists 0; exists p2; auto with zarith. +intros n Rec H1. +case in_app_or with (1 := H1); intros H2. +case in_mkLine with (1 := H2). +intros p2 (H3, H4); exists (Z_of_nat (S n)); exists p2; subst; simpl; auto with zarith. +case Rec with (1 := H2); auto. +intros p1 (p2, (H3, (H4, H5))); exists p1; exists p2; repeat split; auto with zarith. +change (p1 <= Z_of_nat (S n)). +rewrite inj_S; auto with zarith. +Qed. + +Theorem mkRect_ulist: forall n m, ulist (mkRect n m). +intros n; elim n; simpl; auto. +intros n1; rewrite <- app_nil_end; apply mkLine_ulist; auto. +intros n1 Rec m1; apply ulist_app; auto. +apply mkLine_ulist. +intros a H1 H2. +case in_mkLine with (1 := H1); intros p1 ((H3, H4), H5). +case in_mkRect with (1 := H2); intros p2 (p3, ((H6, H7), ((H8, H9), H10))). +subst; injection H10; clear H10; intros; subst. +contradict H7. +change (~ Z_of_nat (S n1) <= Z_of_nat n1). +rewrite inj_S; auto with zarith. +Qed. + +(************************************** + mL is the list {(p, q) | 0 <= p < m-1 /\ 0 <= q < m - 1} + **************************************) +Definition mL := mkRect (Zabs_nat (m - 1)) (Zabs_nat (m -1)). + +(************************************** + Some properties of mL + **************************************) + +Theorem mL_length : length mL = Zabs_nat (m * m). +unfold mL; rewrite mkRect_length; simpl; apply inj_eq_rev. +repeat (rewrite inj_mult || rewrite inj_plus || rewrite inj_Zabs_nat || rewrite Zabs_eq); simpl; auto with zarith. +eq_tac; auto with zarith. +Qed. + +Theorem mL_in: forall p q, 0 <= p < m -> 0 <= q < m -> (In (p, q) mL). +intros p q (H1, H2) (H3, H4); unfold mL; apply mkRect_in; rewrite inj_Zabs_nat; + rewrite Zabs_eq; auto with zarith. +Qed. + +Theorem in_mL: forall p, In p mL-> exists p1, exists p2, 0 <= p1 < m /\ 0 <= p2 < m /\ p = (p1, p2). +unfold mL; intros p H1; case in_mkRect with (1 := H1). +repeat (rewrite inj_Zabs_nat || rewrite Zabs_eq); auto with zarith. +intros p1 (p2, ((H2, H3), ((H4, H5), H6))); exists p1; exists p2; repeat split; auto with zarith. +Qed. + +Theorem mL_ulist: ulist mL. +unfold mL; apply mkRect_ulist; auto. +Qed. + +(************************************** + We define zpmult the multiplication of pairs module m + **************************************) + +Definition zpmult (p q: Z * Z) := let (x ,y) := pmult p q in (Zmod x m, Zmod y m). + +(************************************** + Some properties of zpmult + **************************************) + +Theorem zpmult_internal: forall p q, (In (zpmult p q) mL). +intros p q; unfold zpmult; case (pmult p q); intros z y; apply mL_in; auto with zarith. +apply Z_mod_lt; auto with zarith. +apply Z_mod_lt; auto with zarith. +Qed. + +Theorem zpmult_assoc: forall p q r, (zpmult p (zpmult q r)) = (zpmult (zpmult p q) r). +assert (U: 0 < m); auto with zarith. +intros p q r; unfold zpmult. +generalize (pmult_assoc p q r). +case (pmult p q); intros x1 x2. +case (pmult q r); intros y1 y2. +case p; case r; unfold pmult. +intros z1 z2 t1 t2 H. +match goal with + H: (?X, ?Y) = (?Z, ?T) |- _ => + assert (H1: X = Z); assert (H2: Y = T); try (injection H; simpl; auto; fail); clear H +end. +eq_tac. +generalize (f_equal (fun x => x mod m) H1). +repeat rewrite <- Zmult_assoc. +repeat (rewrite (fun x => Zplus_mod (t1 * x))); auto. +repeat (rewrite (fun x => Zplus_mod (x1 * x))); auto. +repeat (rewrite (fun x => Zplus_mod (x1 mod m * x))); auto. +repeat (rewrite (Zmult_mod t1)); auto. +repeat (rewrite (Zmult_mod x1)); auto. +repeat (rewrite (Zmult_mod base)); auto. +repeat (rewrite (Zmult_mod t2)); auto. +repeat (rewrite (Zmult_mod x2)); auto. +repeat (rewrite (Zmult_mod (t2 mod m))); auto. +repeat (rewrite (Zmult_mod (x1 mod m))); auto. +repeat (rewrite (Zmult_mod (x2 mod m))); auto. +repeat (rewrite Zmod_mod); auto. +generalize (f_equal (fun x => x mod m) H2). +repeat (rewrite (fun x => Zplus_mod (t1 * x))); auto. +repeat (rewrite (fun x => Zplus_mod (x1 * x))); auto. +repeat (rewrite (fun x => Zplus_mod (x1 mod m * x))); auto. +repeat (rewrite (Zmult_mod t1)); auto. +repeat (rewrite (Zmult_mod x1)); auto. +repeat (rewrite (Zmult_mod t2)); auto. +repeat (rewrite (Zmult_mod x2)); auto. +repeat (rewrite (Zmult_mod (t2 mod m))); auto. +repeat (rewrite (Zmult_mod (x1 mod m))); auto. +repeat (rewrite (Zmult_mod (x2 mod m))); auto. +repeat (rewrite Zmod_mod); auto. +Qed. + +Theorem zpmult_0_l: forall p, (zpmult (0, 0) p) = (0, 0). +intros p; case p; intros x y; unfold zpmult, pmult; simpl. +rewrite Zmod_small; auto with zarith. +Qed. + +Theorem zpmult_1_l: forall p, In p mL -> zpmult (1, 0) p = p. +intros p H; case in_mL with (1 := H); clear H; intros p1 (p2, ((H1, H2), (H3, H4))); subst. +unfold zpmult; rewrite pmult_1_l. +repeat rewrite Zmod_small; auto with zarith. +Qed. + +Theorem zpmult_1_r: forall p, In p mL -> zpmult p (1, 0) = p. +intros p H; case in_mL with (1 := H); clear H; intros p1 (p2, ((H1, H2), (H3, H4))); subst. +unfold zpmult; rewrite pmult_1_r. +repeat rewrite Zmod_small; auto with zarith. +Qed. + +Theorem zpmult_comm: forall p q, zpmult p q = zpmult q p. +intros p q; unfold zpmult; rewrite pmult_comm; auto. +Qed. + +(************************************** + We are now ready to build our group + **************************************) + +Definition PGroup : (FGroup zpmult). +apply IGroup with (support := mL) (e:= (1, 0)). +exact P_dec. +apply mL_ulist. +apply mL_in; auto with zarith. +intros; apply zpmult_internal. +intros; apply zpmult_assoc. +exact zpmult_1_l. +exact zpmult_1_r. +Defined. + +End Mod. |