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
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
|
Require Import BinInt BinNat ZArith Znumtheory.
Require Import BoolEq Field_theory.
Require Export Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
Require Import Crypto.Tactics.VerdiTactics.
(* This file is for the actual field tactics and some specialized
* morphisms that help field operate.
*
* When you want a Galois Field, this is the /only module/ you
* should import, because it automatically pulls in everything
* from Galois and the Modulus.
*)
Module GaloisField (M: Modulus).
Module G := Galois M.
Module T := GaloisTheory M.
Export M G T.
(* Define a "ring morphism" between GF and Z, i.e. an equivalence
* between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'.
*
* Doing this allows us to do our coefficient manipulations in Z
* rather than GF, because we know it's equivalent to inject the
* result afterward.
*)
Lemma GFring_morph:
ring_morph GFzero GFone GFplus GFmult GFminus GFopp eq
0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
inject.
Proof.
constructor; intros; try galois;
try (apply gf_eq; simpl; intuition).
apply Zmod_small; destruct modulus; simpl;
apply prime_ge_2 in p; intuition.
replace (- (x mod modulus)) with (0 - (x mod modulus));
try rewrite Zminus_mod_idemp_r; trivial.
replace x with y; intuition.
symmetry; apply Zeq_bool_eq; trivial.
Qed.
(* Redefine our division theory under the ring morphism *)
Lemma GFmorph_div_theory:
div_theory eq Zplus Zmult inject Z.quotrem.
Proof.
constructor; intros; intuition.
replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b);
try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
eq_remove_proofs; demod;
rewrite <- (Z.quot_rem' a b);
destruct a; simpl; trivial.
Qed.
(* Some simple utility lemmas *)
Lemma injectZeroIsGFZero :
GFzero = inject 0.
Proof.
apply gf_eq; simpl; trivial.
Qed.
Lemma injectOneIsGFOne :
GFone = inject 1.
Proof.
apply gf_eq; simpl; intuition.
symmetry; apply Zmod_small; destruct modulus; simpl;
apply prime_ge_2 in p; intuition.
Qed.
Lemma exist_neq: forall A (P: A -> Prop) x y Px Py, x <> y -> exist P x Px <> exist P y Py.
Proof.
intuition; solve_by_inversion.
Qed.
(* Change all GFones to (inject 1) and GFzeros to (inject 0) so that
* we can use our ring morphism to simplify them
*)
Ltac GFpreprocess :=
repeat rewrite injectZeroIsGFZero;
repeat rewrite injectOneIsGFOne.
(* Split up the equation (because field likes /\, then
* change back all of our GFones and GFzeros.
*
* TODO (adamc): what causes it to generate these subproofs?
*)
Ltac GFpostprocess :=
repeat split;
repeat match goal with [ |- context[exist ?a ?b (inject_subproof ?x)] ] =>
replace (exist a b (inject_subproof x)) with (inject x%Z) by reflexivity
end;
repeat rewrite <- injectZeroIsGFZero;
repeat rewrite <- injectOneIsGFOne.
(* Tactic to passively convert from GF to Z in special circumstances *)
Ltac GFconstant t :=
match t with
| inject ?x => x
| _ => NotConstant
end.
(* Add our ring with all the fixin's *)
Add Ring GFring_Z : GFring_theory
(morphism GFring_morph,
constants [GFconstant],
div GFmorph_div_theory,
power_tac GFpower_theory [GFexp_tac]).
(* Add our field with all the fixin's *)
Add Field GFfield_Z : GFfield_theory
(morphism GFring_morph,
preprocess [GFpreprocess],
postprocess [GFpostprocess],
constants [GFconstant],
div GFmorph_div_theory,
power_tac GFpower_theory [GFexp_tac]).
Local Open Scope GF_scope.
Lemma GF_mul_eq : forall x y z, z <> 0 -> x * z = y * z -> x = y.
Proof.
intros ? ? ? z_nonzero mul_z_eq.
replace x with (x * 1) by field.
rewrite <- (GF_multiplicative_inverse z_nonzero).
replace (x * (GFinv z * z)) with ((x * z) * GFinv z) by ring.
rewrite mul_z_eq.
replace (y * z * GFinv z) with (y * (GFinv z * z)) by ring.
rewrite GF_multiplicative_inverse; auto; field.
Qed.
Lemma GF_mul_0_l : forall x, 0 * x = 0.
Proof.
intros; field.
Qed.
Lemma GF_mul_0_r : forall x, x * 0 = 0.
Proof.
intros; field.
Qed.
Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}.
intros.
assert (H := Z.eq_dec (inject x) (inject y)).
destruct H.
- left; galois; intuition.
- right; intuition.
rewrite H in n.
assert (y = y); intuition.
Qed.
Lemma mul_nonzero_l : forall a b, a*b <> 0 -> a <> 0.
intros; intuition; subst.
assert (0 * b = 0) by field; intuition.
Qed.
Lemma mul_nonzero_r : forall a b, a*b <> 0 -> b <> 0.
intros; intuition; subst.
assert (a * 0 = 0) by field; intuition.
Qed.
Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0.
intros.
assert (Z := GF_eq_dec a 0); destruct Z.
- left; intuition.
- assert (a * b / a = 0) by
( rewrite H; field; intuition ).
field_simplify in H0.
replace (b/1) with b in H0 by (field; intuition).
right; intuition.
apply n in H0; intuition.
Qed.
Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0.
intros; intuition; subst.
apply mul_zero_why in H1.
destruct H1; subst; intuition.
Qed.
Hint Resolve mul_nonzero_nonzero.
Lemma GFexp_distr_mul : forall x y z, (0 <= z)%N ->
(x ^ z) * (y ^ z) = (x * y) ^ z.
Proof.
intros.
replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id.
apply natlike_ind with (x := Z.of_N z); simpl; [ field | |
replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto].
intros z' z'_nonneg IHz'.
rewrite Z2N.inj_succ by auto.
rewrite (GFexp_pred x) by apply N.neq_succ_0.
rewrite (GFexp_pred y) by apply N.neq_succ_0.
rewrite (GFexp_pred (x * y)) by apply N.neq_succ_0.
rewrite N.pred_succ.
rewrite <- IHz'.
field.
Qed.
Lemma GF_square_mul : forall x y z, (y <> 0) ->
x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z.
Proof.
intros ? ? ? y_nonzero A.
exists (x / y).
assert ((x / y) ^ 2 = x ^ 2 / y ^ 2) as square_distr_div. {
unfold GFdiv, GFexp, GFexp'.
replace (GFinv (y * y)) with (GFinv y * GFinv y); try ring.
unfold GFinv.
destruct (N.eq_dec (N.pred (totientToN totient)) 0) as [ eq_zero | neq_zero ];
[ rewrite eq_zero | rewrite GFexp_distr_mul ]; try field.
simpl.
do 2 rewrite <- Z2N.inj_pred.
replace 0%N with (Z.to_N 0%Z) by auto.
apply Z2N.inj_le; modulus_bound.
}
assert (y ^ 2 <> 0) as y2_nonzero by (apply mul_nonzero_nonzero; auto).
rewrite (GF_mul_eq _ z (y ^ 2)); auto.
unfold GFdiv.
rewrite <- A.
field; auto.
Qed.
Lemma sqrt_solutions : forall x y, y ^ 2 = x ^ 2 -> y = x \/ y = GFopp x.
Proof.
intros.
(* TODO(jadep) *)
Admitted.
Lemma GFopp_swap : forall x y, GFopp x = y <-> x = GFopp y.
Proof.
split; intro; subst; field.
Qed.
Lemma GFopp_involutive : forall x, GFopp (GFopp x) = x.
Proof.
intros; field.
Qed.
End GaloisField.
|
