From a47b49b11d17add5ca1ea5e650d2f344219b4f7e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 5 Feb 2016 15:24:42 -0500 Subject: Update build process to use COQPATH & _CoqProject Removed all of the files not built by default; they can be resurrected from git history. _CoqProject is the standard way to list the files in a project and to give information to coq_makefile. COQPATH is the standard way to make use of not-yet-installed libraries that are not part of your project (i.e., you don't want to remove them when you `make clean`, etc.). --- coqprime/PrimalityTest/Pepin.v | 123 ----------------------------------------- 1 file changed, 123 deletions(-) delete mode 100644 coqprime/PrimalityTest/Pepin.v (limited to 'coqprime/PrimalityTest/Pepin.v') diff --git a/coqprime/PrimalityTest/Pepin.v b/coqprime/PrimalityTest/Pepin.v deleted file mode 100644 index c400e0a43..000000000 --- a/coqprime/PrimalityTest/Pepin.v +++ /dev/null @@ -1,123 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -(********************************************************************** - Pepin.v - - Pepin's Test for Fermat Number - - Definition: PepinTest - **********************************************************************) -Require Import ZArith. -Require Import ZCAux. -Require Import Pocklington. - -Open Scope Z_scope. - -Definition FermatNumber n := 2^(2^(Z_of_nat n)) + 1. - -Theorem Fermat_pos: forall n, 1 < FermatNumber n. -unfold FermatNumber; intros n; apply Zle_lt_trans with (2 ^ 2 ^(Z_of_nat n)); auto with zarith. -rewrite <- (Zpower_0_r 2); auto with zarith. -apply Zpower_le_monotone; try split; auto with zarith. -Qed. - -Theorem PepinTest: forall n, let Fn := FermatNumber n in (3 ^ ((Fn - 1) / 2) + 1) mod Fn = 0 -> prime Fn. -intros n Fn H. -assert (Hn: 1 < Fn). -unfold Fn; apply Fermat_pos. -apply PocklingtonCorollary1 with (F1 := 2^(2^(Z_of_nat n))) (R1 := 1); auto with zarith. -2: unfold Fn, FermatNumber; auto with zarith. -apply Zlt_le_trans with (2 ^ 1); auto with zarith. -rewrite Zpower_1_r; auto with zarith. -apply Zpower_le_monotone; try split; auto with zarith. -rewrite <- (Zpower_0_r 2); apply Zpower_le_monotone; try split; auto with zarith. -unfold Fn, FermatNumber. -assert (H1: 2 <= 2 ^ 2 ^ Z_of_nat n). -pattern 2 at 1; rewrite <- (Zpower_1_r 2); auto with zarith. -apply Zpower_le_monotone; split; auto with zarith. -rewrite <- (Zpower_0_r 2); apply Zpower_le_monotone; try split; auto with zarith. -apply Zlt_le_trans with (2 * 2 ^2 ^Z_of_nat n). -assert (tmp: forall p, 2 * p = p + p); auto with zarith. -apply Zmult_le_compat_r; auto with zarith. -assert (Hd: (2 | Fn - 1)). -exists (2 ^ (2^(Z_of_nat n) - 1)). -pattern 2 at 3; rewrite <- (Zpower_1_r 2). -rewrite <- Zpower_exp; auto with zarith. -assert (tmp: forall p, p = (p - 1) +1); auto with zarith; rewrite <- tmp. -unfold Fn, FermatNumber; ring. -assert (0 < 2 ^ Z_of_nat n); auto with zarith. -intros p Hp Hp1; exists 3; split; auto with zarith; split; auto. -rewrite (Zdivide_Zdiv_eq 2 (Fn -1)); auto with zarith. -rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith. -rewrite Zpower_mod; auto with zarith. -assert (tmp: forall p, p = (p + 1) -1); auto with zarith; rewrite (fun x => (tmp (3 ^ x))). -rewrite Zminus_mod; auto with zarith. -rewrite H. -rewrite (Zmod_small 1); auto with zarith. -rewrite <- Zpower_mod; auto with zarith. -rewrite Zmod_small; auto with zarith. -simpl; unfold Zpower_pos; simpl; auto with zarith. -apply Z_div_pos; auto with zarith. -apply Zis_gcd_gcd; auto with zarith. -apply Zis_gcd_intro; auto with zarith. -intros x HD1 HD2. -assert (Hd1: p = 2). -apply prime_div_Zpower_prime with (4 := Hp1); auto with zarith. -apply prime_2. -assert (Hd2: (x | 2)). -replace 2 with ((3 ^ ((Fn - 1) / 2) + 1) - (3 ^ ((Fn - 1) / 2) - 1)); auto with zarith. -apply Zdivide_minus_l; auto. -apply Zdivide_trans with (1 := HD2). -apply Zmod_divide; auto with zarith. -rewrite <- Hd1; auto. -replace 1 with (Fn - (Fn - 1)); auto with zarith. -apply Zdivide_minus_l; auto. -apply Zdivide_trans with (1 := Hd2); auto. -Qed. - -(* An optimized version with Zpow_mod *) - -Definition pepin_test n := - let Fn := FermatNumber n in if Z_eq_dec (Zpow_mod 3 ((Fn - 1) / 2) Fn) (Fn - 1) then true else false. - -Theorem PepinTestOp: forall n, pepin_test n = true -> prime (FermatNumber n). -intros n; unfold pepin_test. -match goal with |- context[if ?X then _ else _] => case X end; try (intros; discriminate). -intros H1 _; apply PepinTest. -generalize (Fermat_pos n); intros H2. -rewrite Zplus_mod; auto with zarith. -rewrite <- Zpow_mod_Zpower_correct; auto with zarith. -rewrite H1. -rewrite (Zmod_small 1); auto with zarith. -replace (FermatNumber n - 1 + 1) with (FermatNumber n); auto with zarith. -apply Zdivide_mod; auto with zarith. -apply Z_div_pos; auto with zarith. -Qed. - -Theorem prime5: prime 5. -exact (PepinTestOp 1 (refl_equal _)). -Qed. - -Theorem prime17: prime 17. -exact (PepinTestOp 2 (refl_equal _)). -Qed. - -Theorem prime257: prime 257. -exact (PepinTestOp 3 (refl_equal _)). -Qed. - -Theorem prime65537: prime 65537. -exact (PepinTestOp 4 (refl_equal _)). -Qed. - -(* Too tough !! -Theorem prime4294967297: prime 4294967297. -refine (PepinTestOp 5 (refl_equal _)). -Qed. -*) -- cgit v1.2.3