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
|
Require Import Coq.ZArith.BinInt Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems.
(* Example for modular arithmetic with a concrete modulus in a section *)
Section Mod24.
(* Set notations + - * / refer to F operations *)
Local Open Scope F_scope.
(* Specify modulus *)
Let q := 24.
(* Boilerplate for letting Z numbers be interpreted as field elements *)
Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
(* Boilerplate for [ring]. Similar boilerplate works for [field] if
the modulus is prime . *)
Add Ring Fring_q : (@Fring_theory q)
(morphism (@Fring_morph q),
preprocess [unfold ZToFq; Fpreprocess],
postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
constants [Fconstant],
div (@Fmorph_div_theory q),
power_tac (@Fpower_theory q) [Fexp_tac]).
Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + 2*a*b + b^2.
Proof.
intros.
ring.
Qed.
End Mod24.
(* Example for modular arithmetic with an abstract modulus in a section *)
Section Modq.
Context {q:Z} {prime_q:prime q}.
Existing Instance prime_q.
(* Set notations + - * / refer to F operations *)
Local Open Scope F_scope.
(* Boilerplate for letting Z numbers be interpreted as field elements *)
Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
(* Boilerplate for [field]. Similar boilerplate works for [ring] if
the modulus is not prime . *)
Add Field Ffield_q' : (@Ffield_theory q _)
(morphism (@Fring_morph q),
preprocess [unfold ZToFq; Fpreprocess],
postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
constants [Fconstant],
div (@Fmorph_div_theory q),
power_tac (@Fpower_theory q) [Fexp_tac]).
Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + ZToField 2*(a/c)*(b/c) + b^2/c^2.
Proof.
intros.
field.
Qed.
End Modq.
(*** The old way: Modules ***)
Module Modulus31 <: PrimeModulus.
Definition modulus := 2^5 - 1.
Lemma prime_modulus : prime modulus.
Admitted.
End Modulus31.
Module Modulus127 <: PrimeModulus.
Definition modulus := 2^127 - 1.
Lemma prime_modulus : prime modulus.
Admitted.
End Modulus127.
Module Example31.
(* Then we can construct a field with that modulus *)
Module Import Field := FieldModulo Modulus31.
Import Modulus31.
(* And pull in the appropriate notations *)
Local Open Scope F_scope.
(* First, let's solve a ring example*)
Lemma ring_example: forall x: F modulus, x * (ZToField 2) = x + x.
Proof.
intros.
ring.
Qed.
(* Unfortunately, the [ring] and [field] tactics need syntactic
(not definitional) equality to recognize the ring in question.
Therefore, it is necessary to explicitly rewrite the modulus
(usually hidden by implicitn arguments) match the one passed to
[FieldModulo]. *)
Lemma ring_example': forall x: F (2^5-1), x * (ZToField 2) = x + x.
Proof.
intros.
change (2^5-1)%Z with modulus.
ring.
Qed.
(* Then a field example (we have to know we can't divide by zero!) *)
Lemma field_example: forall x y z: F modulus, z <> 0 ->
x * (y / z) / z = x * y / (z ^ 2).
Proof.
intros; simpl.
field; trivial.
Qed.
(* Then an example with exponentiation *)
Lemma exp_example: forall x: F modulus, x ^ 2 + ZToField 2 * x + 1 = (x + 1) ^ 2.
Proof.
intros; simpl.
field; trivial.
Qed.
(* In general, the rule I've been using is:
- If our goal looks like x = y:
+ If we need to use assumptions to prove the goal, then before
we apply field,
* Perform all relevant substitutions (especially subst)
* If we have something more complex, we're probably going
to have to performe some sequence of "replace X with Y"
and solve out the subgoals manually before we can use
field.
+ Else, just use field directly
- If we just want to simplify terms and put them into a canonical
form, then field_simplify or ring_simplify should do the trick.
Note, however, that the canonical form has lots of annoying "/1"s
- Otherwise, do a "replace X with Y" to generate an equality
so that we can use field in the above case
*)
End Example31.
(* Notice that the field tactics work whether we know what the modulus is *)
Module TimesZeroTransparentTestModule.
Module Import Theory := FieldModulo Modulus127.
Import Modulus127.
Local Open Scope F_scope.
Lemma timesZero : forall a : F modulus, a*0 = 0.
intros.
field.
Qed.
End TimesZeroTransparentTestModule.
(* Or if we don't (i.e. it's opaque) *)
Module TimesZeroParametricTestModule (M: PrimeModulus).
Module Theory := FieldModulo M.
Import Theory M.
Local Open Scope F_scope.
Lemma timesZero : forall a : F modulus, a*0 = 0.
intros.
field.
Qed.
Lemma realisticFraction : forall x y d : F modulus, (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x.
Proof.
intros.
field; try exact Fq_1_neq_0.
Qed.
Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus,
ZQ <> 0 ->
ZP <> 0 ->
ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 ->
ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 ->
ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 ->
((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) *
(ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) /
((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
(ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))) =
(XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)).
Proof.
intros.
field; assumption.
Qed.
End TimesZeroParametricTestModule.
|
