From d3135a69f653034f07b7657486f926a7a20ef3ee Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 1 Jun 2017 23:59:55 -0400 Subject: Strip trailing whitespace With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ``` --- coqprime/Coqprime/Cyclic.v | 16 ++-- coqprime/Coqprime/EGroup.v | 60 ++++++------ coqprime/Coqprime/Euler.v | 6 +- coqprime/Coqprime/FGroup.v | 26 ++--- coqprime/Coqprime/IGroup.v | 44 ++++----- coqprime/Coqprime/Iterator.v | 40 ++++---- coqprime/Coqprime/Lagrange.v | 30 +++--- coqprime/Coqprime/ListAux.v | 72 +++++++------- coqprime/Coqprime/LucasLehmer.v | 61 ++++++------ coqprime/Coqprime/NatAux.v | 10 +- coqprime/Coqprime/PGroup.v | 46 ++++----- coqprime/Coqprime/Permutation.v | 122 +++++++++++------------ coqprime/Coqprime/Pmod.v | 154 +++++++++++++++--------------- coqprime/Coqprime/Pocklington.v | 28 +++--- coqprime/Coqprime/PocklingtonCertificat.v | 153 +++++++++++++++-------------- coqprime/Coqprime/Root.v | 42 ++++---- coqprime/Coqprime/Tactic.v | 28 +++--- coqprime/Coqprime/UList.v | 54 +++++------ coqprime/Coqprime/ZCAux.v | 26 ++--- coqprime/Coqprime/ZCmisc.v | 30 +++--- coqprime/Coqprime/ZProgression.v | 16 ++-- coqprime/Coqprime/ZSum.v | 30 +++--- coqprime/Coqprime/Zp.v | 40 ++++---- coqprime/Makefile | 5 +- 24 files changed, 568 insertions(+), 571 deletions(-) (limited to 'coqprime') diff --git a/coqprime/Coqprime/Cyclic.v b/coqprime/Coqprime/Cyclic.v index c25f683ca..7a9d8e19b 100644 --- a/coqprime/Coqprime/Cyclic.v +++ b/coqprime/Coqprime/Cyclic.v @@ -7,9 +7,9 @@ (*************************************************************) (*********************************************************************** - Cyclic.v - - Proof that an abelien ring is cyclic + Cyclic.v + + Proof that an abelien ring is cyclic ************************************************************************) Require Import ZCAux. Require Import List. @@ -50,13 +50,13 @@ Hypothesis op_internal: forall a, In a support -> In (op a) support. Hypothesis plus_op_zero: forall a, In a support -> plus a (op a) = zero. Hypothesis mult_integral: forall a b, In a support -> In b support -> mult a b = zero -> a = zero \/ b = zero. -Definition IA := (IGroup A mult support e A_dec support_ulist e_in_support mult_internal +Definition IA := (IGroup A mult support e A_dec support_ulist e_in_support mult_internal mult_assoc e_is_zero_l e_is_zero_r). Hint Resolve (fun x => isupport_incl _ mult support e A_dec x). -Theorem gpow_evaln: forall n, 0 < n -> +Theorem gpow_evaln: forall n, 0 < n -> exists p, (length p <= Zabs_nat n)%nat /\ (forall i, In i p -> In i support) /\ forall x, In x IA.(s) -> eval A plus mult zero (zero::p) x = gpow x IA n. intros n Hn; generalize Hn; pattern n; apply natlike_ind; auto with zarith. @@ -92,7 +92,7 @@ intros l n; elim l; simpl; auto. intros H; left; intros a H1; case H1. intros a l1 Rec H. case (A_dec (gpow a IA n) e); intros H2. -case Rec; try intros H3. +case Rec; try intros H3. apply incl_tran with (2 := H); auto with datatypes. left; intros a1 H4; case H4; auto. intros H5; rewrite <- H5; auto. @@ -146,7 +146,7 @@ case (check_list_gpow IA.(s) i); try intros H; auto with datatypes. case (gpow_evaln i); auto; intros p (Hp1, (Hp2, Hp3)). absurd ((op e) = zero). intros H1; case e_not_zero. -rewrite <- (plus_op_zero e); try rewrite H1; auto. +rewrite <- (plus_op_zero e); try rewrite H1; auto. rewrite plus_comm; auto. apply (root_max_is_zero _ (fun x => In x support) plus mult op zero) with (l := IA.(s)) (p := op e :: p); auto with datatypes. simpl; intros x [Hx | Hx]; try rewrite <- Hx; auto. @@ -161,7 +161,7 @@ apply inj_lt_inv. rewrite inj_Zabs_nat; auto with zarith. rewrite Zabs_eq; auto with zarith. Qed. - + Theorem divide_g_order_e_order: forall n, 0 <= n -> (n | g_order IA) -> exists a, In a IA.(s) /\ e_order A_dec a IA = n. intros n Hn H. assert (Hg: 0 < g_order IA). diff --git a/coqprime/Coqprime/EGroup.v b/coqprime/Coqprime/EGroup.v index 933176abd..2752bb002 100644 --- a/coqprime/Coqprime/EGroup.v +++ b/coqprime/Coqprime/EGroup.v @@ -7,8 +7,8 @@ (*************************************************************) (********************************************************************** - EGroup.v - + EGroup.v + Given an element a, create the group {e, a, a^2, ..., a^n} **********************************************************************) Require Import ZArith. @@ -38,10 +38,10 @@ Variable G: FGroup op. Hypothesis a_in_G: In a G.(s). -(************************************** +(************************************** The power function for the group **************************************) - + Set Implicit Arguments. Definition gpow n := match n with Zpos p => iter_pos _ (op a) G.(e) p | _ => G.(e) end. Unset Implicit Arguments. @@ -54,10 +54,10 @@ Theorem gpow_1 : gpow 1 = a. simpl; sauto. Qed. -(************************************** +(************************************** Some properties of the power function **************************************) - + Theorem gpow_in: forall n, In (gpow n) G.(s). intros n; case n; simpl; auto. intros p; apply iter_pos_invariant with (Inv := fun x => In x G.(s)); auto. @@ -91,7 +91,7 @@ rewrite iter_pos_plus; rewrite (fun x y => gpow_op (iter_pos A x y p2)); auto. exact (gpow_in (Zpos p2)). Qed. -Theorem gpow_1_more: +Theorem gpow_1_more: forall n, 0 < n -> gpow n = G.(e) -> forall m, 0 <= m -> exists p, 0 <= p < n /\ gpow m = gpow p. intros n H1 H2 m Hm; generalize Hm; pattern m; apply Z_lt_induction; auto with zarith; clear m Hm. intros m Rec Hm. @@ -110,7 +110,7 @@ apply g_cancel_l with (g:= G) (a := gpow n); sauto. rewrite <- gpow_add; try rewrite <- H3; sauto. Qed. -(************************************** +(************************************** We build the support by iterating the power function **************************************) @@ -118,21 +118,21 @@ Set Implicit Arguments. Fixpoint support_aux (b: A) (n: nat) {struct n}: list A := b::let c := op a b in - match n with - O => nil | - (S n1) =>if A_dec c G.(e) then nil else support_aux c n1 + match n with + O => nil | + (S n1) =>if A_dec c G.(e) then nil else support_aux c n1 end. Definition support := support_aux G.(e) (Zabs_nat (g_order G)). Unset Implicit Arguments. -(************************************** +(************************************** Some properties of the support that helps to prove that we have a group **************************************) -Theorem support_aux_gpow: - forall n m b, 0 <= m -> In b (support_aux (gpow m) n) -> +Theorem support_aux_gpow: + forall n m b, 0 <= m -> In b (support_aux (gpow m) n) -> exists p, (0 <= p < length (support_aux (gpow m) n))%nat /\ b = gpow (m + Z_of_nat p). intros n; elim n; simpl. intros n1 b Hm [H1 | H1]; exists 0%nat; simpl; rewrite Zplus_0_r; auto; case H1. @@ -143,13 +143,13 @@ case H2. case (Rec (1 + m) b); auto with zarith. rewrite gpow_add; auto with zarith. rewrite gpow_1; auto. -intros p (Hp1, Hp2); exists (S p); split; auto with zarith. +intros p (Hp1, Hp2); exists (S p); split; auto with zarith. rewrite <- gpow_1. rewrite <- gpow_add; auto with zarith. rewrite inj_S; rewrite Hp2; eq_tac; auto with zarith. Qed. -Theorem gpow_support_aux_not_e: +Theorem gpow_support_aux_not_e: forall n m p, 0 <= m -> m < p < m + Z_of_nat (length (support_aux (gpow m) n)) -> gpow p <> G.(e). intros n; elim n; simpl. intros m p Hm (H1, H2); contradict H2; auto with zarith. @@ -186,8 +186,8 @@ intros n; elim n; simpl; auto. intros n1 Rec a1; case (A_dec (op a a1) G.(e)); simpl; auto with arith. Qed. -Theorem support_aux_length_le_is_e: - forall n m, 0 <= m -> (length (support_aux (gpow m) n) <= n)%nat -> +Theorem support_aux_length_le_is_e: + forall n m, 0 <= m -> (length (support_aux (gpow m) n) <= n)%nat -> gpow (m + Z_of_nat (length (support_aux (gpow m) n))) = G.(e) . intros n; elim n; simpl; auto. intros m _ H1; contradict H1; auto with arith. @@ -201,8 +201,8 @@ rewrite <- gpow_add; auto with zarith. rewrite Zplus_assoc; rewrite (Zplus_comm 1); intros H2; apply Rec; auto with zarith. Qed. -Theorem support_aux_in: - forall n m p, 0 <= m -> (p < length (support_aux (gpow m) n))% nat -> +Theorem support_aux_in: + forall n m p, 0 <= m -> (p < length (support_aux (gpow m) n))% nat -> (In (gpow (m + Z_of_nat p)) (support_aux (gpow m) n)). intros n; elim n; simpl; auto; clear n. intros m p Hm H1; replace p with 0%nat. @@ -224,7 +224,7 @@ rewrite <- gpow_1; rewrite <- gpow_add; auto with zarith. rewrite Zplus_assoc; rewrite (Zplus_comm 1); intros H2; right; apply Rec; auto with zarith. Qed. -Theorem support_aux_ulist: +Theorem support_aux_ulist: forall n m, 0 <= m -> (forall p, 0 <= p < m -> gpow (1 + p) <> G.(e)) -> ulist (support_aux (gpow m) n). intros n; elim n; auto; clear n. intros m _ _; auto. @@ -338,13 +338,13 @@ apply inj_le_rev; rewrite inj_Zabs_nat; auto with zarith. rewrite Zabs_eq; auto with zarith. Qed. -(************************************** +(************************************** We are now ready to build the group **************************************) Definition Gsupport: (FGroup op). generalize support_incl_G; unfold incl; intros Ho. -apply mkGroup with support G.(e) G.(i); sauto. +apply mkGroup with support G.(e) G.(i); sauto. apply support_ulist. apply support_internal. intros a1 b1 c1 H1 H2 H3; apply G.(assoc); sauto. @@ -352,7 +352,7 @@ apply support_in_e. apply support_i_internal. Defined. -(************************************** +(************************************** Definition of the order of an element **************************************) Set Implicit Arguments. @@ -361,7 +361,7 @@ Definition e_order := Z_of_nat (length support). Unset Implicit Arguments. -(************************************** +(************************************** Some properties of the order of an element **************************************) @@ -474,7 +474,7 @@ apply Zpower_ge_0; auto with zarith. Qed. Theorem gpow_mult: forall (A : Set) (op : A -> A -> A) (a b: A) (G : FGroup op) - (comm: forall a b, In a (s G) -> In b (s G) -> op a b = op b a), + (comm: forall a b, In a (s G) -> In b (s G) -> op a b = op b a), In a (s G) -> In b (s G) -> forall n, 0 <= n -> gpow (op a b) G n = op (gpow a G n) (gpow b G n). intros A op a b G comm Ha Hb n; case n; simpl; auto. intros _; rewrite G.(e_is_zero_r); auto. @@ -504,8 +504,8 @@ case H4; intros q3 H5; exists q3; rewrite H2; rewrite H5; auto with zarith. Qed. Theorem order_mult: forall (A : Set) (op : A -> A -> A) (A_dec: forall a b: A, {a = b} + {~ a = b}) (G : FGroup op) - (comm: forall a b, In a (s G) -> In b (s G) -> op a b = op b a) (a b: A), - In a (s G) -> In b (s G) -> rel_prime (e_order A_dec a G) (e_order A_dec b G) -> + (comm: forall a b, In a (s G) -> In b (s G) -> op a b = op b a) (a b: A), + In a (s G) -> In b (s G) -> rel_prime (e_order A_dec a G) (e_order A_dec b G) -> e_order A_dec (op a b) G = e_order A_dec a G * e_order A_dec b G. intros A op A_dec G comm a b Ha Hb Hab. assert (Hoat: 0 < e_order A_dec a G); try apply e_order_pos. @@ -576,10 +576,10 @@ case (e_order_divide_gpow A Adec op a G H1 m F1 H2); intros q Hq. assert (F2: 1 <= q). case (Zle_or_lt 0 q); intros HH. case (Zle_lt_or_eq _ _ HH); auto with zarith. - intros HH1; generalize Hm; rewrite Hq; rewrite <- HH1; + intros HH1; generalize Hm; rewrite Hq; rewrite <- HH1; auto with zarith. assert (F2: 0 <= (- q) * e_order Adec a G); auto with zarith. - apply Zmult_le_0_compat; auto with zarith. + apply Zmult_le_0_compat; auto with zarith. apply Zlt_le_weak; apply e_order_pos. generalize F2; rewrite Zopp_mult_distr_l_reverse; rewrite <- Hq; auto with zarith. diff --git a/coqprime/Coqprime/Euler.v b/coqprime/Coqprime/Euler.v index 06d92ce57..93f6956ba 100644 --- a/coqprime/Coqprime/Euler.v +++ b/coqprime/Coqprime/Euler.v @@ -20,7 +20,7 @@ Open Scope Z_scope. Definition phi n := Zsum 1 (n - 1) (fun x => if rel_prime_dec x n then 1 else 0). -Theorem phi_def_with_0: +Theorem phi_def_with_0: forall n, 1< n -> phi n = Zsum 0 (n - 1) (fun x => if rel_prime_dec x n then 1 else 0). intros n H; rewrite Zsum_S_left; auto with zarith. case (rel_prime_dec 0 n); intros H2. @@ -47,7 +47,7 @@ Qed. Theorem phi_le_n_minus_1: forall n, 1 < n -> phi n <= n - 1. intros n H; replace (n-1) with ((1 + (n - 1) - 1) * 1); auto with zarith. -rewrite <- Zsum_c; auto with zarith. +rewrite <- Zsum_c; auto with zarith. unfold phi; apply Zsum_le; auto with zarith. intros x H1; case (rel_prime_dec x n); auto with zarith. Qed. @@ -59,7 +59,7 @@ assert (2 <= n); auto with zarith. apply prime_ge_2; auto. rewrite <- Zsum_c; auto with zarith; unfold phi; apply Zsum_ext; auto. intros x (H2, H3); case H; clear H; intros H H1. -generalize (H1 x); case (rel_prime_dec x n); auto with zarith. +generalize (H1 x); case (rel_prime_dec x n); auto with zarith. intros H6 H7; contradict H6; apply H7; split; auto with zarith. Qed. diff --git a/coqprime/Coqprime/FGroup.v b/coqprime/Coqprime/FGroup.v index a55710e7c..ee18761ab 100644 --- a/coqprime/Coqprime/FGroup.v +++ b/coqprime/Coqprime/FGroup.v @@ -7,22 +7,22 @@ (*************************************************************) (********************************************************************** - FGroup.v - - Defintion and properties of finite groups - - Definition: FGroup + FGroup.v + + Defintion and properties of finite groups + + Definition: FGroup **********************************************************************) Require Import List. Require Import UList. Require Import Tactic. Require Import ZArith. -Open Scope Z_scope. +Open Scope Z_scope. Set Implicit Arguments. -(************************************** +(************************************** A finite group is defined for an operation op it has a support (s) op operates inside the group (internal) @@ -32,7 +32,7 @@ Set Implicit Arguments. the inverse operates inside the group (i_internal) it gives an inverse (i_is_inverse_l is_is_inverse_r) **************************************) - + Record FGroup (A: Set) (op: A -> A -> A): Set := mkGroup {s : (list A); unique_s: ulist s; @@ -48,10 +48,10 @@ Record FGroup (A: Set) (op: A -> A -> A): Set := mkGroup i_is_inverse_r: forall a, (In a s) -> op a (i a) = e }. -(************************************** +(************************************** The order of a group is the lengh of the support **************************************) - + Definition g_order (A: Set) (op: A -> A -> A) (g: FGroup op) := Z_of_nat (length g.(s)). Unset Implicit Arguments. @@ -65,7 +65,7 @@ Section FGroup. Variable A: Set. Variable op: A -> A -> A. -(************************************** +(************************************** Some properties of a finite group **************************************) @@ -91,7 +91,7 @@ apply sym_equal; apply assoc with g; sauto. replace (op a (g.(i) a)) with g.(e); sauto. Qed. -Theorem e_unique: forall (g : FGroup op), forall e1, In e1 g.(s) -> (forall a, In a g.(s) -> op e1 a = a) -> e1 = g.(e). +Theorem e_unique: forall (g : FGroup op), forall e1, In e1 g.(s) -> (forall a, In a g.(s) -> op e1 a = a) -> e1 = g.(e). intros g e1 He1 H2. apply trans_equal with (op e1 g.(e)); sauto. Qed. @@ -110,7 +110,7 @@ intro g; apply g_cancel_l with (g:= g) (a := g.(e)); sauto. apply trans_equal with g.(e); sauto. Qed. -(************************************** +(************************************** A group has at least one element **************************************) diff --git a/coqprime/Coqprime/IGroup.v b/coqprime/Coqprime/IGroup.v index 11a73d414..775596a71 100644 --- a/coqprime/Coqprime/IGroup.v +++ b/coqprime/Coqprime/IGroup.v @@ -7,11 +7,11 @@ (*************************************************************) (********************************************************************** - Igroup - + Igroup + Build the group of the inversible elements for the operation - - Definition: ZpGroup + + Definition: ZpGroup **********************************************************************) Require Import ZArith. Require Import Tactic. @@ -37,12 +37,12 @@ Hypothesis op_assoc: forall a b c, In a support -> In b support -> In c support Hypothesis e_is_zero_l: forall a, In a support -> op e a = a. Hypothesis e_is_zero_r: forall a, In a support -> op a e = a. -(************************************** +(************************************** is_inv_aux tests if there is an inverse of a for op in l **************************************) Fixpoint is_inv_aux (l: list A) (a: A) {struct l}: bool := - match l with nil => false | cons b l1 => + match l with nil => false | cons b l1 => if (A_dec (op a b) e) then if (A_dec (op b a) e) then true else is_inv_aux l1 a else is_inv_aux l1 a end. @@ -52,19 +52,19 @@ intros a l1 Rec H; case (A_dec (op a b) e); case (A_dec (op b a) e); auto. intros H1 H2; case (H a); auto; intros H3; case H3; auto. Qed. -(************************************** +(************************************** is_inv tests if there is an inverse in support **************************************) Definition is_inv := is_inv_aux support. -(************************************** +(************************************** isupport_aux returns the sublist of inversible element of support **************************************) Fixpoint isupport_aux (l: list A) : list A := match l with nil => nil | cons a l1 => if is_inv a then a::isupport_aux l1 else isupport_aux l1 end. -(************************************** +(************************************** Some properties of isupport_aux **************************************) @@ -82,7 +82,7 @@ case (is_inv b); auto with datatypes. Qed. -Theorem isupport_aux_not_in: +Theorem isupport_aux_not_in: forall b l, (forall a, (In a support) -> op b a <> e \/ op a b <> e) -> ~ In b (isupport_aux l). intros b l; elim l; simpl; simpl; auto. intros a l1 H; case_eq (is_inv a); intros H1; simpl; auto. @@ -107,13 +107,13 @@ apply H1; apply ulist_app_inv_r with (a:: nil); auto. apply H1; apply ulist_app_inv_r with (a:: nil); auto. Qed. -(************************************** +(************************************** isupport is the sublist of inversible element of support **************************************) Definition isupport := isupport_aux support. -(************************************** +(************************************** Some properties of isupport **************************************) @@ -140,17 +140,17 @@ apply isupport_ulist. apply isupport_incl. Qed. -Theorem isupport_length_strict: - forall b, (In b support) -> (forall a, (In a support) -> op b a <> e \/ op a b <> e) -> +Theorem isupport_length_strict: + forall b, (In b support) -> (forall a, (In a support) -> op b a <> e \/ op a b <> e) -> (length isupport < length support)%nat. intros b H H1; apply ulist_incl_length_strict. apply isupport_ulist. apply isupport_incl. intros H2; case (isupport_aux_not_in b support); auto. Qed. - + Fixpoint inv_aux (l: list A) (a: A) {struct l}: A := - match l with nil => e | cons b l1 => + match l with nil => e | cons b l1 => if A_dec (op a b) e then if (A_dec (op b a) e) then b else inv_aux l1 a else inv_aux l1 a end. @@ -180,25 +180,25 @@ intros l a; elim l; simpl; auto. intros b l1; case (A_dec (op a b) e); case (A_dec (op b a) e); intros _ _ [H1 | H1]; auto. Qed. -(************************************** +(************************************** The inverse function **************************************) Definition inv := inv_aux support. -(************************************** +(************************************** Some properties of inv **************************************) Theorem inv_prop_r: forall a, In a isupport -> op a (inv a) = e. intros a H; unfold inv; apply inv_aux_prop_r with (l := support). -change (is_inv a = true). +change (is_inv a = true). apply isupport_is_inv_true; auto. Qed. Theorem inv_prop_l: forall a, In a isupport -> op (inv a) a = e. intros a H; unfold inv; apply inv_aux_prop_l with (l := support). -change (is_inv a = true). +change (is_inv a = true). apply isupport_is_inv_true; auto. Qed. @@ -220,8 +220,8 @@ case (inv_aux_in support a); unfold inv; auto. intros H1; rewrite H1; apply e_in_support; auto with zarith. Qed. -(************************************** - We are now ready to build our group +(************************************** + We are now ready to build our group **************************************) Definition IGroup : (FGroup op). diff --git a/coqprime/Coqprime/Iterator.v b/coqprime/Coqprime/Iterator.v index 96d3e5655..dbfde2c38 100644 --- a/coqprime/Coqprime/Iterator.v +++ b/coqprime/Coqprime/Iterator.v @@ -9,7 +9,7 @@ Require Export List. Require Export Permutation. Require Import Arith. - + Section Iterator. Variables A B : Set. Variable zero : B. @@ -18,17 +18,17 @@ Variable g : B -> B -> B. Hypothesis g_zero : forall a, g a zero = a. Hypothesis g_trans : forall a b c, g a (g b c) = g (g a b) c. Hypothesis g_sym : forall a b, g a b = g b a. - + Definition iter := fold_right (fun a r => g (f a) r) zero. Hint Unfold iter . - + Theorem iter_app: forall l1 l2, iter (app l1 l2) = g (iter l1) (iter l2). intros l1; elim l1; simpl; auto. intros l2; rewrite g_sym; auto. intros a l H l2; rewrite H. rewrite g_trans; auto. Qed. - + Theorem iter_permutation: forall l1 l2, permutation l1 l2 -> iter l1 = iter l2. intros l1 l2 H; elim H; simpl; auto; clear H l1 l2. intros a l1 l2 H1 H2; apply f_equal2 with ( f := g ); auto. @@ -36,7 +36,7 @@ intros a b l; (repeat rewrite g_trans). apply f_equal2 with ( f := g ); auto. intros l1 l2 l3 H H0 H1 H2; apply trans_equal with ( 1 := H0 ); auto. Qed. - + Lemma iter_inv: forall P l, P zero -> @@ -45,14 +45,14 @@ Lemma iter_inv: intros P l H H0; (elim l; simpl; auto). Qed. Variable next : A -> A. - + Fixpoint progression (m : A) (n : nat) {struct n} : list A := match n with 0 => nil | S n1 => cons m (progression (next m) n1) end. - + Fixpoint next_n (c : A) (n : nat) {struct n} : A := match n with 0 => c | S n1 => next_n (next c) n1 end. - + Theorem progression_app: forall a b n m, le m n -> @@ -64,9 +64,9 @@ intros m H a b n; case n; simpl; clear n. intros H1; absurd (0 < 1 + m); auto with arith. intros n H0 H1; apply f_equal2 with ( f := @cons A ); auto with arith. Qed. - + Let iter_progression := fun m n => iter (progression m n). - + Theorem iter_progression_app: forall a b n m, le m n -> @@ -76,11 +76,11 @@ Theorem iter_progression_app: intros a b n m H H0; unfold iter_progression; rewrite (progression_app a b n m); (try apply iter_app); auto. Qed. - + Theorem length_progression: forall z n, length (progression z n) = n. intros z n; generalize z; elim n; simpl; auto. Qed. - + End Iterator. Implicit Arguments iter [A B]. Implicit Arguments progression [A]. @@ -88,21 +88,21 @@ Implicit Arguments next_n [A]. Hint Unfold iter . Hint Unfold progression . Hint Unfold next_n . - + Theorem iter_ext: forall (A B : Set) zero (f1 : A -> B) f2 g l, (forall a, In a l -> f1 a = f2 a) -> iter zero f1 g l = iter zero f2 g l. intros A B zero f1 f2 g l; elim l; simpl; auto. intros a l0 H H0; apply f_equal2 with ( f := g ); auto. Qed. - + Theorem iter_map: forall (A B C : Set) zero (f : B -> C) g (k : A -> B) l, iter zero f g (map k l) = iter zero (fun x => f (k x)) g l. intros A B C zero f g k l; elim l; simpl; auto. intros; apply f_equal2 with ( f := g ); auto with arith. Qed. - + Theorem iter_comp: forall (A B : Set) zero (f1 f2 : A -> B) g l, (forall a, g a zero = a) -> @@ -115,7 +115,7 @@ intros a l0 H; rewrite <- H; (repeat rewrite <- g_trans). apply f_equal2 with ( f := g ); auto. (repeat rewrite g_trans); apply f_equal2 with ( f := g ); auto. Qed. - + Theorem iter_com: forall (A B : Set) zero (f : A -> A -> B) g l1 l2, (forall a, g a zero = a) -> @@ -142,7 +142,7 @@ apply f_equal2 with ( f := g ); auto. (repeat rewrite <- H0); auto. apply f_equal2 with ( f := g ); auto. Qed. - + Theorem iter_comp_const: forall (A B : Set) zero (f : A -> B) g k l, k zero = zero -> @@ -151,14 +151,14 @@ Theorem iter_comp_const: intros A B zero f g k l H H0; elim l; simpl; auto. intros a l0 H1; rewrite H0; apply f_equal2 with ( f := g ); auto. Qed. - + Lemma next_n_S: forall n m, next_n S n m = plus n m. intros n m; generalize n; elim m; clear n m; simpl; auto with arith. intros m H n; case n; simpl; auto with arith. rewrite H; auto with arith. intros n1; rewrite H; simpl; auto with arith. Qed. - + Theorem progression_S_le_init: forall n m p, In p (progression S n m) -> le n p. intros n m; generalize n; elim m; clear n m; simpl; auto. @@ -167,7 +167,7 @@ intros m H n p [H1|H1]; auto with arith. subst n; auto. apply le_S_n; auto with arith. Qed. - + Theorem progression_S_le_end: forall n m p, In p (progression S n m) -> lt p (n + m). intros n m; generalize n; elim m; clear n m; simpl; auto. diff --git a/coqprime/Coqprime/Lagrange.v b/coqprime/Coqprime/Lagrange.v index b35460bad..4765c76c4 100644 --- a/coqprime/Coqprime/Lagrange.v +++ b/coqprime/Coqprime/Lagrange.v @@ -7,12 +7,12 @@ (*************************************************************) (********************************************************************** - Lagrange.v - - Proof of Lagrange theorem: - the oder of a subgroup divides the order of a group - - Definition: lagrange + Lagrange.v + + Proof of Lagrange theorem: + the oder of a subgroup divides the order of a group + + Definition: lagrange **********************************************************************) Require Import List. Require Import UList. @@ -37,7 +37,7 @@ Variable H:(FGroup op). Hypothesis G_in_H: (incl G.(s) H.(s)). -(************************************** +(************************************** A group and a subgroup have the same neutral element **************************************) @@ -53,11 +53,11 @@ apply trans_equal with (op G.(e) H.(e)); sauto. eq_tac; sauto. Qed. -(************************************** +(************************************** The proof works like this. If G = {e, g1, g2, g3, .., gn} and {e, h1, h2, h3, ..., hm} we construct the list mkGH - {e, g1, g2, g3, ...., gn + {e, g1, g2, g3, ...., gn hi*e, hi * g1, hi * g2, ..., hi * gn if hi does not appear before .... hk*e, hk * g1, hk * g2, ..., hk * gn if hk does not appear before @@ -67,16 +67,16 @@ Qed. **************************************) Fixpoint mkList (base l: (list A)) { struct l} : (list A) := - match l with + match l with nil => nil | cons a l1 => let r1 := mkList base l1 in - if (In_dec A_dec a r1) then r1 else + if (In_dec A_dec a r1) then r1 else (map (op a) base) ++ r1 end. Definition mkGH := mkList G.(s) H.(s). -Theorem mkGH_length: divide (length G.(s)) (length mkGH). +Theorem mkGH_length: divide (length G.(s)) (length mkGH). unfold mkGH; elim H.(s); simpl. exists 0%nat; auto with arith. intros a l1 (c, H1); case (In_dec A_dec a (mkList G.(s) l1)); intros H2. @@ -161,11 +161,11 @@ assert (In a H.(s)); sauto; apply (H2 a); auto with datatypes. unfold mkGH; apply H1; auto with datatypes. Qed. -(************************************** +(************************************** Lagrange theorem **************************************) - -Theorem lagrange: (g_order G | (g_order H)). + +Theorem lagrange: (g_order G | (g_order H)). unfold g_order. rewrite Permutation.permutation_length with (l := H.(s)) (m:= mkGH). case mkGH_length; intros x H1; exists (Z_of_nat x). diff --git a/coqprime/Coqprime/ListAux.v b/coqprime/Coqprime/ListAux.v index c3c9602bd..2443faf52 100644 --- a/coqprime/Coqprime/ListAux.v +++ b/coqprime/Coqprime/ListAux.v @@ -7,9 +7,9 @@ (*************************************************************) (********************************************************************** - Aux.v - - Auxillary functions & Theorems + Aux.v + + Auxillary functions & Theorems **********************************************************************) Require Export List. Require Export Arith. @@ -17,18 +17,18 @@ Require Export Tactic. Require Import Inverse_Image. Require Import Wf_nat. -(************************************** +(************************************** Some properties on list operators: app, map,... **************************************) - + Section List. Variables (A : Set) (B : Set) (C : Set). Variable f : A -> B. -(************************************** - An induction theorem for list based on length +(************************************** + An induction theorem for list based on length **************************************) - + Theorem list_length_ind: forall (P : list A -> Prop), (forall (l1 : list A), @@ -40,7 +40,7 @@ intros P H l; apply wf_inverse_image with ( R := lt ); auto. apply lt_wf. Qed. - + Definition list_length_induction: forall (P : list A -> Set), (forall (l1 : list A), @@ -52,7 +52,7 @@ intros P H l; apply wf_inverse_image with ( R := lt ); auto. apply lt_wf. Qed. - + Theorem in_ex_app: forall (a : A) (l : list A), In a l -> (exists l1 : list A , exists l2 : list A , l = l1 ++ (a :: l2) ). @@ -66,20 +66,20 @@ rewrite Hl2; auto. Qed. (************************************** - Properties on app + Properties on app **************************************) - + Theorem length_app: forall (l1 l2 : list A), length (l1 ++ l2) = length l1 + length l2. intros l1; elim l1; simpl; auto. Qed. - + Theorem app_inv_head: forall (l1 l2 l3 : list A), l1 ++ l2 = l1 ++ l3 -> l2 = l3. intros l1; elim l1; simpl; auto. intros a l H l2 l3 H0; apply H; injection H0; auto. Qed. - + Theorem app_inv_tail: forall (l1 l2 l3 : list A), l2 ++ l1 = l3 ++ l1 -> l2 = l3. intros l1 l2; generalize l1; elim l2; clear l1 l2; simpl; auto. @@ -94,7 +94,7 @@ rewrite H1; auto with arith. simpl; intros b l0 H0; injection H0. intros H1 H2; rewrite H2, (H _ _ H1); auto. Qed. - + Theorem app_inv_app: forall l1 l2 l3 l4 a, l1 ++ l2 = l3 ++ (a :: l4) -> @@ -109,7 +109,7 @@ injection H0; auto. intros [l5 H1]. left; exists l5; injection H0; intros; subst; auto. Qed. - + Theorem app_inv_app2: forall l1 l2 l3 l4 a b, l1 ++ l2 = l3 ++ (a :: (b :: l4)) -> @@ -129,7 +129,7 @@ intros [l5 HH1]; left; exists l5; injection H0; intros; subst; auto. intros [H1|[H1 H2]]; auto. right; right; split; auto; injection H0; intros; subst; auto. Qed. - + Theorem same_length_ex: forall (a : A) l1 l2 l3, length (l1 ++ (a :: l2)) = length l3 -> @@ -148,10 +148,10 @@ exists (b :: l4); exists l5; exists b1; (repeat (simpl; split; auto)). rewrite HH3; auto. Qed. -(************************************** - Properties on map +(************************************** + Properties on map **************************************) - + Theorem in_map_inv: forall (b : B) (l : list A), In b (map f l) -> (exists a : A , In a l /\ b = f a ). @@ -161,7 +161,7 @@ intros a0 l0 H [H1|H1]; auto. exists a0; auto. case (H H1); intros a1 [H2 H3]; exists a1; auto. Qed. - + Theorem in_map_fst_inv: forall a (l : list (B * C)), In a (map (fst (B:=_)) l) -> (exists c , In (a, c) l ). @@ -171,16 +171,16 @@ intros a0 l0 H [H0|H0]; auto. exists (snd a0); left; rewrite <- H0; case a0; simpl; auto. case H; auto; intros l1 Hl1; exists l1; auto. Qed. - + Theorem length_map: forall l, length (map f l) = length l. intros l; elim l; simpl; auto. Qed. - + Theorem map_app: forall l1 l2, map f (l1 ++ l2) = map f l1 ++ map f l2. intros l; elim l; simpl; auto. intros a l0 H l2; rewrite H; auto. Qed. - + Theorem map_length_decompose: forall l1 l2 l3 l4, length l1 = length l2 -> @@ -197,10 +197,10 @@ intros H4 H5; split; auto. subst; auto. Qed. -(************************************** - Properties of flat_map +(************************************** + Properties of flat_map **************************************) - + Theorem in_flat_map: forall (l : list B) (f : B -> list C) a b, In a (f b) -> In b l -> In a (flat_map f l). @@ -209,7 +209,7 @@ intros a l0 H a0 b H0 [H1|H1]; apply in_or_app; auto. left; rewrite H1; auto. right; apply H with ( b := b ); auto. Qed. - + Theorem in_flat_map_ex: forall (l : list B) (f : B -> list C) a, In a (flat_map f l) -> (exists b , In b l /\ In a (f b) ). @@ -221,17 +221,17 @@ intros H1; case H with ( 1 := H1 ). intros b [H2 H3]; exists b; simpl; auto. Qed. -(************************************** - Properties of fold_left +(************************************** + Properties of fold_left **************************************) -Theorem fold_left_invol: +Theorem fold_left_invol: forall (f: A -> B -> A) (P: A -> Prop) l a, P a -> (forall x y, P x -> P (f x y)) -> P (fold_left f l a). intros f1 P l; elim l; simpl; auto. -Qed. +Qed. -Theorem fold_left_invol_in: +Theorem fold_left_invol_in: forall (f: A -> B -> A) (P: A -> Prop) l a b, In b l -> (forall x, P (f x b)) -> (forall x y, P x -> P (f x y)) -> P (fold_left f l a). @@ -245,17 +245,17 @@ Qed. End List. -(************************************** +(************************************** Propertie of list_prod **************************************) - + Theorem length_list_prod: forall (A : Set) (l1 l2 : list A), length (list_prod l1 l2) = length l1 * length l2. intros A l1 l2; elim l1; simpl; auto. intros a l H; rewrite length_app; rewrite length_map; rewrite H; auto. Qed. - + Theorem in_list_prod_inv: forall (A B : Set) a l1 l2, In a (list_prod l1 l2) -> diff --git a/coqprime/Coqprime/LucasLehmer.v b/coqprime/Coqprime/LucasLehmer.v index a0e3b8e46..6e3d218f2 100644 --- a/coqprime/Coqprime/LucasLehmer.v +++ b/coqprime/Coqprime/LucasLehmer.v @@ -7,11 +7,11 @@ (*************************************************************) (********************************************************************** - LucasLehamer.v - + LucasLehamer.v + Build the sequence for the primality test of Mersenne numbers - - Definition: LucasLehmer + + Definition: LucasLehmer **********************************************************************) Require Import ZArith. Require Import ZCAux. @@ -27,7 +27,7 @@ Require Import IGroup. Open Scope Z_scope. -(************************************** +(************************************** The seeds of the serie **************************************) @@ -43,13 +43,13 @@ Theorem w_mult_v : pmult w v = (1, 0). simpl; auto. Qed. -(************************************** +(************************************** Definition of the power function for pairs p^n **************************************) Definition ppow p n := match n with Zpos q => iter_pos _ (pmult p) (1, 0) q | _ => (1, 0) end. -(************************************** +(************************************** Some properties of ppow **************************************) @@ -66,7 +66,7 @@ Qed. Theorem ppow_op: forall a b p, iter_pos _ (pmult a) b p = pmult (iter_pos _ (pmult a) (1, 0) p) b. intros a b p; generalize b; elim p; simpl; auto; clear b p. intros p Rec b. -rewrite (Rec b). +rewrite (Rec b). try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos _ x y p)); auto. repeat rewrite pmult_assoc; auto. intros p Rec b. @@ -118,13 +118,13 @@ rewrite (fun x y => pmult_comm (iter_pos _ x y p3) p); auto. rewrite (pmult_assoc m); try apply pmult_comm; auto. Qed. -(************************************** +(************************************** We can now define our series of pairs s **************************************) Definition s n := pplus (ppow w (2 ^ n)) (ppow v (2 ^ n)). -(************************************** +(************************************** Some properties of s **************************************) @@ -149,7 +149,7 @@ repeat rewrite <- ppow_mult; auto with zarith. rewrite (pmult_comm v w); rewrite w_mult_v. rewrite ppow_1. repeat rewrite tpower_1. -rewrite pplus_comm; repeat rewrite <- pplus_assoc; +rewrite pplus_comm; repeat rewrite <- pplus_assoc; rewrite pplus_comm; repeat rewrite <- pplus_assoc. simpl; case (ppow (7, -4) (2 ^n)); simpl; intros z1 z2; eq_tac; auto with zarith. Qed. @@ -201,7 +201,7 @@ Section Lucas. Variable p: Z. -(************************************** +(************************************** Definition of the mersenne number **************************************) @@ -216,7 +216,7 @@ Qed. Hypothesis p_pos2: 2 < p. -(************************************** +(************************************** We suppose that the mersenne number divides s **************************************) @@ -224,7 +224,7 @@ Hypothesis Mp_divide_sn: (Mp | fst (s (p - 2))). Variable q: Z. -(************************************** +(************************************** We take a divisor of Mp and shows that Mp <= q^2, hence Mp is prime **************************************) @@ -236,7 +236,7 @@ Theorem q_pos: 1 < q. apply Zlt_trans with (2 := q_pos2); auto with zarith. Qed. -(************************************** +(************************************** The definition of the groups of inversible pairs **************************************) @@ -285,18 +285,18 @@ intros a _; left; rewrite zpmult_0_l; auto with zarith. intros; discriminate. Qed. -(************************************** +(************************************** The power function zpow: a^n **************************************) -Definition zpow a := gpow a pgroup. +Definition zpow a := gpow a pgroup. -(************************************** +(************************************** Some properties of zpow **************************************) -Theorem zpow_def: - forall a b, In a pgroup.(FGroup.s) -> 0 <= b -> +Theorem zpow_def: + forall a b, In a pgroup.(FGroup.s) -> 0 <= b -> zpow a b = ((fst (ppow a b)) mod q, (snd (ppow a b)) mod q). generalize q_pos; intros HM. generalize q_pos2; intros HM2. @@ -362,7 +362,7 @@ rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith. unfold zpow; rewrite gpow_gpow; auto with zarith. generalize zpow_w_n_minus_1; unfold zpow; intros H1; rewrite H1; clear H1. simpl; unfold zpmult, pmult. -repeat (rewrite Zmult_0_l || rewrite Zmult_0_r || rewrite Zplus_0_l || +repeat (rewrite Zmult_0_l || rewrite Zmult_0_r || rewrite Zplus_0_l || rewrite Zplus_0_r || rewrite Zmult_1_r). eq_tac; auto. pattern (-1 mod q) at 1; rewrite <- (Zmod_mod (-1) q); auto with zarith. @@ -371,7 +371,7 @@ rewrite Zmod_small; auto with zarith. apply w_in_pgroup. Qed. -(************************************** +(************************************** As e = (1, 0), the previous equation implies that the order of the group divide 2^p **************************************) @@ -385,7 +385,7 @@ apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith. exact zpow_w_n. Qed. -(************************************** +(************************************** So it is less than equal **************************************) @@ -396,19 +396,19 @@ apply Zpower_gt_0; auto with zarith. apply e_order_divide_pow. Qed. -(************************************** +(************************************** So order(w) must be 2^q **************************************) Theorem e_order_eq_pow: exists q, (e_order P_dec w pgroup) = 2 ^ q. -case (Zdivide_power_2 (e_order P_dec w pgroup) 2 p); auto with zarith. +case (Zdivide_power_2 (e_order P_dec w pgroup) 2 p); auto with zarith. apply Zlt_le_weak; apply e_order_pos. apply prime_2. apply e_order_divide_pow; auto. intros x H; exists x; auto with zarith. Qed. -(************************************** +(************************************** Buth this q can only be p otherwise it would contradict w^2^(p -1) = (-1, 0) **************************************) @@ -449,7 +449,7 @@ apply (gpow_e_order_is_e _ P_dec _ w pgroup). apply w_in_pgroup. Qed. -(************************************** +(************************************** We have then the expected conclusion **************************************) @@ -483,7 +483,7 @@ Qed. End Lucas. -(************************************** +(************************************** We build the sequence in Z **************************************) @@ -494,7 +494,7 @@ Definition SS p := | _ => (Zmodd 4 n) end. -Theorem SS_aux_correct: +Theorem SS_aux_correct: forall p z1 z2 n, 0 <= n -> 0 < z1 -> z2 = fst (s n) mod z1 -> iter_pos _ (fun x => Zmodd (Zsquare x - 2) z1) z2 p = fst (s (n + Zpos p)) mod z1. intros p; pattern p; apply Pind. @@ -558,7 +558,7 @@ pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp; auto with zarith. replace (p - 1 + 1) with p; auto with zarith. Qed. -(************************************** +(************************************** The test **************************************) @@ -594,4 +594,3 @@ Qed. Theorem prime524287: prime 524287. exact (LucasTest 19 (refl_equal _)). Qed. - diff --git a/coqprime/Coqprime/NatAux.v b/coqprime/Coqprime/NatAux.v index eab09150c..71d90cf9f 100644 --- a/coqprime/Coqprime/NatAux.v +++ b/coqprime/Coqprime/NatAux.v @@ -7,9 +7,9 @@ (*************************************************************) (********************************************************************** - Aux.v - - Auxillary functions & Theorems + Aux.v + + Auxillary functions & Theorems **********************************************************************) Require Export Arith. @@ -24,7 +24,7 @@ Qed. (************************************** - Definitions and properties of the power for nat + Definitions and properties of the power for nat **************************************) Fixpoint pow (n m: nat) {struct m} : nat := match m with O => 1%nat | (S m1) => (n * pow n m1)%nat end. @@ -56,7 +56,7 @@ apply pow_pos; auto with arith. Qed. (************************************ - Definition of the divisibility for nat + Definition of the divisibility for nat **************************************) Definition divide a b := exists c, b = a * c. diff --git a/coqprime/Coqprime/PGroup.v b/coqprime/Coqprime/PGroup.v index e9c1b2f47..5d8dc5d35 100644 --- a/coqprime/Coqprime/PGroup.v +++ b/coqprime/Coqprime/PGroup.v @@ -7,12 +7,12 @@ (*************************************************************) (********************************************************************** - PGroup.v - + PGroup.v + Build the group of pairs modulo needed for the theorem of lucas lehmer - - Definition: PGroup + + Definition: PGroup **********************************************************************) Require Import ZArith. Require Import Znumtheory. @@ -29,7 +29,7 @@ Open Scope Z_scope. Definition base := 3. -(************************************** +(************************************** Equality is decidable on pairs **************************************) @@ -42,13 +42,13 @@ 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 **************************************) @@ -62,13 +62,13 @@ 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 **************************************) @@ -109,7 +109,7 @@ intros p q r; case p; case q; case r; intros r1 r2 q1 q2 p1 p2; unfold pplus, pm 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. @@ -118,14 +118,14 @@ 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. + (a, Z_of_nat n) :: match n with O => nil | (S n1) => mkLine a n1 end. -(************************************** +(************************************** Some properties of mkLine **************************************) @@ -165,14 +165,14 @@ 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. + (mkLine (Z_of_nat n) m) ++ match n with O => nil | (S n1) => mkRect n1 m end. -(************************************** +(************************************** Some properties of mkRect **************************************) @@ -221,12 +221,12 @@ 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 **************************************) @@ -237,7 +237,7 @@ 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; +intros p q (H1, H2) (H3, H4); unfold mL; apply mkRect_in; rewrite inj_Zabs_nat; rewrite Zabs_eq; auto with zarith. Qed. @@ -251,13 +251,13 @@ 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 **************************************) @@ -329,8 +329,8 @@ 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 +(************************************** + We are now ready to build our group **************************************) Definition PGroup : (FGroup zpmult). diff --git a/coqprime/Coqprime/Permutation.v b/coqprime/Coqprime/Permutation.v index a06693f89..3a9b0860e 100644 --- a/coqprime/Coqprime/Permutation.v +++ b/coqprime/Coqprime/Permutation.v @@ -7,20 +7,20 @@ (*************************************************************) (********************************************************************** - Permutation.v - - Defintion and properties of permutations + Permutation.v + + Defintion and properties of permutations **********************************************************************) Require Export List. Require Export ListAux. - + Section permutation. Variable A : Set. -(************************************** +(************************************** Definition of permutations as sequences of adjacent transpositions **************************************) - + Inductive permutation : list A -> list A -> Prop := | permutation_nil : permutation nil nil | permutation_skip : @@ -33,10 +33,10 @@ Inductive permutation : list A -> list A -> Prop := permutation l1 l2 -> permutation l2 l3 -> permutation l1 l3. Hint Constructors permutation. -(************************************** +(************************************** Reflexivity **************************************) - + Theorem permutation_refl : forall l : list A, permutation l l. simple induction l. apply permutation_nil. @@ -45,10 +45,10 @@ apply permutation_skip with (1 := H). Qed. Hint Resolve permutation_refl. -(************************************** +(************************************** Symmetry **************************************) - + Theorem permutation_sym : forall l m : list A, permutation l m -> permutation m l. intros l1 l2 H'; elim H'. @@ -61,10 +61,10 @@ intros l1' l2' l3' H1 H2 H3 H4. apply permutation_trans with (1 := H4) (2 := H2). Qed. -(************************************** +(************************************** Compatibility with list length **************************************) - + Theorem permutation_length : forall l m : list A, permutation l m -> length l = length m. intros l m H'; elim H'; simpl in |- *; auto. @@ -72,20 +72,20 @@ intros l1 l2 l3 H'0 H'1 H'2 H'3. rewrite <- H'3; auto. Qed. -(************************************** +(************************************** A permutation of the nil list is the nil list **************************************) - + Theorem permutation_nil_inv : forall l : list A, permutation l nil -> l = nil. intros l H; generalize (permutation_length _ _ H); case l; simpl in |- *; auto. intros; discriminate. Qed. - -(************************************** + +(************************************** A permutation of the singleton list is the singleton list **************************************) - + Let permutation_one_inv_aux : forall l1 l2 : list A, permutation l1 l2 -> forall a : A, l1 = a :: nil -> l2 = a :: nil. @@ -101,19 +101,19 @@ Theorem permutation_one_inv : intros a l H; apply permutation_one_inv_aux with (l1 := a :: nil); auto. Qed. -(************************************** +(************************************** Compatibility with the belonging **************************************) - + Theorem permutation_in : forall (a : A) (l m : list A), permutation l m -> In a l -> In a m. intros a l m H; elim H; simpl in |- *; auto; intuition. Qed. -(************************************** +(************************************** Compatibility with the append function **************************************) - + Theorem permutation_app_comp : forall l1 l2 l3 l4, permutation l1 l2 -> permutation l3 l4 -> permutation (l1 ++ l3) (l2 ++ l4). @@ -128,10 +128,10 @@ apply permutation_trans with (l2 ++ l4); auto. Qed. Hint Resolve permutation_app_comp. -(************************************** +(************************************** Swap two sublists **************************************) - + Theorem permutation_app_swap : forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1). intros l1; elim l1; auto. @@ -152,10 +152,10 @@ apply (app_ass l2 (a :: nil) l). apply (app_ass l2 (a :: nil) l). Qed. -(************************************** +(************************************** A transposition is a permutation **************************************) - + Theorem permutation_transposition : forall a b l1 l2 l3, permutation (l1 ++ a :: l2 ++ b :: l3) (l1 ++ b :: l2 ++ a :: l3). @@ -173,10 +173,10 @@ apply permutation_app_comp; auto. apply permutation_app_swap; auto. Qed. -(************************************** +(************************************** An element of a list can be put on top of the list to get a permutation **************************************) - + Theorem in_permutation_ex : forall a l, In a l -> exists l1 : list A, permutation (a :: l1) l. intros a l; elim l; simpl in |- *; auto. @@ -186,8 +186,8 @@ exists l0; rewrite H0; auto. case H; auto; intros l1 Hl1; exists (a0 :: l1). apply permutation_trans with (a0 :: a :: l1); auto. Qed. - -(************************************** + +(************************************** A permutation of a cons can be inverted **************************************) @@ -232,7 +232,7 @@ intros l6 (l7, (Hl3, Hl4)). exists l6; exists l7; split; auto. apply permutation_trans with (1 := Hl2); auto. Qed. - + Theorem permutation_cons_ex : forall (a : A) (l1 l2 : list A), permutation (a :: l1) l2 -> @@ -242,10 +242,10 @@ intros a l1 l2 H. apply (permutation_cons_ex_aux a (a :: l1) l2 H nil l1); simpl in |- *; auto. Qed. -(************************************** +(************************************** A permutation can be simply inverted if the two list starts with a cons **************************************) - + Theorem permutation_inv : forall (a : A) (l1 l2 : list A), permutation (a :: l1) (a :: l2) -> permutation l1 l2. @@ -260,11 +260,11 @@ apply permutation_skip; apply permutation_app_swap. apply (permutation_app_swap (a0 :: l4) l5). Qed. -(************************************** - Take a list and return tle list of all pairs of an element of the +(************************************** + Take a list and return tle list of all pairs of an element of the list and the remaining list **************************************) - + Fixpoint split_one (l : list A) : list (A * list A) := match l with | nil => nil (A:=A * list A) @@ -273,10 +273,10 @@ Fixpoint split_one (l : list A) : list (A * list A) := :: map (fun p : A * list A => (fst p, a :: snd p)) (split_one l1) end. -(************************************** +(************************************** The pairs of the list are a permutation **************************************) - + Theorem split_one_permutation : forall (a : A) (l1 l2 : list A), In (a, l1) (split_one l2) -> permutation (a :: l1) l2. @@ -294,10 +294,10 @@ apply H2; auto. case a1; simpl in |- *; auto. Qed. -(************************************** +(************************************** All elements of the list are there **************************************) - + Theorem split_one_in_ex : forall (a : A) (l1 : list A), In a l1 -> exists l2 : list A, In (a, l2) (split_one l1). @@ -312,10 +312,10 @@ apply auto. Qed. -(************************************** +(************************************** An auxillary function to generate all permutations **************************************) - + Fixpoint all_permutations_aux (l : list A) (n : nat) {struct n} : list (list A) := match n with @@ -326,13 +326,13 @@ Fixpoint all_permutations_aux (l : list A) (n : nat) {struct n} : map (cons (fst p)) (all_permutations_aux (snd p) n1)) ( split_one l) end. -(************************************** +(************************************** Generate all the permutations **************************************) - + Definition all_permutations (l : list A) := all_permutations_aux l (length l). - -(************************************** + +(************************************** All the elements of the list are permutations **************************************) @@ -361,14 +361,14 @@ apply permutation_length; auto. apply permutation_sym; apply split_one_permutation; auto. apply split_one_permutation; auto. Qed. - + Theorem all_permutations_permutation : forall l1 l2 : list A, In l1 (all_permutations l2) -> permutation l1 l2. intros l1 l2 H; apply all_permutations_aux_permutation with (n := length l2); auto. Qed. - -(************************************** + +(************************************** A permutation is in the list **************************************) @@ -399,17 +399,17 @@ apply permutation_inv with (a := a1). apply permutation_trans with (1 := H2). apply permutation_sym; apply split_one_permutation; auto. Qed. - + Theorem permutation_all_permutations : forall l1 l2 : list A, permutation l1 l2 -> In l1 (all_permutations l2). intros l1 l2 H; unfold all_permutations in |- *; apply permutation_all_permutations_aux; auto. Qed. -(************************************** +(************************************** Permutation is decidable **************************************) - + Definition permutation_dec : (forall a b : A, {a = b} + {a <> b}) -> forall l1 l2 : list A, {permutation l1 l2} + {~ permutation l1 l2}. @@ -418,10 +418,10 @@ case (In_dec (list_eq_dec H) l1 (all_permutations l2)). intros i; left; apply all_permutations_permutation; auto. intros i; right; contradict i; apply permutation_all_permutations; auto. Defined. - + End permutation. -(************************************** +(************************************** Hints **************************************) @@ -430,7 +430,7 @@ Hint Resolve permutation_refl. Hint Resolve permutation_app_comp. Hint Resolve permutation_app_swap. -(************************************** +(************************************** Implicits **************************************) @@ -439,10 +439,10 @@ Implicit Arguments split_one [A]. Implicit Arguments all_permutations [A]. Implicit Arguments permutation_dec [A]. -(************************************** +(************************************** Permutation is compatible with map **************************************) - + Theorem permutation_map : forall (A B : Set) (f : A -> B) l1 l2, permutation l1 l2 -> permutation (map f l1) (map f l2). @@ -450,8 +450,8 @@ intros A B f l1 l2 H; elim H; simpl in |- *; auto. intros l0 l3 l4 H0 H1 H2 H3; apply permutation_trans with (2 := H3); auto. Qed. Hint Resolve permutation_map. - -(************************************** + +(************************************** Permutation of a map can be inverted *************************************) @@ -482,7 +482,7 @@ case H2 with (1 := HH2); auto. intros l5 (HH3, HH4); exists l5; split; auto. apply permutation_trans with (1 := HH3); auto. Qed. - + Theorem permutation_map_ex : forall (A B : Set) (f : A -> B) l1 l2, permutation (map f l1) l2 -> @@ -491,10 +491,10 @@ intros A0 B f l1 l2 H; apply permutation_map_ex_aux with (l1 := map f l1); auto. Qed. -(************************************** +(************************************** Permutation is compatible with flat_map **************************************) - + Theorem permutation_flat_map : forall (A B : Set) (f : A -> list B) l1 l2, permutation l1 l2 -> permutation (flat_map f l1) (flat_map f l2). diff --git a/coqprime/Coqprime/Pmod.v b/coqprime/Coqprime/Pmod.v index f64af48e3..3075b10f9 100644 --- a/coqprime/Coqprime/Pmod.v +++ b/coqprime/Coqprime/Pmod.v @@ -33,11 +33,11 @@ Fixpoint div_eucl (a b : positive) {struct a} : N * N := let (q, r) := div_eucl a' b in match q, r with | N0, N0 => (0%N, 0%N) (* Impossible *) - | N0, Npos r => + | N0, Npos r => if (xI r) ?< b then (0%N, Npos (xI r)) else (1%N,PminusN (xI r) b) | Npos q, N0 => if 1 ?< b then (Npos (xO q), 1%N) else (Npos (xI q), 0%N) - | Npos q, Npos r => + | Npos q, Npos r => if (xI r) ?< b then (Npos (xO q), Npos (xI r)) else (Npos (xI q),PminusN (xI r) b) end @@ -46,17 +46,17 @@ Infix "/" := div_eucl : P_scope. Open Scope Z_scope. Opaque Zmult. -Lemma div_eucl_spec : forall a b, +Lemma div_eucl_spec : forall a b, Zpos a = fst (a/b)%P * b + snd (a/b)%P /\ snd (a/b)%P < b. -Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega). +Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega). intros a b;generalize a;clear a;induction a;simpl;zsimpl. case IHa; destruct (a/b)%P as [q r]. case q; case r; simpl fst; simpl snd. rewrite Zmult_0_l; rewrite Zplus_0_r; intros HH; discriminate HH. intros p H; rewrite H; - match goal with - | [|- context [ ?xx ?< b ]] => + match goal with + | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto. @@ -65,16 +65,16 @@ Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega). rewrite PminusN_le... generalize H1; zsimpl; auto. intros p H; rewrite H; - match goal with - | [|- context [ ?xx ?< b ]] => + match goal with + | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring. ring_simplify. case (Zle_lt_or_eq _ _ H1); auto with zarith. intros p p1 H; rewrite H. - match goal with - | [|- context [ ?xx ?< b ]] => + match goal with + | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring. @@ -86,8 +86,8 @@ Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega). case q; case r; simpl fst; simpl snd. rewrite Zmult_0_l; rewrite Zplus_0_r; intros HH; discriminate HH. intros p H; rewrite H; - match goal with - | [|- context [ ?xx ?< b ]] => + match goal with + | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto. @@ -98,8 +98,8 @@ Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega). intros p H; rewrite H; simpl; intros H1; split; auto. zsimpl; ring. intros p p1 H; rewrite H. - match goal with - | [|- context [ ?xx ?< b ]] => + match goal with + | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring. @@ -107,8 +107,8 @@ Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega). generalize H1; zsimpl; auto. rewrite PminusN_le... generalize H1; zsimpl; auto. - match goal with - | [|- context [ ?xx ?< b ]] => + match goal with + | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl. @@ -130,15 +130,15 @@ Fixpoint Pmod (a b : positive) {struct a} : N := | N0 => 0%N | Npos r' => if (xO r') ?< b then Npos (xO r') - else PminusN (xO r') b + else PminusN (xO r') b end | xI a' => let r := Pmod a' b in match r with | N0 => if 1 ?< b then 1%N else 0%N - | Npos r' => + | Npos r' => if (xI r') ?< b then Npos (xI r') - else PminusN (xI r') b + else PminusN (xI r') b end end. @@ -151,8 +151,8 @@ Proof with auto. try (rewrite IHa; assert (H1 := div_eucl_spec a b); destruct (a/b) as [q r]; destruct q as [|q];destruct r as [|r];simpl in *; - match goal with - | [|- context [ ?xx ?< b ]] => + match goal with + | [|- context [ ?xx ?< b ]] => assert (H2 := is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end;simpl) ... @@ -175,17 +175,17 @@ Proof. destruct (a mod a)%P;auto with zarith. unfold Z_of_N;assert (H1:= Zlt_0_pos p0);intros (H2,H3);elimtype False;omega. Qed. - + Lemma mod_le_2r : forall (a b r: positive) (q:N), Zpos a = b*q + r -> b <= a -> r < b -> 2*r <= a. Proof. intros a b r q H0 H1 H2. - assert (H3:=Zlt_0_pos a). assert (H4:=Zlt_0_pos b). assert (H5:=Zlt_0_pos r). - destruct q as [|q]. rewrite Zmult_0_r in H0. elimtype False;omega. - assert (H6:=Zlt_0_pos q). unfold Z_of_N in H0. + assert (H3:=Zlt_0_pos a). assert (H4:=Zlt_0_pos b). assert (H5:=Zlt_0_pos r). + destruct q as [|q]. rewrite Zmult_0_r in H0. elimtype False;omega. + assert (H6:=Zlt_0_pos q). unfold Z_of_N in H0. assert (Zpos r = a - b*q). omega. simpl;zsimpl. pattern r at 2;rewrite H. - assert (b <= b * q). + assert (b <= b * q). pattern (Zpos b) at 1;rewrite <- (Zmult_1_r b). apply Zmult_le_compat;try omega. apply Zle_trans with (a - b * q + b). omega. @@ -197,7 +197,7 @@ Proof. intros a b r H;generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl; rewrite H;simpl;intros (H1,H2);omega. Qed. - + Lemma mod_le : forall a b r, a mod b = Npos r -> r <= b. Proof. intros a b r H;assert (H1:= mod_lt _ _ _ H);omega. Qed. @@ -205,7 +205,7 @@ Lemma mod_le_a : forall a b r, a mod b = r -> r <= a. Proof. intros a b r H;generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl; rewrite H;simpl;intros (H1,H2). - assert (0 <= fst (a / b) * b). + assert (0 <= fst (a / b) * b). destruct (fst (a / b));simpl;auto with zarith. auto with zarith. Qed. @@ -236,7 +236,7 @@ Fixpoint gcd_log2 (a b c:positive) {struct c}: option positive := end end. -Fixpoint egcd_log2 (a b c:positive) {struct c}: +Fixpoint egcd_log2 (a b c:positive) {struct c}: option (Z * Z * positive) := match a/b with | (_, N0) => Some (0, 1, b) @@ -244,14 +244,14 @@ Fixpoint egcd_log2 (a b c:positive) {struct c}: match b/r, c with | (_, N0), _ => Some (1, -q, r) | (q', Npos r'), xH => None - | (q', Npos r'), xO c' => + | (q', Npos r'), xO c' => match egcd_log2 r r' c' with None => None | Some (u', v', w') => let u := u' - v' * q' in Some (u, v' - q * u, w') end - | (q', Npos r'), xI c' => + | (q', Npos r'), xI c' => match egcd_log2 r r' c' with None => None | Some (u', v', w') => @@ -261,13 +261,13 @@ Fixpoint egcd_log2 (a b c:positive) {struct c}: end end. -Lemma egcd_gcd_log2: forall c a b, +Lemma egcd_gcd_log2: forall c a b, match egcd_log2 a b c, gcd_log2 a b c with None, None => True | Some (u,v,r), Some r' => r = r' | _, _ => False end. -induction c; simpl; auto; try +induction c; simpl; auto; try (intros a b; generalize (Pmod_div_eucl a b); case (a/b); simpl; intros q r1 H; subst; case (a mod b); auto; intros r; generalize (Pmod_div_eucl b r); case (b/r); simpl; @@ -276,27 +276,27 @@ induction c; simpl; auto; try intros ((p1,p2),p3); case gcd_log2; auto). Qed. -Ltac rw l := +Ltac rw l := match l with | (?r, ?r1) => match type of r with True => rewrite <- r1 | _ => rw r; rw r1 - end + end | ?r => rewrite r - end. + end. -Lemma egcd_log2_ok: forall c a b, +Lemma egcd_log2_ok: forall c a b, match egcd_log2 a b c with None => True | Some (u,v,r) => u * a + v * b = r end. induction c; simpl; auto; - intros a b; generalize (div_eucl_spec a b); case (a/b); + intros a b; generalize (div_eucl_spec a b); case (a/b); simpl fst; simpl snd; intros q r1; case r1; try (intros; ring); simpl; intros r (Hr1, Hr2); clear r1; - generalize (div_eucl_spec b r); case (b/r); - simpl fst; simpl snd; intros q' r1; case r1; + generalize (div_eucl_spec b r); case (b/r); + simpl fst; simpl snd; intros q' r1; case r1; try (intros; rewrite Hr1; ring); simpl; intros r' (Hr'1, Hr'2); clear r1; auto; generalize (IHc r r'); case egcd_log2; auto; @@ -305,11 +305,11 @@ induction c; simpl; auto; Qed. -Fixpoint log2 (a:positive) : positive := - match a with +Fixpoint log2 (a:positive) : positive := + match a with | xH => xH - | xO a => Psucc (log2 a) - | xI a => Psucc (log2 a) + | xO a => Psucc (log2 a) + | xI a => Psucc (log2 a) end. Lemma gcd_log2_1: forall a c, gcd_log2 a xH c = Some xH. @@ -335,18 +335,18 @@ Proof. assert (H1:= Zlt_0_pos (log2 a));elimtype False;omega. Qed. -Lemma mod_log2 : +Lemma mod_log2 : forall a b r:positive, a mod b = Npos r -> b <= a -> log2 r + 1 <= log2 a. Proof. intros; cut (log2 (xO r) <= log2 a). simpl;zsimpl;trivial. apply log2_Zle. - replace (Zpos (xO r)) with (2 * r)%Z;trivial. + replace (Zpos (xO r)) with (2 * r)%Z;trivial. generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl;rewrite H. rewrite Zmult_comm;intros [H1 H2];apply mod_le_2r with b (fst (a/b));trivial. Qed. Lemma gcd_log2_None_aux : - forall c a b, Zpos b <= Zpos a -> log2 b <= log2 c -> + forall c a b, Zpos b <= Zpos a -> log2 b <= log2 c -> gcd_log2 a b c <> None. Proof. induction c;simpl;intros; @@ -360,12 +360,12 @@ Proof. assert (H1 := Zlt_0_pos (log2 b));omega. rewrite (log2_1_inv _ H1) in Heq;rewrite mod1 in Heq;discriminate Heq. Qed. - + Lemma gcd_log2_None : forall a b, Zpos b <= Zpos a -> gcd_log2 a b b <> None. Proof. intros;apply gcd_log2_None_aux;auto with zarith. Qed. - + Lemma gcd_log2_Zle : - forall c1 c2 a b, log2 c1 <= log2 c2 -> + forall c1 c2 a b, log2 c1 <= log2 c2 -> gcd_log2 a b c1 <> None -> gcd_log2 a b c2 = gcd_log2 a b c1. Proof with zsimpl;trivial;try omega. induction c1;destruct c2;simpl;intros; @@ -386,8 +386,8 @@ Proof. intros a b c H1 H2; apply gcd_log2_Zle; trivial. apply gcd_log2_None; trivial. Qed. - -Lemma gcd_log2_mod0 : + +Lemma gcd_log2_mod0 : forall a b c, a mod b = N0 -> gcd_log2 a b c = Some b. Proof. intros a b c H;destruct c;simpl;rewrite H;trivial. Qed. @@ -405,7 +405,7 @@ Proof. Qed. Opaque Pmod. -Lemma gcd_log2_mod : forall a b, Zpos b <= Zpos a -> +Lemma gcd_log2_mod : forall a b, Zpos b <= Zpos a -> forall r, a mod b = Npos r -> gcd_log2 a b b = gcd_log2 b r r. Proof. intros a b;generalize a;clear a; assert (Hacc := Zwf_pos b). @@ -426,7 +426,7 @@ Proof. rewrite mod1 in Hmod;discriminate Hmod. Qed. -Lemma gcd_log2_xO_Zle : +Lemma gcd_log2_xO_Zle : forall a b, Zpos b <= Zpos a -> gcd_log2 a b (xO b) = gcd_log2 a b b. Proof. intros a b Hle;apply gcd_log2_Zle. @@ -434,7 +434,7 @@ Proof. apply gcd_log2_None_aux;auto with zarith. Qed. -Lemma gcd_log2_xO_Zlt : +Lemma gcd_log2_xO_Zlt : forall a b, Zpos a < Zpos b -> gcd_log2 a b (xO b) = gcd_log2 b a a. Proof. intros a b H;simpl. assert (Hlt := Zlt_0_pos a). @@ -445,7 +445,7 @@ Proof. assert (H2 := mod_lt _ _ _ H1). rewrite (gcd_log2_Zle_log a p b);auto with zarith. symmetry;apply gcd_log2_mod;auto with zarith. - apply log2_Zle. + apply log2_Zle. replace (Zpos p) with (Z_of_N (Npos p));trivial. apply mod_le_a with a;trivial. Qed. @@ -468,13 +468,13 @@ Qed. Definition gcd a b := match gcd_log2 a b (xO b) with - | Some p => p + | Some p => p | None => (* can not appear *) 1%positive end. Definition egcd a b := match egcd_log2 a b (xO b) with - | Some p => p + | Some p => p | None => (* can not appear *) (1,1,1%positive) end. @@ -499,15 +499,15 @@ Proof. destruct (Z_lt_le_dec a b) as [z|z]. pattern (gcd_log2 a b (xO b)) at 1; rewrite gcd_log2_xO_Zlt;trivial. rewrite (lt_mod _ _ z) in H;inversion H. - assert (r <= b). omega. + assert (r <= b). omega. generalize (gcd_log2_None _ _ H2). - destruct (gcd_log2 b r r);intros;trivial. + destruct (gcd_log2 b r r);intros;trivial. assert (log2 b <= log2 (xO b)). simpl;zsimpl;omega. pattern (gcd_log2 a b (xO b)) at 1; rewrite gcd_log2_Zle_log;auto with zarith. pattern (gcd_log2 a b b) at 1;rewrite (gcd_log2_mod _ _ z _ H). - assert (r <= b). omega. + assert (r <= b). omega. generalize (gcd_log2_None _ _ H3). - destruct (gcd_log2 b r r);intros;trivial. + destruct (gcd_log2 b r r);intros;trivial. Qed. Require Import ZArith. @@ -515,7 +515,7 @@ Require Import Znumtheory. Hint Rewrite Zpos_mult times_Zmult square_Zmult Psucc_Zplus: zmisc. -Ltac mauto := +Ltac mauto := trivial;autorewrite with zmisc;trivial;auto with zarith. Lemma gcd_Zis_gcd : forall a b:positive, (Zis_gcd b a (gcd b a)%P). @@ -534,13 +534,13 @@ Proof with mauto. apply Zis_gcd_sym;auto. Qed. -Lemma egcd_Zis_gcd : forall a b:positive, - let (uv,w) := egcd a b in - let (u,v) := uv in +Lemma egcd_Zis_gcd : forall a b:positive, + let (uv,w) := egcd a b in + let (u,v) := uv in u * a + v * b = w /\ (Zis_gcd b a w). Proof with mauto. intros a b; unfold egcd. - generalize (egcd_log2_ok (xO b) a b) (egcd_gcd_log2 (xO b) a b) + generalize (egcd_log2_ok (xO b) a b) (egcd_gcd_log2 (xO b) a b) (egcd_log2_x0 a b) (gcd_Zis_gcd b a); unfold egcd, gcd. case egcd_log2; try (intros ((u,v),w)); case gcd_log2; try (intros; match goal with H: False |- _ => case H end); @@ -548,7 +548,7 @@ Proof with mauto. intros; subst; split; try apply Zis_gcd_sym; auto. Qed. -Definition Zgcd a b := +Definition Zgcd a b := match a, b with | Z0, _ => b | _, Z0 => a @@ -563,8 +563,8 @@ Lemma Zgcd_is_gcd : forall x y, Zis_gcd x y (Zgcd x y). Proof. destruct x;destruct y;simpl. apply Zis_gcd_0. - apply Zis_gcd_sym;apply Zis_gcd_0. - apply Zis_gcd_sym;apply Zis_gcd_0. + apply Zis_gcd_sym;apply Zis_gcd_0. + apply Zis_gcd_sym;apply Zis_gcd_0. apply Zis_gcd_0. apply gcd_Zis_gcd. apply Zis_gcd_sym;apply Zis_gcd_minus;simpl;apply gcd_Zis_gcd. @@ -573,24 +573,24 @@ Proof. apply Zis_gcd_minus;apply Zis_gcd_minus;simpl;apply gcd_Zis_gcd. Qed. -Definition Zegcd a b := +Definition Zegcd a b := match a, b with | Z0, Z0 => (0,0,0) | Zpos _, Z0 => (1,0,a) | Zneg _, Z0 => (-1,0,-a) | Z0, Zpos _ => (0,1,b) | Z0, Zneg _ => (0,-1,-b) - | Zpos a, Zneg b => + | Zpos a, Zneg b => match egcd a b with (u,v,w) => (u,-v, Zpos w) end | Zneg a, Zpos b => match egcd a b with (u,v,w) => (-u,v, Zpos w) end - | Zpos a, Zpos b => + | Zpos a, Zpos b => match egcd a b with (u,v,w) => (u,v, Zpos w) end - | Zneg a, Zneg b => + | Zneg a, Zneg b => match egcd a b with (u,v,w) => (-u,-v, Zpos w) end end. -Lemma Zegcd_is_egcd : forall x y, +Lemma Zegcd_is_egcd : forall x y, match Zegcd x y with (u,v,w) => u * x + v * y = w /\ Zis_gcd x y w /\ 0 <= w end. @@ -604,11 +604,11 @@ Proof. try (rewrite zx0; apply Zis_gcd_minus; try rewrite zx1; auto; apply Zis_gcd_minus; try rewrite zx1; simpl; auto); try apply Zis_gcd_0; try (apply Zis_gcd_sym;apply Zis_gcd_0); - generalize (egcd_Zis_gcd p p0); case egcd; intros (u,v) w (H1, H2); + generalize (egcd_Zis_gcd p p0); case egcd; intros (u,v) w (H1, H2); split; repeat rewrite zx0; try (rewrite <- H1; ring); auto; (split; [idtac | red; intros; discriminate]). apply Zis_gcd_sym; auto. - apply Zis_gcd_sym; apply Zis_gcd_minus; rw zx1; + apply Zis_gcd_sym; apply Zis_gcd_minus; rw zx1; apply Zis_gcd_sym; auto. apply Zis_gcd_minus; rw zx1; auto. apply Zis_gcd_minus; rw zx1; auto. diff --git a/coqprime/Coqprime/Pocklington.v b/coqprime/Coqprime/Pocklington.v index 9871cd3e6..09c0b901c 100644 --- a/coqprime/Coqprime/Pocklington.v +++ b/coqprime/Coqprime/Pocklington.v @@ -12,14 +12,14 @@ Require Import Tactic. Require Import ZCAux. Require Import Zp. Require Import FGroup. -Require Import EGroup. +Require Import EGroup. Require Import Euler. Open Scope Z_scope. -Theorem Pocklington: -forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> - (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> +Theorem Pocklington: +forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> + (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> forall n, prime n -> (n | N) -> n mod F1 = 1. intros N F1 R1 HF1 HR1 Neq Rec n Hn H. assert (HN: 1 < N). @@ -73,9 +73,9 @@ apply Zdivide_trans with (1:= HiF1); rewrite Neq; apply Zdivide_factor_r. apply Zorder_div; auto. Qed. -Theorem PocklingtonCorollary1: +Theorem PocklingtonCorollary1: forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> N < F1 * F1 -> - (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> + (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> prime N. intros N F1 R1 H H1 H2 H3 H4; case (prime_dec N); intros H5; auto. assert (HN: 1 < N). @@ -93,9 +93,9 @@ apply Pocklington with (R1 := R1) (4 := H4); auto. apply Zlt_square_mult_inv; auto with zarith. Qed. -Theorem PocklingtonCorollary2: -forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> - (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> +Theorem PocklingtonCorollary2: +forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> + (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> forall n, 0 <= n -> (n | N) -> n mod F1 = 1. intros N F1 R1 H1 H2 H3 H4 n H5; pattern n; apply prime_induction; auto. assert (HN: 1 < N). @@ -114,9 +114,9 @@ Qed. Definition isSquare x := exists y, x = y * y. -Theorem PocklingtonExtra: +Theorem PocklingtonExtra: forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> Zeven F1 -> Zodd R1 -> - (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> + (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> forall m, 1 <= m -> (forall l, 1 <= l < m -> ~((l * F1 + 1) | N)) -> let s := (R1 / (2 * F1)) in let r := (R1 mod (2 * F1)) in @@ -186,7 +186,7 @@ case (Zeven_odd_dec (c + d)); auto; intros O1. contradict ER1; apply Zeven_not_Zodd; rewrite L6; rewrite <- Zplus_assoc; apply Zeven_plus_Zeven; auto. apply Zeven_mult_Zeven_r; auto. assert (L6_2: Zeven (c * d)). -case (Zeven_odd_dec c); intros HH1. +case (Zeven_odd_dec c); intros HH1. apply Zeven_mult_Zeven_l; auto. case (Zeven_odd_dec d); intros HH2. apply Zeven_mult_Zeven_r; auto. @@ -237,9 +237,9 @@ rewrite <- L10. replace (8 * s) with (4 * (2 * s)); auto with zarith; try rewrite L11; ring. Qed. -Theorem PocklingtonExtraCorollary: +Theorem PocklingtonExtraCorollary: forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> Zeven F1 -> Zodd R1 -> - (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> + (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> let s := (R1 / (2 * F1)) in let r := (R1 mod (2 * F1)) in N < 2 * F1 * F1 * F1 -> (s = 0 \/ ~ isSquare (r * r - 8 * s)) -> prime N. diff --git a/coqprime/Coqprime/PocklingtonCertificat.v b/coqprime/Coqprime/PocklingtonCertificat.v index ecf4462ed..9d3a032fd 100644 --- a/coqprime/Coqprime/PocklingtonCertificat.v +++ b/coqprime/Coqprime/PocklingtonCertificat.v @@ -34,7 +34,7 @@ Definition nprim sc := | Pock_certif n _ _ _ => n | SPock_certif n _ _ => n | Ell_certif n _ _ _ _ _ _ => n - + end. Open Scope positive_scope. @@ -51,11 +51,11 @@ Definition mkProd' (l:dec_prime) := fold_right (fun (k:positive*positive) r => times (fst k) r) 1%positive l. Definition mkProd_pred (l:dec_prime) := - fold_right (fun (k:positive*positive) r => + fold_right (fun (k:positive*positive) r => if ((snd k) ?= 1)%P then r else times (pow (fst k) (Ppred (snd k))) r) 1%positive l. -Definition mkProd (l:dec_prime) := +Definition mkProd (l:dec_prime) := fold_right (fun (k:positive*positive) r => times (pow (fst k) (snd k)) r) 1%positive l. (* [pow_mod a m n] return [a^m mod n] *) @@ -84,7 +84,7 @@ Definition Npow_mod a m n := (* [fold_pow_mod a [q1,_;...;qn,_]] b = a ^(q1*...*qn) mod b *) (* invariant a mod N = a *) -Definition fold_pow_mod a l n := +Definition fold_pow_mod a l n := fold_left (fun a' (qp:positive*positive) => Npow_mod a' (fst qp) n) l a. @@ -99,15 +99,15 @@ Definition times_mod x y n := Definition Npred_mod p n := match p with | N0 => Npos (Ppred n) - | Npos p => + | Npos p => if (p ?= 1) then N0 else Npos (Ppred p) - end. - + end. + Fixpoint all_pow_mod (prod a : N) (l:dec_prime) (n:positive) {struct l}: N*N := match l with | nil => (prod,a) - | (q,_) :: l => + | (q,_) :: l => let m := Npred_mod (fold_pow_mod a l n) n in all_pow_mod (times_mod prod m n) (Npow_mod a q n) l n end. @@ -117,19 +117,19 @@ Fixpoint pow_mod_pred (a:N) (l:dec_prime) (n:positive) {struct l} : N := | nil => a | (q,p)::l => if (p ?= 1) then pow_mod_pred a l n - else + else let a' := iter_pos _ (fun x => Npow_mod x q n) a (Ppred p) in pow_mod_pred a' l n end. Definition is_odd p := - match p with + match p with | xO _ => false | _ => true end. -Definition is_even p := - match p with +Definition is_even p := + match p with | xO _ => true | _ => false end. @@ -137,19 +137,19 @@ Definition is_even p := Definition check_s_r s r sqrt := match s with | N0 => true - | Npos p => + | Npos p => match (Zminus (square r) (xO (xO (xO p)))) with | Zpos x => let sqrt2 := square sqrt in let sqrt12 := square (Psucc sqrt) in - if sqrt2 ?< x then x ?< sqrt12 + if sqrt2 ?< x then x ?< sqrt12 else false | Zneg _ => true | Z0 => false end end. -Definition test_pock N a dec sqrt := +Definition test_pock N a dec sqrt := if (2 ?< N) then let Nm1 := Ppred N in let F1 := mkProd dec in @@ -165,8 +165,8 @@ Definition test_pock N a dec sqrt := match all_pow_mod 1%N A dec N with | (Npos p, Npos aNm1) => if (aNm1 ?= 1) then - if gcd p N ?= 1 then - if check_s_r s r sqrt then + if gcd p N ?= 1 then + if check_s_r s r sqrt then (N ?< (times ((times ((xO F1)+r+1) F1) + r) F1) + 1) else false else false @@ -176,10 +176,10 @@ Definition test_pock N a dec sqrt := | _ => false end else false - else false + else false else false | _=> false - end + end else false. Fixpoint is_in (p : positive) (lc : Certif) {struct lc} : bool := @@ -191,10 +191,10 @@ Fixpoint is_in (p : positive) (lc : Certif) {struct lc} : bool := Fixpoint all_in (lc : Certif) (lp : dec_prime) {struct lp} : bool := match lp with | nil => true - | (p,_) :: lp => - if all_in lc lp + | (p,_) :: lp => + if all_in lc lp then is_in p lc - else false + else false end. Definition gt2 n := @@ -212,7 +212,7 @@ Fixpoint test_Certif (lc : Certif) : bool := if gt2 p then match Mp p with | Zpos n' => - if (n ?= n') then + if (n ?= n') then match SS p with | Z0 => true | _ => false @@ -220,10 +220,10 @@ Fixpoint test_Certif (lc : Certif) : bool := else false | _ => false end - else false + else false else false | (Pock_certif n a dec sqrt) :: lc => - if test_pock n a dec sqrt then + if test_pock n a dec sqrt then if all_in lc dec then test_Certif lc else false else false (* Shoudl be done later to do it with Z *) @@ -231,9 +231,9 @@ Fixpoint test_Certif (lc : Certif) : bool := | (Ell_certif _ _ _ _ _ _ _):: lc => false end. -Lemma pos_eq_1_spec : +Lemma pos_eq_1_spec : forall p, - if (p ?= 1)%P then p = xH + if (p ?= 1)%P then p = xH else (1 < p). Proof. unfold Zlt;destruct p;simpl; auto; red;reflexivity. @@ -248,7 +248,7 @@ Lemma mod_unique : forall b q1 r1 q2 r2, Proof with auto with zarith. intros b q1 r1 q2 r2 H1 H2 H3. assert (r2 = (b * q1 + r1) -b*q2). rewrite H3;ring. - assert (b*(q2 - q1) = r1 - r2 ). rewrite H;ring. + assert (b*(q2 - q1) = r1 - r2 ). rewrite H;ring. assert (-b < r1 - r2 < b). omega. destruct (Ztrichotomy q1 q2) as [H5 | [H5 | H5]]. assert (q2 - q1 >= 1). omega. @@ -277,10 +277,10 @@ Qed. Hint Resolve Zpower_gt_0 Zlt_0_pos Zge_0_pos Zlt_le_weak Zge_0_pos_add: zmisc. -Hint Rewrite Zpos_mult Zpower_mult Zpower_1_r Zmod_mod Zpower_exp +Hint Rewrite Zpos_mult Zpower_mult Zpower_1_r Zmod_mod Zpower_exp times_Zmult square_Zmult Psucc_Zplus: zmisc. -Ltac mauto := +Ltac mauto := trivial;autorewrite with zmisc;trivial;auto with zmisc zarith. Lemma mod_lt : forall a (b:positive), a mod b < b. @@ -318,9 +318,9 @@ Proof. assert (b>0). mauto. unfold Zmod; assert (H1 := Z_div_mod a b H). destruct (Zdiv_eucl a b) as (q2, r2). - assert (H2 := div_eucl_spec a b). + assert (H2 := div_eucl_spec a b). assert (Z_of_N (fst (a / b)%P) = q2 /\ Z_of_N (snd (a/b)%P) = r2). - destruct H1;destruct H2. + destruct H1;destruct H2. apply mod_unique with b;mauto. split;mauto. unfold Zle;destruct (snd (a / b)%P);intro;discriminate. @@ -351,7 +351,7 @@ Proof. destruct (pow_mod a m n); mauto. rewrite (Zmult_mod (a^m)(a^m)); auto with zmisc. rewrite <- IHm. destruct (pow_mod a m n);simpl; mauto. -Qed. +Qed. Hint Rewrite pow_mod_spec Zpower_0 : zmisc. Lemma Npow_mod_spec : forall a p n, Z_of_N (Npow_mod a p n) = a^p mod n. @@ -360,7 +360,7 @@ Proof. Qed. Hint Rewrite Npow_mod_spec : zmisc. -Lemma iter_Npow_mod_spec : forall n q p a, +Lemma iter_Npow_mod_spec : forall n q p a, Z_of_N (iter_pos N (fun x : N => Npow_mod x q n) a p) = a^q^p mod n. Proof. induction p; mauto; intros; simpl Pos.iter; mauto; repeat rewrite IHp. @@ -370,28 +370,28 @@ Proof. Qed. Hint Rewrite iter_Npow_mod_spec : zmisc. -Lemma fold_pow_mod_spec : forall (n:positive) l (a:N), +Lemma fold_pow_mod_spec : forall (n:positive) l (a:N), Z_of_N a = a mod n -> - Z_of_N (fold_pow_mod a l n) = a^(mkProd' l) mod n. + Z_of_N (fold_pow_mod a l n) = a^(mkProd' l) mod n. Proof. - unfold fold_pow_mod;induction l; simpl fold_left; simpl mkProd'; + unfold fold_pow_mod;induction l; simpl fold_left; simpl mkProd'; intros; mauto. rewrite IHl; mauto. Qed. -Hint Rewrite fold_pow_mod_spec : zmisc. +Hint Rewrite fold_pow_mod_spec : zmisc. Lemma pow_mod_pred_spec : forall (n:positive) l (a:N), Z_of_N a = a mod n -> - Z_of_N (pow_mod_pred a l n) = a^(mkProd_pred l) mod n. + Z_of_N (pow_mod_pred a l n) = a^(mkProd_pred l) mod n. Proof. unfold pow_mod_pred;induction l;simpl mkProd;intros; mauto. destruct a as (q,p). simpl mkProd_pred. destruct (p ?= 1)%P; rewrite IHl; mauto; simpl. Qed. -Hint Rewrite pow_mod_pred_spec : zmisc. +Hint Rewrite pow_mod_pred_spec : zmisc. -Lemma mkProd_pred_mkProd : forall l, +Lemma mkProd_pred_mkProd : forall l, (mkProd_pred l)*(mkProd' l) = mkProd l. Proof. induction l;simpl;intros; mauto. @@ -418,7 +418,7 @@ Proof. assert ( 0 <= a mod b < b). apply Z_mod_lt; mauto. destruct (mod_unique b (a/b) (a mod b) 0 a H0 H); mauto. - rewrite <- Z_div_mod_eq; mauto. + rewrite <- Z_div_mod_eq; mauto. Qed. Lemma Npred_mod_spec : forall p n, Z_of_N p < Zpos n -> @@ -455,7 +455,7 @@ Qed. Lemma fold_aux : forall a N (n:positive) l prod, fold_left (fun (r : Z) (k : positive * positive) => - r * (a ^(N / fst k) - 1) mod n) l (prod mod n) mod n = + r * (a ^(N / fst k) - 1) mod n) l (prod mod n) mod n = fold_left (fun (r : Z) (k : positive * positive) => r * (a^(N / fst k) - 1)) l prod mod n. @@ -465,12 +465,12 @@ Qed. Lemma fst_all_pow_mod : forall (n a:positive) l (R:positive) (prod A :N), - 1 < n -> + 1 < n -> Z_of_N prod = prod mod n -> Z_of_N A = a^R mod n -> - Z_of_N (fst (all_pow_mod prod A l n)) = + Z_of_N (fst (all_pow_mod prod A l n)) = (fold_left - (fun r (k:positive*positive) => + (fun r (k:positive*positive) => (r * (a ^ (R* mkProd' l / (fst k)) - 1))) l prod) mod n. Proof. induction l;simpl;intros; mauto. @@ -483,23 +483,23 @@ Proof. rewrite Z_div_mult;auto with zmisc zarith. rewrite <- fold_aux. rewrite <- (fold_aux a (R * q * mkProd' l) n l (prod * (a ^ (R * mkProd' l) - 1)))... - assert ( ((prod * (A ^ mkProd' l - 1)) mod n) = + assert ( ((prod * (A ^ mkProd' l - 1)) mod n) = ((prod * ((a ^ R) ^ mkProd' l - 1)) mod n)). repeat rewrite (Zmult_mod prod);auto with zmisc. rewrite Zminus_mod;auto with zmisc. rewrite (Zminus_mod ((a ^ R) ^ mkProd' l));auto with zmisc. rewrite (Zpower_mod (a^R));auto with zmisc. rewrite H1; mauto. - rewrite H3; mauto. + rewrite H3; mauto. rewrite H1; mauto. Qed. Lemma is_odd_Zodd : forall p, is_odd p = true -> Zodd p. -Proof. +Proof. destruct p;intros;simpl;trivial;discriminate. Qed. Lemma is_even_Zeven : forall p, is_even p = true -> Zeven p. -Proof. +Proof. destruct p;intros;simpl;trivial;discriminate. Qed. @@ -513,12 +513,12 @@ Qed. Lemma le_square : forall x y, 0 <= x -> x <= y -> x*x <= y*y. Proof. intros; apply Zle_trans with (x*y). - apply Zmult_le_compat_l;trivial. + apply Zmult_le_compat_l;trivial. apply Zmult_le_compat_r;trivial. omega. Qed. -Lemma borned_square : forall x y, 0 <= x -> 0 <= y -> - x*x < y*y < (x+1)*(x+1) -> False. +Lemma borned_square : forall x y, 0 <= x -> 0 <= y -> + x*x < y*y < (x+1)*(x+1) -> False. Proof. intros;destruct (Z_lt_ge_dec x y) as [z|z]. assert (x + 1 <= y). omega. @@ -539,25 +539,25 @@ Qed. Ltac spec_dec := repeat match goal with | [H:(?x ?= ?y)%P = _ |- _] => - generalize (is_eq_spec x y); + generalize (is_eq_spec x y); rewrite H;clear H; autorewrite with zmisc; intro | [H:(?x ?< ?y)%P = _ |- _] => - generalize (is_lt_spec x y); + generalize (is_lt_spec x y); rewrite H; clear H; autorewrite with zmisc; intro end. Ltac elimif := match goal with - | [H: (if ?b then _ else _) = _ |- _] => + | [H: (if ?b then _ else _) = _ |- _] => let H1 := fresh "H" in (CaseEq b;intros H1; rewrite H1 in H; try discriminate H); elimif | _ => spec_dec end. -Lemma check_s_r_correct : forall s r sqrt, check_s_r s r sqrt = true -> +Lemma check_s_r_correct : forall s r sqrt, check_s_r s r sqrt = true -> Z_of_N s = 0 \/ ~ isSquare (r * r - 8 * s). Proof. unfold check_s_r;intros. @@ -566,7 +566,7 @@ Proof. rewrite H1 in H;try discriminate H. elimif. assert (Zpos (xO (xO (xO s))) = 8 * s). repeat rewrite Zpos_xO_add;ring. - generalizeclear H1; rewrite H2;mauto;intros. + generalizeclear H1; rewrite H2;mauto;intros. apply (not_square sqrt). simpl Z.of_N; rewrite H1;auto. intros (y,Heq). @@ -579,10 +579,10 @@ Proof. destruct y;discriminate Heq2. Qed. -Lemma in_mkProd_prime_div_in : - forall p:positive, prime p -> - forall (l:dec_prime), - (forall k, In k l -> prime (fst k)) -> +Lemma in_mkProd_prime_div_in : + forall p:positive, prime p -> + forall (l:dec_prime), + (forall k, In k l -> prime (fst k)) -> Zdivide p (mkProd l) -> exists n,In (p, n) l. Proof. induction l;simpl mkProd; simpl In; mauto. @@ -591,7 +591,7 @@ Proof. apply Zdivide_le; auto with zarith. intros. case prime_mult with (2 := H1); auto with zarith; intros H2. - exists (snd a);left. + exists (snd a);left. destruct a;simpl in *. assert (Zpos p = Zpos p0). rewrite (prime_div_Zpower_prime p1 p p0); mauto. @@ -616,7 +616,7 @@ Proof. rewrite Zmult_comm;apply Zis_gcd_for_euclid2;simpl in *. apply Zis_gcd_sym;auto. Qed. - + Lemma test_pock_correct : forall N a dec sqrt, (forall k, In k dec -> prime (Zpos (fst k))) -> test_pock N a dec sqrt = true -> @@ -632,10 +632,10 @@ Proof. generalize (div_eucl_spec R1 (xO (mkProd dec))); destruct ((R1 / xO (mkProd dec))%P) as (s,r'); mauto;intros (H7,H8). destruct r' as [|r];try discriminate H0. - generalize (fst_all_pow_mod N a dec (R1*mkProd_pred dec) 1 + generalize (fst_all_pow_mod N a dec (R1*mkProd_pred dec) 1 (pow_mod_pred (pow_mod a R1 N) dec N)). generalize (snd_all_pow_mod N dec 1 (pow_mod_pred (pow_mod a R1 N) dec N)). - destruct (all_pow_mod 1 (pow_mod_pred (pow_mod a R1 N) dec N) dec N) as + destruct (all_pow_mod 1 (pow_mod_pred (pow_mod a R1 N) dec N) dec N) as (prod,aNm1); mauto; simpl Z_of_N. destruct prod as [|prod];try discriminate H0. destruct aNm1 as [|aNm1];try discriminate H0;elimif. @@ -654,7 +654,7 @@ Proof. end; mauto. rewrite Zmod_small; mauto. assert (1 < mkProd dec). - assert (H14 := Zlt_0_pos (mkProd dec)). + assert (H14 := Zlt_0_pos (mkProd dec)). assert (1 <= mkProd dec); mauto. destruct (Zle_lt_or_eq _ _ H15); mauto. inversion H16. rewrite <- H18 in H5;discriminate H5. @@ -671,7 +671,7 @@ Proof. auto with zmisc zarith. rewrite H2; mauto. apply is_even_Zeven; auto. - apply is_odd_Zodd; auto. + apply is_odd_Zodd; auto. intros p; case p; clear p. intros HH; contradict HH. apply not_prime_0. @@ -691,7 +691,7 @@ Proof. revert H2; mauto; intro H2. rewrite <- H2. match goal with |- context [fold_left ?f _ _] => - apply (ListAux.fold_left_invol_in _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) + apply (ListAux.fold_left_invol_in _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) with (b := (p, q)); auto with zarith end. rewrite <- Heqr. @@ -702,7 +702,7 @@ Proof. apply check_s_r_correct with sqrt; mauto. Qed. -Lemma is_in_In : +Lemma is_in_In : forall p lc, is_in p lc = true -> exists c, In c lc /\ p = nprim c. Proof. induction lc;simpl;try (intros;discriminate). @@ -711,7 +711,7 @@ Proof. destruct (IHlc H) as [c [H1 H2]];exists c;auto. Qed. -Lemma all_in_In : +Lemma all_in_In : forall lc lp, all_in lc lp = true -> forall pq, In pq lp -> exists c, In c lc /\ fst pq = nprim c. Proof. @@ -721,8 +721,8 @@ Proof. rewrite <- H0;simpl;apply is_in_In;trivial. Qed. -Lemma test_Certif_In_Prime : - forall lc, test_Certif lc = true -> +Lemma test_Certif_In_Prime : + forall lc, test_Certif lc = true -> forall c, In c lc -> prime (nprim c). Proof with mauto. induction lc;simpl;intros. elim H0. @@ -732,10 +732,10 @@ Proof with mauto. CaseEq (Mp p);[intros Heq|intros N' Heq|intros N' Heq];rewrite Heq in H; try discriminate H. elimif. CaseEq (SS p);[intros Heq'|intros N'' Heq'|intros N'' Heq'];rewrite Heq' in H; - try discriminate H. + try discriminate H. rewrite H2;rewrite <- Heq. apply LucasLehmer;trivial. -(destruct p; try discriminate H1). +(destruct p; try discriminate H1). simpl in H1; generalize (is_lt_spec 2 p); rewrite H1; auto. elimif. apply (test_pock_correct N a d p); mauto. @@ -748,9 +748,8 @@ discriminate. discriminate. Qed. -Lemma Pocklington_refl : +Lemma Pocklington_refl : forall c lc, test_Certif (c::lc) = true -> prime (nprim c). Proof. intros c lc Heq;apply test_Certif_In_Prime with (c::lc);trivial;simpl;auto. Qed. - diff --git a/coqprime/Coqprime/Root.v b/coqprime/Coqprime/Root.v index 2f65790d6..0b432b788 100644 --- a/coqprime/Coqprime/Root.v +++ b/coqprime/Coqprime/Root.v @@ -7,9 +7,9 @@ (*************************************************************) (*********************************************************************** - Root.v - - Proof that a polynomial has at most n roots + Root.v + + Proof that a polynomial has at most n roots ************************************************************************) Require Import ZArith. Require Import List. @@ -30,11 +30,11 @@ Variable zero one: A. Let pol := list A. -Definition toA z := -match z with - Z0 => zero -| Zpos p => iter_pos _ (plus one) zero p -| Zneg p => op (iter_pos _ (plus one) zero p) +Definition toA z := +match z with + Z0 => zero +| Zpos p => iter_pos _ (plus one) zero p +| Zneg p => op (iter_pos _ (plus one) zero p) end. Fixpoint eval (p: pol) (x: A) {struct p} : A := @@ -47,8 +47,8 @@ Fixpoint div (p: pol) (x: A) {struct p} : pol * A := match p with nil => (nil, zero) | a::nil => (nil, a) -| a::p1 => - (snd (div p1 x)::fst (div p1 x), +| a::p1 => + (snd (div p1 x)::fst (div p1 x), (plus a (mult x (snd (div p1 x))))) end. @@ -82,7 +82,7 @@ simpl; intuition. intros a2 p2 Rec Hi; split. case Rec; auto with datatypes. intros H H1 i. -replace (In i (fst (div (a1 :: a2 :: p2) a))) with +replace (In i (fst (div (a1 :: a2 :: p2) a))) with (snd (div (a2::p2) a) = i \/ In i (fst (div (a2::p2) a))); auto. intros [Hi1 | Hi1]; auto. rewrite <- Hi1; auto. @@ -93,13 +93,13 @@ case Rec; auto with datatypes. Qed. -Theorem div_correct: +Theorem div_correct: forall p x y, P x -> P y -> (forall i, In i p -> P i) -> eval p y = plus (mult (eval (fst (div p x)) y) (plus y (op x))) (snd (div p x)). intros p x y; elim p; simpl. intros; rewrite mult_zero; try rewrite plus_zero; auto. intros a l; case l; simpl; auto. intros _ px py pa; rewrite (fun x => mult_comm x zero); repeat rewrite mult_zero; try apply plus_comm; auto. -intros a1 l1. +intros a1 l1. generalize (div_P (a1::l1) x); simpl. match goal with |- context[fst ?A] => case A end; simpl. intros q r Hd Rec px py pi. @@ -117,7 +117,7 @@ repeat rewrite mult_plus_distr; auto. repeat (rewrite (fun x y => (mult_comm (plus x y))) || rewrite mult_plus_distr); auto. rewrite (fun x => (plus_comm x (mult y r))); auto. repeat rewrite plus_assoc; try apply f_equal2 with (f := plus); auto. -2: repeat rewrite mult_assoc; try rewrite (fun y => mult_comm y (op x)); +2: repeat rewrite mult_assoc; try rewrite (fun y => mult_comm y (op x)); repeat rewrite mult_assoc; auto. rewrite (fun z => (plus_comm z (mult (op x) r))); auto. repeat rewrite plus_assoc; try apply f_equal2 with (f := plus); auto. @@ -127,7 +127,7 @@ rewrite (plus_comm (op x)); try rewrite plus_op_zero; auto. rewrite (fun x => mult_comm x zero); try rewrite mult_zero; try rewrite plus_zero; auto. Qed. -Theorem div_correct_factor: +Theorem div_correct_factor: forall p a, (forall i, In i p -> P i) -> P a -> eval p a = zero -> forall x, P x -> eval p x = (mult (eval (fst (div p a)) x) (plus x (op a))). intros p a Hp Ha H x px. @@ -143,14 +143,14 @@ Theorem length_decrease: forall p x, p <> nil -> (length (fst (div p x)) < lengt intros p x; elim p; simpl; auto. intros H1; case H1; auto. intros a l; case l; simpl; auto. -intros a1 l1. +intros a1 l1. match goal with |- context[fst ?A] => case A end; simpl; auto with zarith. intros p1 _ H H1. apply lt_n_S; apply H; intros; discriminate. Qed. -Theorem root_max: -forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) -> +Theorem root_max: +forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) -> (forall x, In x l -> eval p x = zero) -> (length p <= length l)%nat -> forall x, P x -> eval p x = zero. intros p l; generalize p; elim l; clear l p; simpl; auto. intros p; case p; simpl; auto. @@ -178,8 +178,8 @@ apply lt_n_Sm_le;apply lt_le_trans with (length (a1 :: p2)); auto with zarith. apply length_decrease; auto with datatypes. Qed. -Theorem root_max_is_zero: -forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) -> +Theorem root_max_is_zero: +forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) -> (forall x, In x l -> eval p x = zero) -> (length p <= length l)%nat -> forall x, (In x p) -> x = zero. intros p l; generalize p; elim l; clear l p; simpl; auto. intros p; case p; simpl; auto. @@ -236,4 +236,4 @@ apply sym_equal; apply plus_zero; auto. intros HH; case Hz; rewrite <- HH; auto. Qed. -End Root. \ No newline at end of file +End Root. diff --git a/coqprime/Coqprime/Tactic.v b/coqprime/Coqprime/Tactic.v index 93a244149..b0f8f4f28 100644 --- a/coqprime/Coqprime/Tactic.v +++ b/coqprime/Coqprime/Tactic.v @@ -8,19 +8,19 @@ (********************************************************************** - Tactic.v - Useful tactics + Tactic.v + Useful tactics **********************************************************************) (************************************** - A simple tactic to end a proof + A simple tactic to end a proof **************************************) Ltac finish := intros; auto; trivial; discriminate. (************************************** A tactic for proof by contradiction - with contradict H + with contradict H H: ~A |- B gives |- A H: ~A |- ~ B gives H: B |- A H: A |- B gives |- ~ A @@ -28,19 +28,19 @@ Ltac finish := intros; auto; trivial; discriminate. H: A |- ~ B gives H: A |- ~ A **************************************) -Ltac contradict name := +Ltac contradict name := let term := type of name in ( - match term with - (~_) => - match goal with + match term with + (~_) => + match goal with |- ~ _ => let x := fresh in - (intros x; case name; + (intros x; case name; generalize x; clear x name; intro name) | |- _ => case name; clear name end - | _ => - match goal with + | _ => + match goal with |- ~ _ => let x := fresh in (intros x; absurd term; [idtac | exact name]; generalize x; clear x name; @@ -60,10 +60,10 @@ Ltac case_eq name := (************************************** - A tactic to use f_equal? theorems + A tactic to use f_equal? theorems **************************************) -Ltac eq_tac := +Ltac eq_tac := match goal with |- (?g _ = ?g _) => apply f_equal with (f := g) | |- (?g ?X _ = ?g ?X _) => apply f_equal with (f := g X) @@ -77,7 +77,7 @@ Ltac eq_tac := | |- (?g _ _ _ _ _ = ?g _ _ _ _) => apply f_equal4 with (f := g) end. -(************************************** +(************************************** A stupid tactic that tries auto also after applying sym_equal **************************************) diff --git a/coqprime/Coqprime/UList.v b/coqprime/Coqprime/UList.v index 7b9d982ea..7dbd8562d 100644 --- a/coqprime/Coqprime/UList.v +++ b/coqprime/Coqprime/UList.v @@ -7,33 +7,33 @@ (*************************************************************) (*********************************************************************** - UList.v - - Definition of list with distinct elements - - Definition: ulist + UList.v + + Definition of list with distinct elements + + Definition: ulist ************************************************************************) Require Import List. Require Import Arith. Require Import Permutation. Require Import ListSet. - + Section UniqueList. Variable A : Set. Variable eqA_dec : forall (a b : A), ({ a = b }) + ({ a <> b }). (* A list is unique if there is not twice the same element in the list *) - + Inductive ulist : list A -> Prop := ulist_nil: ulist nil | ulist_cons: forall a l, ~ In a l -> ulist l -> ulist (a :: l) . Hint Constructors ulist . (* Inversion theorem *) - + Theorem ulist_inv: forall a l, ulist (a :: l) -> ulist l. intros a l H; inversion H; auto. Qed. (* The append of two unique list is unique if the list are distinct *) - + Theorem ulist_app: forall l1 l2, ulist l1 -> @@ -48,7 +48,7 @@ apply ulist_inv with ( 1 := H0 ); auto. intros a0 H3 H4; apply (H2 a0); auto. Qed. (* Iinversion theorem the appended list *) - + Theorem ulist_app_inv: forall l1 l2 (a : A), ulist (l1 ++ l2) -> In a l1 -> In a l2 -> False. intros l1; elim l1; simpl; auto. @@ -59,7 +59,7 @@ apply (H l2 a0); auto. apply ulist_inv with ( 1 := H0 ); auto. Qed. (* Iinversion theorem the appended list *) - + Theorem ulist_app_inv_l: forall (l1 l2 : list A), ulist (l1 ++ l2) -> ulist l1. intros l1; elim l1; simpl; auto. intros a l H l2 H0. @@ -68,13 +68,13 @@ intros H5; case iH2; auto with datatypes. apply H with l2; auto. Qed. (* Iinversion theorem the appended list *) - + Theorem ulist_app_inv_r: forall (l1 l2 : list A), ulist (l1 ++ l2) -> ulist l2. intros l1; elim l1; simpl; auto. intros a l H l2 H0; inversion H0; auto. Qed. (* Uniqueness is decidable *) - + Definition ulist_dec: forall l, ({ ulist l }) + ({ ~ ulist l }). intros l; elim l; auto. intros a l1 [H|H]; auto. @@ -83,7 +83,7 @@ right; red; intros H1; inversion H1; auto. right; intros H1; case H; apply ulist_inv with ( 1 := H1 ). Defined. (* Uniqueness is compatible with permutation *) - + Theorem ulist_perm: forall (l1 l2 : list A), permutation l1 l2 -> ulist l1 -> ulist l2. intros l1 l2 H; elim H; clear H l1 l2; simpl; auto. @@ -103,7 +103,7 @@ intros H; case iH1; simpl; auto. inversion_clear H0 as [|ia il iH1 iH2]; auto. inversion iH2; auto. Qed. - + Theorem ulist_def: forall l a, In a l -> ulist l -> ~ (exists l1 , permutation l (a :: (a :: l1)) ). @@ -112,7 +112,7 @@ absurd (ulist (a :: (a :: l1))); auto. intros H2; inversion_clear H2; simpl; auto with datatypes. apply ulist_perm with ( 1 := H1 ); auto. Qed. - + Theorem ulist_incl_permutation: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> (exists l3 , permutation l2 (l1 ++ l3) ). @@ -134,7 +134,7 @@ intros l4 H4; exists l4. apply permutation_trans with (a :: l3); auto. apply permutation_sym; auto. Qed. - + Theorem ulist_eq_permutation: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> length l1 = length l2 -> permutation l1 l2. @@ -150,7 +150,7 @@ replace l1 with (app l1 l3); auto. apply permutation_sym; auto. rewrite H5; rewrite app_nil_end; auto. Qed. - + Theorem ulist_incl_length: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> le (length l1) (length l2). @@ -166,8 +166,8 @@ intros l1 l2 H1 H2 H3 H4. apply ulist_eq_permutation; auto. apply le_antisym; apply ulist_incl_length; auto. Qed. - - + + Theorem ulist_incl_length_strict: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> ~ incl l2 l1 -> lt (length l1) (length l2). @@ -180,14 +180,14 @@ intros H2; case Hi0; auto. intros a HH; apply permutation_in with ( 1 := H2 ); auto. intros a l Hl0; (rewrite plus_comm; simpl; rewrite plus_comm; auto with arith). Qed. - + Theorem in_inv_dec: forall (a b : A) l, In a (cons b l) -> a = b \/ ~ a = b /\ In a l. intros a b l H; case (eqA_dec a b); auto; intros H1. right; split; auto; inversion H; auto. case H1; auto. Qed. - + Theorem in_ex_app_first: forall (a : A) (l : list A), In a l -> @@ -203,7 +203,7 @@ case H; auto; intros l1 [l2 [Hl2 Hl3]]; exists (a1 :: l1); exists l2; simpl; subst; auto. intros H4; case H4; auto. Qed. - + Theorem ulist_inv_ulist: forall (l : list A), ~ ulist l -> @@ -239,7 +239,7 @@ replace (l1 ++ (a1 :: (l2 ++ (a1 :: l3)))) with ((l1 ++ (a1 :: l2)) ++ (a1 :: l3)); auto with datatypes. (repeat (rewrite <- ass_app; simpl)); auto. Qed. - + Theorem incl_length_repetition: forall (l1 l2 : list A), incl l1 l2 -> @@ -253,11 +253,11 @@ intros l1 l2 H H0; apply ulist_inv_ulist. intros H1; absurd (le (length l1) (length l2)); auto with arith. apply ulist_incl_length; auto. Qed. - + End UniqueList. Implicit Arguments ulist [A]. Hint Constructors ulist . - + Theorem ulist_map: forall (A B : Set) (f : A -> B) l, (forall x y, (In x l) -> (In y l) -> f x = f y -> x = y) -> ulist l -> ulist (map f l). @@ -270,7 +270,7 @@ case in_map_inv with ( 1 := H1 ); auto with datatypes. intros b1 [Hb1 Hb2]. replace a1 with b1; auto with datatypes. Qed. - + Theorem ulist_list_prod: forall (A : Set) (l1 l2 : list A), ulist l1 -> ulist l2 -> ulist (list_prod l1 l2). diff --git a/coqprime/Coqprime/ZCAux.v b/coqprime/Coqprime/ZCAux.v index de03a2fe2..2da30c800 100644 --- a/coqprime/Coqprime/ZCAux.v +++ b/coqprime/Coqprime/ZCAux.v @@ -7,9 +7,9 @@ (*************************************************************) (********************************************************************** - ZCAux.v - - Auxillary functions & Theorems + ZCAux.v + + Auxillary functions & Theorems **********************************************************************) Require Import ArithRing. @@ -57,7 +57,7 @@ pattern q at 1; rewrite <- (Zmult_1_l q). apply Zmult_lt_compat_r; auto with zarith. Qed. -Theorem prime_induction: forall (P: Z -> Prop), P 0 -> P 1 -> (forall p q, prime p -> P q -> P (p * q)) -> forall p, 0 <= p -> P p. +Theorem prime_induction: forall (P: Z -> Prop), P 0 -> P 1 -> (forall p q, prime p -> P q -> P (p * q)) -> forall p, 0 <= p -> P p. intros P H H1 H2 p Hp. generalize Hp; pattern p; apply Z_lt_induction; auto; clear p Hp. intros p Rec Hp. @@ -94,13 +94,13 @@ ring. exists 0; repeat split; try rewrite Zpower_1_r; try rewrite Zpower_exp_0; auto with zarith. Qed. -Theorem prime_div_induction: +Theorem prime_div_induction: forall (P: Z -> Prop) n, 0 < n -> (P 1) -> - (forall p i, prime p -> 0 <= i -> (p^i | n) -> P (p^i)) -> - (forall p q, rel_prime p q -> P p -> P q -> P (p * q)) -> - forall m, 0 <= m -> (m | n) -> P m. + (forall p i, prime p -> 0 <= i -> (p^i | n) -> P (p^i)) -> + (forall p q, rel_prime p q -> P p -> P q -> P (p * q)) -> + forall m, 0 <= m -> (m | n) -> P m. intros P n P1 Hn H H1 m Hm. generalize Hm; pattern m; apply Z_lt_induction; auto; clear m Hm. intros m Rec Hm H2. @@ -119,7 +119,7 @@ case Zle_lt_or_eq with (1 := Hi); clear Hi; intros Hi. assert (Hpi: 0 < p ^ i). apply Zpower_gt_0; auto with zarith. apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. -rewrite (Z_div_exact_2 m (p ^ i)); auto with zarith. +rewrite (Z_div_exact_2 m (p ^ i)); auto with zarith. apply H1; auto with zarith. apply rel_prime_sym; apply rel_prime_Zpower_r; auto with zarith. apply rel_prime_sym. @@ -256,7 +256,7 @@ intros a b (H1, H2); apply Zle_trans with (a * b); auto with zarith. Qed. Theorem Zlt_square_mult_inv: forall a b, 0 <= a -> 0 <= b -> a * a < b * b -> a < b. -intros a b H1 H2 H3; case (Zle_or_lt b a); auto; intros H4; apply Zmult_lt_reg_r with a; +intros a b H1 H2 H3; case (Zle_or_lt b a); auto; intros H4; apply Zmult_lt_reg_r with a; contradict H3; apply Zle_not_lt; apply Zle_square_mult; auto. Qed. @@ -278,13 +278,13 @@ repeat rewrite Zpower_pos_is_exp; auto. repeat rewrite Rec; auto. replace (Zpower_pos a 1) with a; auto. 2: unfold Zpower_pos; simpl; auto with zarith. -repeat rewrite (fun x => (Zmult_mod x a)); auto. -rewrite (Zmult_mod (Zpower_pos a p)); auto. +repeat rewrite (fun x => (Zmult_mod x a)); auto. +rewrite (Zmult_mod (Zpower_pos a p)); auto. case (Zpower_pos a p mod n); auto. intros p Rec n H1; rewrite <- Pplus_diag; auto. repeat rewrite Zpower_pos_is_exp; auto. repeat rewrite Rec; auto. -rewrite (Zmult_mod (Zpower_pos a p)); auto. +rewrite (Zmult_mod (Zpower_pos a p)); auto. case (Zpower_pos a p mod n); auto. unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto with zarith. Qed. diff --git a/coqprime/Coqprime/ZCmisc.v b/coqprime/Coqprime/ZCmisc.v index c1bdacc63..67709a146 100644 --- a/coqprime/Coqprime/ZCmisc.v +++ b/coqprime/Coqprime/ZCmisc.v @@ -27,14 +27,14 @@ Proof. intros p;rewrite Zpos_xO;ring. Qed. Lemma Psucc_Zplus : forall p, Zpos (Psucc p) = p + 1. Proof. intros p;rewrite Zpos_succ_morphism;unfold Zsucc;trivial. Qed. -Hint Rewrite Zpos_xI_add Zpos_xO_add Pplus_carry_spec +Hint Rewrite Zpos_xI_add Zpos_xO_add Pplus_carry_spec Psucc_Zplus Zpos_plus : zmisc. Lemma Zlt_0_pos : forall p, 0 < Zpos p. Proof. unfold Zlt;trivial. Qed. - -Lemma Pminus_mask_carry_spec : forall p q, + +Lemma Pminus_mask_carry_spec : forall p q, Pminus_mask_carry p q = Pminus_mask p (Psucc q). Proof. intros p q;generalize q p;clear q p. @@ -48,17 +48,17 @@ Ltac zsimpl := autorewrite with zmisc. Ltac CaseEq t := generalize (refl_equal t);pattern t at -1;case t. Ltac generalizeclear H := generalize H;clear H. -Lemma Pminus_mask_spec : - forall p q, +Lemma Pminus_mask_spec : + forall p q, match Pminus_mask p q with | IsNul => Zpos p = Zpos q - | IsPos k => Zpos p = q + k + | IsPos k => Zpos p = q + k | IsNeq => p < q end. Proof with zsimpl;auto with zarith. induction p;destruct q;simpl;zsimpl; - match goal with - | [|- context [(Pminus_mask ?p1 ?q1)]] => + match goal with + | [|- context [(Pminus_mask ?p1 ?q1)]] => assert (H1 := IHp q1);destruct (Pminus_mask p1 q1) | _ => idtac end;simpl ... @@ -69,7 +69,7 @@ Proof with zsimpl;auto with zarith. assert (H:= Zlt_0_pos q) ... assert (H:= Zlt_0_pos q) ... Qed. -Definition PminusN x y := +Definition PminusN x y := match Pminus_mask x y with | IsPos k => Npos k | _ => N0 @@ -100,7 +100,7 @@ Definition is_lt (n m : positive) := end. Infix "?<" := is_lt (at level 70, no associativity) : P_scope. -Lemma is_lt_spec : forall n m, if n ?< m then (n < m)%Z else (m <= n)%Z. +Lemma is_lt_spec : forall n m, if n ?< m then (n < m)%Z else (m <= n)%Z. Proof. intros n m; unfold is_lt, Zlt, Zle, Zcompare. rewrite Pos.compare_antisym. @@ -113,7 +113,7 @@ Definition is_eq a b := | _ => false end. Infix "?=" := is_eq (at level 70, no associativity) : P_scope. - + Lemma is_eq_refl : forall n, n ?= n = true. Proof. intros n;unfold is_eq;rewrite Pos.compare_refl;trivial. Qed. @@ -123,14 +123,14 @@ Proof. destruct (n ?= m)%positive;trivial;try discriminate. Qed. -Lemma is_eq_spec_pos : forall n m, if n ?= m then n = m else m <> n. +Lemma is_eq_spec_pos : forall n m, if n ?= m then n = m else m <> n. Proof. intros n m; CaseEq (n ?= m);intro H. rewrite (is_eq_eq _ _ H);trivial. intro H1;rewrite H1 in H;rewrite is_eq_refl in H;discriminate H. Qed. -Lemma is_eq_spec : forall n m, if n ?= m then Zpos n = m else Zpos m <> n. +Lemma is_eq_spec : forall n m, if n ?= m then Zpos n = m else Zpos m <> n. Proof. intros n m; CaseEq (n ?= m);intro H. rewrite (is_eq_eq _ _ H);trivial. @@ -145,8 +145,8 @@ Definition is_Eq a b := | _, _ => false end. -Lemma is_Eq_spec : - forall n m, if is_Eq n m then Z_of_N n = m else Z_of_N m <> n. +Lemma is_Eq_spec : + forall n m, if is_Eq n m then Z_of_N n = m else Z_of_N m <> n. Proof. destruct n;destruct m;simpl;trivial;try (intro;discriminate). apply is_eq_spec. diff --git a/coqprime/Coqprime/ZProgression.v b/coqprime/Coqprime/ZProgression.v index 51ce91cdc..ec69df5a6 100644 --- a/coqprime/Coqprime/ZProgression.v +++ b/coqprime/Coqprime/ZProgression.v @@ -10,7 +10,7 @@ Require Export Iterator. Require Import ZArith. Require Export UList. Open Scope Z_scope. - + Theorem next_n_Z: forall n m, next_n Zsucc n m = n + Z_of_nat m. intros n m; generalize n; elim m; clear n m. intros n; simpl; auto with zarith. @@ -19,7 +19,7 @@ replace (n + Z_of_nat (S m)) with (Zsucc n + Z_of_nat m); auto with zarith. rewrite <- H; auto with zarith. rewrite inj_S; auto with zarith. Qed. - + Theorem Zprogression_end: forall n m, progression Zsucc n (S m) = @@ -33,7 +33,7 @@ replace (Zsucc n1 + Z_of_nat m1) with (n1 + Z_of_nat (S m1)); auto with zarith. replace (Z_of_nat (S m1)) with (1 + Z_of_nat m1); auto with zarith. rewrite inj_S; auto with zarith. Qed. - + Theorem Zprogression_pred_end: forall n m, progression Zpred n (S m) = @@ -47,7 +47,7 @@ replace (Zpred n1 - Z_of_nat m1) with (n1 - Z_of_nat (S m1)); auto with zarith. replace (Z_of_nat (S m1)) with (1 + Z_of_nat m1); auto with zarith. rewrite inj_S; auto with zarith. Qed. - + Theorem Zprogression_opp: forall n m, rev (progression Zsucc n m) = progression Zpred (n + Z_of_nat (pred m)) m. @@ -63,7 +63,7 @@ intros m1; replace (n + Z_of_nat (pred (S m1))) with (Zpred (n + Z_of_nat (S m1))); auto. rewrite inj_S; simpl; (unfold Zpred; unfold Zsucc); auto with zarith. Qed. - + Theorem Zprogression_le_init: forall n m p, In p (progression Zsucc n m) -> (n <= p). intros n m; generalize n; elim m; clear n m; simpl; auto. @@ -71,7 +71,7 @@ intros; contradiction. intros m H n p [H1|H1]; auto with zarith. generalize (H _ _ H1); auto with zarith. Qed. - + Theorem Zprogression_le_end: forall n m p, In p (progression Zsucc n m) -> (p < n + Z_of_nat m). intros n m; generalize n; elim m; clear n m; auto. @@ -84,14 +84,14 @@ apply Zplus_lt_compat_l; red; simpl; auto with zarith. apply Zlt_le_trans with (Zsucc n + Z_of_nat m); auto with zarith. rewrite inj_S; rewrite Zplus_succ_comm; auto with zarith. Qed. - + Theorem ulist_Zprogression: forall a n, ulist (progression Zsucc a n). intros a n; generalize a; elim n; clear a n; simpl; auto with zarith. intros n H1 a; apply ulist_cons; auto. intros H2; absurd (Zsucc a <= a); auto with zarith. apply Zprogression_le_init with ( 1 := H2 ). Qed. - + Theorem in_Zprogression: forall a b n, ( a <= b < a + Z_of_nat n ) -> In b (progression Zsucc a n). intros a b n; generalize a b; elim n; clear a b n; auto with zarith. diff --git a/coqprime/Coqprime/ZSum.v b/coqprime/Coqprime/ZSum.v index 3a7f14065..95a8f74a5 100644 --- a/coqprime/Coqprime/ZSum.v +++ b/coqprime/Coqprime/ZSum.v @@ -19,14 +19,14 @@ Require Import ZProgression. Open Scope Z_scope. (* Iterated Sum *) - + Definition Zsum := fun n m f => if Zle_bool n m then iter 0 f Zplus (progression Zsucc n (Zabs_nat ((1 + m) - n))) else iter 0 f Zplus (progression Zpred n (Zabs_nat ((1 + n) - m))). Hint Unfold Zsum . - + Lemma Zsum_nn: forall n f, Zsum n n f = f n. intros n f; unfold Zsum; rewrite Zle_bool_refl. replace ((1 + n) - n) with 1; auto with zarith. @@ -39,7 +39,7 @@ intros a1 l1 Hl1. apply permutation_trans with (cons a1 (rev l1)); auto. change (permutation (rev l1 ++ (a1 :: nil)) (app (cons a1 nil) (rev l1))); auto. Qed. - + Lemma Zsum_swap: forall (n m : Z) (f : Z -> Z), Zsum n m f = Zsum m n f. intros n m f; unfold Zsum. generalize (Zle_cases n m) (Zle_cases m n); case (Zle_bool n m); @@ -85,7 +85,7 @@ repeat rewrite <- plus_n_Sm; simpl; auto. intros p H3; contradict H3; auto with zarith. apply permutation_rev. Qed. - + Lemma Zsum_split_up: forall (n m p : Z) (f : Z -> Z), ( n <= m < p ) -> Zsum n p f = Zsum n m f + Zsum (m + 1) p f. @@ -128,20 +128,20 @@ apply inj_eq_rev; auto with zarith. rewrite inj_S; (repeat rewrite inj_Zabs_nat); auto with zarith. (repeat rewrite Zabs_eq); auto with zarith. Qed. - + Lemma Zsum_S_left: forall (n m : Z) (f : Z -> Z), n < m -> Zsum n m f = f n + Zsum (n + 1) m f. intros n m f H; rewrite (Zsum_split_up n n m f); auto with zarith. rewrite Zsum_nn; auto with zarith. Qed. - + Lemma Zsum_S_right: forall (n m : Z) (f : Z -> Z), n <= m -> Zsum n (m + 1) f = Zsum n m f + f (m + 1). intros n m f H; rewrite (Zsum_split_up n m (m + 1) f); auto with zarith. rewrite Zsum_nn; auto with zarith. Qed. - + Lemma Zsum_split_down: forall (n m p : Z) (f : Z -> Z), ( p < m <= n ) -> Zsum n p f = Zsum n m f + Zsum (m - 1) p f. @@ -191,13 +191,13 @@ Lemma Zsum_add: intros n m f g; unfold Zsum; case (Zle_bool n m); apply iter_comp; auto with zarith. Qed. - + Lemma Zsum_times: forall n m x f, x * Zsum n m f = Zsum n m (fun i=> x * f i). intros n m x f. unfold Zsum. case (Zle_bool n m); intros; apply iter_comp_const with (k := (fun y : Z => x * y)); auto with zarith. Qed. - + Lemma inv_Zsum: forall (P : Z -> Prop) (n m : Z) (f : Z -> Z), n <= m -> @@ -241,7 +241,7 @@ replace (Zpred (n + 1)) with (Zpred n + 1); auto with zarith. unfold Zpred; auto with zarith. exists (Zabs_nat ((1 + n) - m)); auto. Qed. - + Theorem Zsum_c: forall (c p q : Z), p <= q -> Zsum p q (fun x => c) = ((1 + q) - p) * c. intros c p q Hq; unfold Zsum. @@ -256,7 +256,7 @@ intros n H p0; replace (Z_of_nat (S n)) with (Z_of_nat n + 1); auto with zarith. simpl; rewrite H; ring. rewrite inj_S; auto with zarith. Qed. - + Theorem Zsum_Zsum_f: forall (i j k l : Z) (f : Z -> Z -> Z), i <= j -> @@ -266,7 +266,7 @@ Theorem Zsum_Zsum_f: intros; apply Zsum_ext; intros; auto with zarith. rewrite Zsum_S_right; auto with zarith. Qed. - + Theorem Zsum_com: forall (i j k l : Z) (f : Z -> Z -> Z), Zsum i j (fun x => Zsum k l (fun y => f x y)) = @@ -274,7 +274,7 @@ Theorem Zsum_com: intros; unfold Zsum; case (Zle_bool i j); case (Zle_bool k l); apply iter_com; auto with zarith. Qed. - + Theorem Zsum_le: forall (n m : Z) (f g : Z -> Z), n <= m -> @@ -301,7 +301,7 @@ forall (f g: Z -> Z) l, (forall a, In a l -> f a <= g a) -> iter 0 f Zplus l <= iter 0 g Zplus l. intros f g l; elim l; simpl; auto with zarith. Qed. - + Theorem Zsum_lt: forall n m f g, (forall x, n <= x -> x <= m -> f x <= g x) -> @@ -327,7 +327,7 @@ apply in_Zprogression. rewrite inj_Zabs_nat; auto with zarith. rewrite Zabs_eq; auto with zarith. Qed. - + Theorem Zsum_minus: forall n m f g, Zsum n m f - Zsum n m g = Zsum n m (fun x => f x - g x). intros n m f g; apply trans_equal with (Zsum n m f + (-1) * Zsum n m g); auto with zarith. diff --git a/coqprime/Coqprime/Zp.v b/coqprime/Coqprime/Zp.v index 1e5295191..6383b08b9 100644 --- a/coqprime/Coqprime/Zp.v +++ b/coqprime/Coqprime/Zp.v @@ -7,12 +7,12 @@ (*************************************************************) (********************************************************************** - Zp.v - + Zp.v + Build the group of the inversible element on {1, 2, .., n-1} for the multiplication modulo n - - Definition: ZpGroup + + Definition: ZpGroup **********************************************************************) Require Import ZArith Znumtheory Zpow_facts. Require Import Tactic. @@ -34,14 +34,14 @@ 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. + Z_of_nat m :: match m with O => nil | (S m1) => mkZp_aux m1 end. -(************************************** +(************************************** Some properties of mkZp_aux **************************************) @@ -75,13 +75,13 @@ 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 **************************************) @@ -109,13 +109,13 @@ 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 **************************************) @@ -155,7 +155,7 @@ Qed. Definition Lrel := isupport_aux _ pmult mkZp 1 Z_eq_dec (progression Zsucc 0 (Zabs_nat n)). -Theorem rel_prime_is_inv: +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. @@ -184,8 +184,8 @@ unfold pmult in H2; rewrite (Zmult_comm c); try rewrite H2. ring. Qed. -(************************************** - We are now ready to build our group +(************************************** + We are now ready to build our group **************************************) Definition ZPGroup : (FGroup pmult). @@ -232,7 +232,7 @@ 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))). +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). @@ -246,7 +246,7 @@ 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). +assert (In a mkZp). apply (isupport_aux_incl _ pmult mkZp 1 Z_eq_dec); auto. apply in_mkZp; auto. Qed. @@ -330,8 +330,8 @@ 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. +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. @@ -343,7 +343,7 @@ 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). +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. @@ -355,7 +355,7 @@ 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). +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. diff --git a/coqprime/Makefile b/coqprime/Makefile index c8e44a658..2b995982e 100644 --- a/coqprime/Makefile +++ b/coqprime/Makefile @@ -14,7 +14,7 @@ # # This Makefile was generated by the command line : -# coq_makefile -f _CoqProject -o Makefile +# coq_makefile -f _CoqProject -o Makefile # .DEFAULT_GOAL := all @@ -151,7 +151,7 @@ endif # # ####################################### -all: $(VOFILES) +all: $(VOFILES) quick: $(VOFILES:.vo=.vio) @@ -316,4 +316,3 @@ $(addsuffix .beautified,$(VFILES)): %.v.beautified: # Edit at your own risks ! # # END OF WARNING - -- cgit v1.2.3