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/Coqprime/Euler.v | 88 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 coqprime/Coqprime/Euler.v (limited to 'coqprime/Coqprime/Euler.v') diff --git a/coqprime/Coqprime/Euler.v b/coqprime/Coqprime/Euler.v new file mode 100644 index 000000000..06d92ce57 --- /dev/null +++ b/coqprime/Coqprime/Euler.v @@ -0,0 +1,88 @@ + +(*************************************************************) +(* 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 *) +(*************************************************************) + +(************************************************************************ + + Definition of the Euler Totient function + +*************************************************************************) +Require Import ZArith. +Require Export Znumtheory. +Require Import Tactic. +Require Export ZSum. + +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: + 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. +contradict H2; apply not_rel_prime_0; auto. +rewrite Zplus_0_l; auto. +Qed. + +Theorem phi_pos: forall n, 1 < n -> 0 < phi n. +intros n H; unfold phi. +case (Zle_lt_or_eq 2 n); auto with zarith; intros H1; subst. +rewrite Zsum_S_left; simpl; auto with zarith. +case (rel_prime_dec 1 n); intros H2. +apply Zlt_le_trans with (1 + 0); auto with zarith. +apply Zplus_le_compat_l. +pattern 0 at 1; replace 0 with ((1 + (n - 1) - 2) * 0); auto with zarith. +rewrite <- Zsum_c; auto with zarith. +apply Zsum_le; auto with zarith. +intros x H3; case (rel_prime_dec x n); auto with zarith. +case H2; apply rel_prime_1; auto with zarith. +rewrite Zsum_nn. +case (rel_prime_dec (2 - 1) 2); auto with zarith. +intros H1; contradict H1; apply rel_prime_1; auto with zarith. +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. +unfold phi; apply Zsum_le; auto with zarith. +intros x H1; case (rel_prime_dec x n); auto with zarith. +Qed. + +Theorem prime_phi_n_minus_1: forall n, prime n -> phi n = n - 1. +intros n H; replace (n-1) with ((1 + (n - 1) - 1) * 1); auto with zarith. +assert (Hu: 1 <= n - 1). +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. +intros H6 H7; contradict H6; apply H7; split; auto with zarith. +Qed. + +Theorem phi_n_minus_1_prime: forall n, 1 < n -> phi n = n - 1 -> prime n. +intros n H H1; case (prime_dec n); auto; intros H2. +assert (H3: phi n < n - 1); auto with zarith. +replace (n-1) with ((1 + (n - 1) - 1) * 1); auto with zarith. +assert (Hu: 1 <= n - 1); auto with zarith. +rewrite <- Zsum_c; auto with zarith; unfold phi; apply Zsum_lt; auto. +intros x _; case (rel_prime_dec x n); auto with zarith. +case not_prime_divide with n; auto. +intros x (H3, H4); exists x; repeat split; auto with zarith. +case (rel_prime_dec x n); auto with zarith. +intros H5; absurd (x = 1 \/ x = -1); auto with zarith. +case (Zis_gcd_unique x n x 1); auto. +apply Zis_gcd_intro; auto; exists 1; auto with zarith. +contradict H3; rewrite H1; auto with zarith. +Qed. + +Theorem phi_divide_prime: forall n, 1 < n -> (n - 1 | phi n) -> prime n. +intros n H1 H2; apply phi_n_minus_1_prime; auto. +apply Zle_antisym. +apply phi_le_n_minus_1; auto. +apply Zdivide_le; auto; auto with zarith. +apply phi_pos; auto. +Qed. -- cgit v1.2.3