blob: 4fd151d366419dbaa1cf8129de3c3108aec8fd79 (
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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
Require Import BinInt BinNat ZArith Znumtheory.
Require Import Eqdep_dec.
Require Import Tactics.VerdiTactics.
Section GaloisPreliminaries.
Definition Prime := {x: Z | prime x}.
Definition primeToZ(x: Prime) := proj1_sig x.
Coercion primeToZ: Prime >-> Z.
End GaloisPreliminaries.
Module Type Modulus.
Parameter modulus: Prime.
End Modulus.
Module Galois (M: Modulus).
Import M.
Definition GF := {x: Z | x = x mod modulus}.
Definition GFToZ(x: GF) := proj1_sig x.
Coercion GFToZ: GF >-> Z.
Definition ZToGF (x: Z) : if ((0 <=? x) && (x <? modulus))%bool then GF else True.
break_if; [|trivial].
exists x.
destruct (Bool.andb_true_eq _ _ (eq_sym Heqb)); clear Heqb.
erewrite Zmod_small; [trivial|].
intuition.
- rewrite <- Z.leb_le; auto.
- rewrite <- Z.ltb_lt; auto.
Defined.
Theorem gf_eq: forall (x y: GF), x = y <-> GFToZ x = GFToZ y.
Proof.
destruct x, y; intuition; simpl in *; try congruence.
subst x.
f_equal.
apply UIP_dec.
apply Z.eq_dec.
Qed.
(* Elementary operations *)
Definition GFzero: GF.
exists 0.
abstract trivial.
Defined.
Definition GFone: GF.
exists 1.
abstract( symmetry; apply Zmod_small; intuition;
destruct modulus; simpl;
apply prime_ge_2 in p; intuition).
Defined.
Lemma GFone_nonzero : GFone <> GFzero.
Proof.
unfold GFone, GFzero.
intuition; solve_by_inversion.
Qed.
Hint Resolve GFone_nonzero.
Definition GFplus(x y: GF): GF.
exists ((x + y) mod modulus);
abstract (rewrite Zmod_mod; trivial).
Defined.
Definition GFminus(x y: GF): GF.
exists ((x - y) mod modulus).
abstract (rewrite Zmod_mod; trivial).
Defined.
Definition GFmult(x y: GF): GF.
exists ((x * y) mod modulus).
abstract (rewrite Zmod_mod; trivial).
Defined.
Definition GFopp(x: GF): GF := GFminus GFzero x.
(* Totient Preliminaries *)
Fixpoint GFexp' (x: GF) (power: positive) :=
match power with
| xH => x
| xO power' => GFexp' (GFmult x x) power'
| xI power' => GFmult x (GFexp' (GFmult x x) power')
end.
Definition GFexp (x: GF) (power: N): GF :=
match power with
| N0 => GFone
| Npos power' => GFexp' x power'
end.
(* Inverses + division derived from the existence of a totient *)
Definition isTotient(e: N) := N.gt e 0 /\ forall g: GF, g <> GFzero ->
GFexp g e = GFone.
Definition Totient := {e: N | isTotient e}.
Theorem fermat_little_theorem: isTotient (N.pred (Z.to_N modulus)).
Admitted.
Definition totient : Totient.
exists (N.pred (Z.to_N modulus)).
exact fermat_little_theorem.
Defined.
Definition totientToN(x: Totient) := proj1_sig x.
Coercion totientToN: Totient >-> N.
Definition GFinv(x: GF): GF := GFexp x (N.pred totient).
Definition GFdiv(x y: GF): GF := GFmult x (GFinv y).
End Galois.
|
