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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
|
Require Import BinInt BinNat ZArith Znumtheory.
Require Import Eqdep_dec.
Require Import Tactics.VerdiTactics.
(* This file is for the high-level type definitions of
* GF, Primes, Moduli, etc. and their notations and essential
* operations.
*
* The lemmas required for the ring and field theories are
* in GaloisTheory.v and the actual tactic implementations
* for the field are in GaloisField.v. An introduction to the
* use of our implementation of the Galois field is in
* GaloisTutorial.v
*)
Section GaloisPreliminaries.
(* The core prime modulus type, relying on Znumtheory's prime *)
Definition Prime := {x: Z | prime x}.
(* Automagically coerce primes to Z *)
Definition primeToZ(x: Prime) := proj1_sig x.
Coercion primeToZ: Prime >-> Z.
End GaloisPreliminaries.
(* A module to hold the field's modulus, which will be an argument to
* all of our Galois modules.
*)
Module Type Modulus.
Parameter modulus: Prime.
End Modulus.
(* The core Galois Field model *)
Module Galois (M: Modulus).
Import M.
(* The sigma definition of an element of the field: we have
* an element corresponding to the values in Z which can be
* produced by a 'mod' operation.
*)
Definition GF := {x: Z | x = x mod modulus}.
Delimit Scope GF_scope with GF.
Local Open Scope GF_scope.
(* Automagically convert GF to Z when needed *)
Definition GFToZ(x: GF) := proj1_sig x.
Coercion GFToZ: GF >-> Z.
(* Automagically convert Z to GF when needed *)
Definition inject(x: Z): GF.
exists (x mod modulus).
abstract (rewrite Zmod_mod; trivial).
Defined.
Coercion inject : Z >-> GF.
(* Convert Z to GF without a mod operation, for when the modulus is opaque *)
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.
(* Core lemma: equality in GF implies equality in Z *)
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.
(* Core values: One and Zero *)
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.
(* Elementary operations: +, -, * *)
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.
(* Modular exponentiation *)
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.
(* Preliminaries to inversion in a prime field *)
Definition isTotient(e: N) := N.gt e 0 /\ forall g: GF, g <> GFzero ->
GFexp g e = GFone.
Definition Totient := {e: N | isTotient e}.
(* Get a totient via Fermat's little theorem *)
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.
(* Define inversion and division *)
Definition GFinv(x: GF): GF := GFexp x (N.pred totient).
Definition GFdiv(x y: GF): GF := GFmult x (GFinv y).
(* Notations for all of the operations we just made *)
Notation "1" := GFone : GF_scope.
Notation "0" := GFzero : GF_scope.
Infix "+" := GFplus : GF_scope.
Infix "-" := GFminus : GF_scope.
Infix "*" := GFmult : GF_scope.
Infix "/" := GFdiv : GF_scope.
Infix "^" := GFexp : GF_scope.
End Galois.
|
