blob: e571d8e3c6545edd48748a4ef9253220710d24c8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
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 Coq.ZArith.ZArith.
Require Export Coq.ZArith.Znumtheory.
Require Import Coqprime.Tactic.
Require Export Coqprime.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.
|
