1 (* ========================================================================= *)
2 (* Theorems about representations as sums of 2 and 4 squares. *)
3 (* ========================================================================= *)
5 needs "Library/prime.ml";;
6 needs "Library/analysis.ml";; (*** only for REAL_ARCH_LEAST! ***)
10 (* ------------------------------------------------------------------------- *)
11 (* Definition of involution and various basic lemmas. *)
12 (* ------------------------------------------------------------------------- *)
14 let involution = new_definition
15 `involution f s = !x. x IN s ==> f(x) IN s /\ (f(f(x)) = x)`;;
17 let INVOLUTION_IMAGE = prove
18 (`!f s. involution f s ==> (IMAGE f s = s)`,
19 REWRITE_TAC[involution; EXTENSION; IN_IMAGE] THEN MESON_TAC[]);;
21 let INVOLUTION_DELETE = prove
22 (`involution f s /\ a IN s /\ (f a = a) ==> involution f (s DELETE a)`,
23 REWRITE_TAC[involution; IN_DELETE] THEN MESON_TAC[]);;
25 let INVOLUTION_STEPDOWN = prove
26 (`involution f s /\ a IN s ==> involution f (s DIFF {a, (f a)})`,
27 REWRITE_TAC[involution; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[]);;
29 let INVOLUTION_NOFIXES = prove
30 (`involution f s ==> involution f {x | x IN s /\ ~(f x = x)}`,
31 REWRITE_TAC[involution; IN_ELIM_THM] THEN MESON_TAC[]);;
33 let INVOLUTION_SUBSET = prove
34 (`!f s t. involution f s /\ (!x. x IN t ==> f(x) IN t) /\ t SUBSET s
36 REWRITE_TAC[involution; SUBSET] THEN MESON_TAC[]);;
38 (* ------------------------------------------------------------------------- *)
39 (* Involution with no fixpoints can only occur on finite set of even card *)
40 (* ------------------------------------------------------------------------- *)
42 let INVOLUTION_EVEN_STEP = prove
45 (!x:A. x IN s ==> ~(f x = x)) /\
47 ==> FINITE(s DIFF {a, (f a)}) /\
48 involution f (s DIFF {a, (f a)}) /\
49 (!x:A. x IN (s DIFF {a, (f a)}) ==> ~(f x = x)) /\
50 (CARD s = CARD(s DIFF {a, (f a)}) + 2)`,
51 SIMP_TAC[FINITE_DIFF; INVOLUTION_STEPDOWN; IN_DIFF] THEN STRIP_TAC THEN
52 SUBGOAL_THEN `s = (a:A) INSERT (f a) INSERT (s DIFF {a, (f a)})` MP_TAC THENL
53 [REWRITE_TAC[EXTENSION; IN_INSERT; IN_DIFF; NOT_IN_EMPTY] THEN
54 ASM_MESON_TAC[involution]; ALL_TAC] THEN
55 DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [th]) THEN
56 ASM_SIMP_TAC[CARD_CLAUSES; FINITE_DIFF; FINITE_INSERT] THEN
57 ASM_SIMP_TAC[IN_INSERT; IN_DIFF; NOT_IN_EMPTY] THEN ARITH_TAC);;
59 let INVOLUTION_EVEN_INDUCT = prove
60 (`!n s. FINITE(s) /\ (CARD s = n) /\ involution f s /\
61 (!x:A. x IN s ==> ~(f x = x))
63 MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
64 ASM_CASES_TAC `s:A->bool = {}` THEN
65 ASM_REWRITE_TAC[CARD_CLAUSES; ARITH] THEN
66 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [EXTENSION]) THEN
67 REWRITE_TAC[NOT_IN_EMPTY; NOT_FORALL_THM] THEN
68 DISCH_THEN(X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC) THEN STRIP_TAC THEN
69 FIRST_X_ASSUM(MP_TAC o SPEC `CARD(s DIFF {a:A, (f a)})`) THEN
70 REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
71 DISCH_THEN(MP_TAC o SPEC `s DIFF {a:A, (f a)}`) THEN
72 MP_TAC INVOLUTION_EVEN_STEP THEN ASM_REWRITE_TAC[] THEN
73 STRIP_TAC THEN ASM_REWRITE_TAC[ARITH_RULE `n < n + 2`] THEN
74 SIMP_TAC[EVEN_ADD; ARITH]);;
76 let INVOLUTION_EVEN = prove
77 (`!s. FINITE(s) /\ involution f s /\ (!x:A. x IN s ==> ~(f x = x))
79 MESON_TAC[INVOLUTION_EVEN_INDUCT]);;
81 (* ------------------------------------------------------------------------- *)
82 (* So an involution with exactly one fixpoint has odd card domain. *)
83 (* ------------------------------------------------------------------------- *)
85 let INVOLUTION_FIX_ODD = prove
86 (`FINITE(s) /\ involution f s /\ (?!a:A. a IN s /\ (f a = a))
88 REWRITE_TAC[EXISTS_UNIQUE_DEF] THEN STRIP_TAC THEN
89 SUBGOAL_THEN `s = (a:A) INSERT (s DELETE a)` SUBST1_TAC THENL
90 [REWRITE_TAC[EXTENSION; IN_INSERT; IN_DELETE] THEN ASM_MESON_TAC[];
92 ASM_SIMP_TAC[CARD_CLAUSES; FINITE_DELETE; IN_DELETE; ODD; NOT_ODD] THEN
93 MATCH_MP_TAC INVOLUTION_EVEN THEN
94 ASM_SIMP_TAC[INVOLUTION_DELETE; FINITE_DELETE; IN_DELETE] THEN
97 (* ------------------------------------------------------------------------- *)
98 (* And an involution on a set of odd finite card must have a fixpoint. *)
99 (* ------------------------------------------------------------------------- *)
101 let INVOLUTION_ODD = prove
102 (`!n s. FINITE(s) /\ involution f s /\ ODD(CARD s)
103 ==> ?a. a IN s /\ (f a = a)`,
104 REWRITE_TAC[GSYM NOT_EVEN] THEN MESON_TAC[INVOLUTION_EVEN]);;
106 (* ------------------------------------------------------------------------- *)
107 (* Consequently, if one involution has a unique fixpoint, other has one. *)
108 (* ------------------------------------------------------------------------- *)
110 let INVOLUTION_FIX_FIX = prove
111 (`!f g s. FINITE(s) /\ involution f s /\ involution g s /\
112 (?!x. x IN s /\ (f x = x)) ==> ?x. x IN s /\ (g x = x)`,
113 REPEAT STRIP_TAC THEN MATCH_MP_TAC INVOLUTION_ODD THEN
114 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC INVOLUTION_FIX_ODD THEN
117 (* ------------------------------------------------------------------------- *)
118 (* Formalization of Zagier's "one-sentence" proof over the natural numbers. *)
119 (* ------------------------------------------------------------------------- *)
121 let zset = new_definition
122 `zset(a) = {(x,y,z) | x EXP 2 + 4 * y * z = a}`;;
124 let zag = new_definition
126 if x + z < y then (x + 2 * z,z,y - (x + z))
127 else if x < 2 * y then (2 * y - x, y, (x + z) - y)
128 else (x - 2 * y,(x + z) - y, y)`;;
130 let tag = new_definition
131 `tag((x,y,z):num#num#num) = (x,z,y)`;;
133 let ZAG_INVOLUTION_GENERAL = prove
134 (`0 < x /\ 0 < y /\ 0 < z ==> (zag(zag(x,y,z)) = (x,y,z))`,
135 REWRITE_TAC[zag] THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
136 REWRITE_TAC[zag] THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
137 REWRITE_TAC[PAIR_EQ] THEN
138 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);;
140 let IN_TRIPLE = prove
141 (`(a,b,c) IN {(x,y,z) | P x y z} <=> P a b c`,
142 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN MESON_TAC[]);;
144 let PRIME_SQUARE = prove
145 (`!n. ~prime(n * n)`,
146 GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN
147 ASM_REWRITE_TAC[PRIME_0; MULT_CLAUSES] THEN
148 REWRITE_TAC[prime; NOT_FORALL_THM; DE_MORGAN_THM] THEN
149 ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[ARITH] THEN
150 DISJ2_TAC THEN EXISTS_TAC `n:num` THEN
151 ASM_SIMP_TAC[DIVIDES_LMUL; DIVIDES_REFL] THEN
152 GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [ARITH_RULE `n = n * 1`] THEN
153 ASM_SIMP_TAC[EQ_MULT_LCANCEL]);;
156 (`!n. ~prime(4 * n)`,
157 GEN_TAC THEN REWRITE_TAC[prime; NOT_FORALL_THM; DE_MORGAN_THM] THEN
158 DISJ2_TAC THEN EXISTS_TAC `2` THEN
159 SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 * 2`)) THEN
160 ASM_SIMP_TAC[GSYM MULT_ASSOC; DIVIDES_RMUL; DIVIDES_REFL; ARITH_EQ] THEN
161 ASM_CASES_TAC `n = 0` THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;
163 let PRIME_XYZ_NONZERO = prove
164 (`prime(x EXP 2 + 4 * y * z) ==> 0 < x /\ 0 < y /\ 0 < z`,
165 CONV_TAC CONTRAPOS_CONV THEN
166 REWRITE_TAC[DE_MORGAN_THM; ARITH_RULE `~(0 < x) = (x = 0)`] THEN
167 DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC) THEN
168 REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES; PRIME_SQUARE; PRIME_4X]);;
170 let ZAG_INVOLUTION = prove
171 (`!p. prime(p) ==> involution zag (zset(p))`,
172 REPEAT STRIP_TAC THEN REWRITE_TAC[involution; FORALL_PAIR_THM] THEN
173 MAP_EVERY X_GEN_TAC [`x:num`; `y:num`; `z:num`] THEN
174 REWRITE_TAC[zset; IN_TRIPLE] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
176 [REWRITE_TAC[zag] THEN REPEAT COND_CASES_TAC THEN
177 ASM_REWRITE_TAC[IN_TRIPLE] THEN
178 RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT]) THEN
179 ASM_SIMP_TAC[GSYM INT_OF_NUM_EQ; GSYM INT_OF_NUM_ADD; EXP_2;
180 GSYM INT_OF_NUM_MUL; GSYM INT_OF_NUM_SUB; LT_IMP_LE] THEN
182 MATCH_MP_TAC ZAG_INVOLUTION_GENERAL THEN
183 ASM_MESON_TAC[PRIME_XYZ_NONZERO]]);;
185 let TAG_INVOLUTION = prove
186 (`!a. involution tag (zset a)`,
187 REWRITE_TAC[involution; tag; zset; FORALL_PAIR_THM] THEN
188 REWRITE_TAC[IN_TRIPLE] THEN REWRITE_TAC[MULT_AC]);;
190 let ZAG_LEMMA = prove
191 (`(zag(x,y,z) = (x,y,z)) ==> (y = x)`,
192 REWRITE_TAC[zag; INT_POW_2] THEN
193 REPEAT(COND_CASES_TAC THEN ASM_SIMP_TAC[PAIR_EQ]) THEN
194 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);;
196 let ZSET_BOUND = prove
197 (`0 < y /\ 0 < z /\ (x EXP 2 + 4 * y * z = p)
198 ==> x <= p /\ y <= p /\ z <= p`,
199 REPEAT GEN_TAC THEN STRIP_TAC THEN
200 FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN CONJ_TAC THENL
201 [MESON_TAC[EXP_2; LE_SQUARE_REFL; ARITH_RULE `(a <= b ==> a <= b + c)`];
202 CONJ_TAC THEN MATCH_MP_TAC(ARITH_RULE `y <= z ==> y <= x + z`) THENL
203 [GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [MULT_SYM]; ALL_TAC] THEN
204 REWRITE_TAC[ARITH_RULE `y <= 4 * a * y <=> 1 * y <= (4 * a) * y`] THEN
205 ASM_REWRITE_TAC[LE_MULT_RCANCEL] THEN
206 ASM_SIMP_TAC[ARITH_RULE `0 < a ==> 1 <= 4 * a`]]);;
208 let ZSET_FINITE = prove
209 (`!p. prime(p) ==> FINITE(zset p)`,
210 GEN_TAC THEN DISCH_TAC THEN
211 MP_TAC(SPEC `p + 1` FINITE_NUMSEG_LT) THEN
213 MP_TAC(funpow 2 (MATCH_MP FINITE_PRODUCT o CONJ th) th)) THEN
214 MATCH_MP_TAC(REWRITE_RULE[TAUT `a /\ b ==> c <=> b ==> a ==> c`]
216 REWRITE_TAC[zset; SUBSET; FORALL_PAIR_THM; IN_TRIPLE] THEN
217 MAP_EVERY X_GEN_TAC [`x:num`; `y:num`; `z:num`] THEN
218 REWRITE_TAC[IN_ELIM_THM; EXISTS_PAIR_THM; PAIR_EQ] THEN
219 REWRITE_TAC[ARITH_RULE `x < p + 1 <=> x <= p`; PAIR_EQ] THEN
220 DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`x:num`; `y:num`; `z:num`] THEN
221 ASM_REWRITE_TAC[] THEN REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
222 MAP_EVERY EXISTS_TAC [`y:num`; `z:num`] THEN REWRITE_TAC[] THEN
223 ASM_MESON_TAC[ZSET_BOUND; PRIME_XYZ_NONZERO]);;
225 let SUM_OF_TWO_SQUARES = prove
226 (`!p k. prime(p) /\ (p = 4 * k + 1) ==> ?x y. p = x EXP 2 + y EXP 2`,
227 SIMP_TAC[] THEN REPEAT STRIP_TAC THEN
228 SUBGOAL_THEN `?t. t IN zset(p) /\ (tag(t) = t)` MP_TAC THENL
230 REWRITE_TAC[LEFT_IMP_EXISTS_THM; FORALL_PAIR_THM; tag; PAIR_EQ] THEN
231 REWRITE_TAC[zset; IN_TRIPLE; EXP_2] THEN
232 ASM_MESON_TAC[ARITH_RULE `4 * x * y = (2 * x) * (2 * y)`]] THEN
233 MATCH_MP_TAC INVOLUTION_FIX_FIX THEN EXISTS_TAC `zag` THEN
234 ASM_SIMP_TAC[ZAG_INVOLUTION; TAG_INVOLUTION; ZSET_FINITE] THEN
235 REWRITE_TAC[EXISTS_UNIQUE_ALT] THEN EXISTS_TAC `1,1,k:num` THEN
236 REWRITE_TAC[FORALL_PAIR_THM] THEN
237 MAP_EVERY X_GEN_TAC [`x:num`; `y:num`; `z:num`] THEN EQ_TAC THENL
239 DISCH_THEN(SUBST1_TAC o SYM) THEN
240 REWRITE_TAC[zset; zag; IN_TRIPLE; ARITH] THEN
241 REWRITE_TAC[MULT_CLAUSES; ARITH_RULE `~(1 + k < 1)`; PAIR_EQ] THEN
243 REWRITE_TAC[zset; IN_TRIPLE] THEN STRIP_TAC THEN
244 FIRST_ASSUM(SUBST_ALL_TAC o MATCH_MP ZAG_LEMMA) THEN
245 UNDISCH_TAC `x EXP 2 + 4 * x * z = 4 * k + 1` THEN
246 REWRITE_TAC[EXP_2; ARITH_RULE `x * x + 4 * x * z = x * (4 * z + x)`] THEN
247 DISCH_THEN(ASSUME_TAC o SYM) THEN UNDISCH_TAC `prime p` THEN
248 ASM_REWRITE_TAC[] THEN REWRITE_TAC[prime] THEN
249 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `x:num`)) THEN
250 SIMP_TAC[DIVIDES_RMUL; DIVIDES_REFL] THEN
251 DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC MP_TAC) THENL
252 [UNDISCH_TAC `4 * k + 1 = 1 * (4 * z + 1)` THEN
253 REWRITE_TAC[MULT_CLAUSES; PAIR_EQ] THEN ARITH_TAC;
254 ONCE_REWRITE_TAC[ARITH_RULE `(a = a * b) = (a * b = a * 1)`] THEN
255 ASM_SIMP_TAC[EQ_MULT_LCANCEL] THEN STRIP_TAC THENL
256 [UNDISCH_TAC `4 * k + 1 = x * (4 * z + x)` THEN
257 ASM_REWRITE_TAC[MULT_CLAUSES; ADD_EQ_0; ARITH_EQ];
258 UNDISCH_TAC `4 * z + x = 1` THEN REWRITE_TAC[PAIR_EQ] THEN
259 ASM_CASES_TAC `z = 0` THENL
260 [ALL_TAC; UNDISCH_TAC `~(z = 0)` THEN ARITH_TAC] THEN
261 UNDISCH_TAC `4 * k + 1 = x * (4 * z + x)` THEN
262 ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
263 ASM_CASES_TAC `x = 1` THEN ASM_REWRITE_TAC[] THEN
264 REWRITE_TAC[MULT_CLAUSES] THEN ARITH_TAC]]);;
266 (* ------------------------------------------------------------------------- *)
267 (* General pigeonhole lemma. *)
268 (* ------------------------------------------------------------------------- *)
270 let PIGEONHOLE_LEMMA = prove
272 FINITE(s) /\ FINITE(t) /\
273 (!x. x IN s ==> f(x) IN t) /\
274 (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)) /\
275 (!x. x IN s ==> g(x) IN t) /\
276 (!x y. x IN s /\ y IN s /\ (g x = g y) ==> (x = y)) /\
277 CARD(t) < 2 * CARD(s)
278 ==> ?x y. x IN s /\ y IN s /\ (f x = g y)`,
279 REPEAT STRIP_TAC THEN
280 MP_TAC(ISPECL [`IMAGE (f:A->B) s`; `IMAGE (g:A->B) s`] CARD_UNION) THEN
281 SUBGOAL_THEN `(CARD(IMAGE (f:A->B) s) = CARD s) /\
282 (CARD(IMAGE (g:A->B) s) = CARD s)`
283 STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[CARD_IMAGE_INJ]; ALL_TAC] THEN
284 ASM_SIMP_TAC[FINITE_IMAGE] THEN
285 MATCH_MP_TAC(TAUT `(~a ==> c) /\ ~b ==> (a ==> b) ==> c`) THEN CONJ_TAC THENL
286 [REWRITE_TAC[EXTENSION; IN_INSERT; IN_INTER; IN_IMAGE; NOT_IN_EMPTY] THEN
287 MESON_TAC[]; ALL_TAC] THEN
288 MATCH_MP_TAC(ARITH_RULE `!t. t < 2 * s /\ p <= t ==> ~(p = s + s)`) THEN
289 EXISTS_TAC `CARD(t:B->bool)` THEN ASM_REWRITE_TAC[] THEN
290 MATCH_MP_TAC CARD_SUBSET THEN REWRITE_TAC[SUBSET; IN_UNION; IN_IMAGE] THEN
293 (* ------------------------------------------------------------------------- *)
294 (* In particular, consider functions out of 0...(p-1)/2, mod p. *)
295 (* ------------------------------------------------------------------------- *)
297 let PIGEONHOLE_LEMMA_P12 = prove
300 (!x. 2 * x < p ==> f(x) < p) /\
301 (!x y. 2 * x < p /\ 2 * y < p /\ (f x = f y) ==> (x = y)) /\
302 (!x. 2 * x < p ==> g(x) < p) /\
303 (!x y. 2 * x < p /\ 2 * y < p /\ (g x = g y) ==> (x = y))
304 ==> ?x y. 2 * x < p /\ 2 * y < p /\ (f x = g y)`,
305 REPEAT GEN_TAC THEN REWRITE_TAC[ODD_EXISTS] THEN
306 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
307 FIRST_X_ASSUM(X_CHOOSE_THEN `k:num` SUBST1_TAC) THEN
308 MP_TAC(ISPECL [`f:num->num`; `g:num->num`;
309 `{x:num | 2 * x < 2 * k + 1}`; `{x:num | x < 2 * k + 1}`]
310 PIGEONHOLE_LEMMA) THEN
311 REWRITE_TAC[ADD1; ARITH_RULE `2 * x < 2 * k + 1 <=> x < k + 1`] THEN
312 REWRITE_TAC[FINITE_NUMSEG_LT; CARD_NUMSEG_LT] THEN
313 REWRITE_TAC[IN_ELIM_THM; ARITH_RULE `2 * k + 1 < 2 * (k + 1)`]);;
315 (* ------------------------------------------------------------------------- *)
316 (* Show that \x. x^2 + a (mod p) satisfies the conditions. *)
317 (* ------------------------------------------------------------------------- *)
319 let SQUAREMOD_INJ_LEMMA = prove
320 (`!p x d. prime(p) /\ 2 * (x + d) < p /\
321 ((x + d) * (x + d) + m * p = x * x + n * p)
323 REPEAT STRIP_TAC THEN
324 SUBGOAL_THEN `p divides d \/ p divides (2 * x + d)` MP_TAC THENL
325 [MATCH_MP_TAC PRIME_DIVPROD THEN ASM_REWRITE_TAC[divides] THEN
326 EXISTS_TAC `n - m:num` THEN REWRITE_TAC[LEFT_SUB_DISTRIB] THEN
327 MATCH_MP_TAC(ARITH_RULE `!a:num. (a + b + d = a + c) ==> (b = c - d)`) THEN
328 EXISTS_TAC `x * x:num` THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
329 FIRST_ASSUM(SUBST1_TAC o SYM) THEN ARITH_TAC;
330 DISCH_THEN(DISJ_CASES_THEN(MP_TAC o MATCH_MP DIVIDES_LE)) THEN
331 SIMP_TAC[ADD_EQ_0] THEN UNDISCH_TAC `2 * (x + d) < p` THEN ARITH_TAC]);;
333 let SQUAREMOD_INJ = prove
335 ==> (!x. 2 * x < p ==> (x EXP 2 + a) MOD p < p) /\
336 (!x y. 2 * x < p /\ 2 * y < p /\
337 ((x EXP 2 + a) MOD p = (y EXP 2 + a) MOD p)
339 REPEAT STRIP_TAC THEN
340 FIRST_ASSUM(ASSUME_TAC o MATCH_MP(ARITH_RULE `x < a ==> ~(a = 0)`)) THEN
341 ASM_SIMP_TAC[DIVISION] THEN
343 `(x EXP 2 + a = (x EXP 2 + a) DIV p * p + (x EXP 2 + a) MOD p) /\
344 (y EXP 2 + a = (y EXP 2 + a) DIV p * p + (y EXP 2 + a) MOD p)`
345 MP_TAC THENL [ASM_SIMP_TAC[DIVISION]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN
346 DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
347 `(x2 + a = xp + b:num) /\ (y2 + a = yp + b)
348 ==> (x2 + yp = y2 + xp)`)) THEN
349 DISJ_CASES_THEN MP_TAC (SPECL [`x:num`; `y:num`] LE_CASES) THEN
350 DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST_ALL_TAC o
351 REWRITE_RULE[LE_EXISTS])
352 THENL [ONCE_REWRITE_TAC[EQ_SYM_EQ]; ALL_TAC] THEN
353 REWRITE_TAC[EXP_2; ARITH_RULE `(x + d = x) = (d = 0)`] THEN
354 ASM_MESON_TAC[SQUAREMOD_INJ_LEMMA]);;
356 (* ------------------------------------------------------------------------- *)
357 (* Show that also a reflection mod p retains this property. *)
358 (* ------------------------------------------------------------------------- *)
360 let REFLECT_INJ = prove
361 (`(!x. 2 * x < p ==> f(x) < p) /\
362 (!x y. 2 * x < p /\ 2 * y < p /\ (f x = f y) ==> (x = y))
363 ==> (!x. 2 * x < p ==> p - 1 - f(x) < p) /\
364 (!x y. 2 * x < p /\ 2 * y < p /\ (p - 1 - f(x) = p - 1 - f(y))
366 REPEAT GEN_TAC THEN STRIP_TAC THEN
367 REWRITE_TAC[ARITH_RULE `2 * x < p ==> p - 1 - y < p`] THEN
368 REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
369 MATCH_MP_TAC(ARITH_RULE
370 `x < p /\ y < p /\ (p - 1 - x = p - 1 - y) ==> (x = y)`) THEN
373 (* ------------------------------------------------------------------------- *)
374 (* Hence the main result. *)
375 (* ------------------------------------------------------------------------- *)
377 let LAGRANGE_LEMMA_ODD = prove
378 (`!a p. prime(p) /\ ODD(p)
379 ==> ?n x y. 2 * x < p /\ 2 * y < p /\
380 (n * p = x EXP 2 + y EXP 2 + a + 1)`,
381 REPEAT STRIP_TAC THEN
382 SUBGOAL_THEN `~(p = 0)` ASSUME_TAC THENL [ASM_MESON_TAC[ODD]; ALL_TAC] THEN
383 MP_TAC(ISPECL [`\x. (x EXP 2 + a) MOD p`;
384 `\x. p - 1 - (x EXP 2 + 0) MOD p`; `p:num`]
385 PIGEONHOLE_LEMMA_P12) THEN
386 REWRITE_TAC[] THEN ANTS_TAC THENL
387 [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT
388 `(a /\ b) /\ (c /\ d) ==> a /\ b /\ c /\ d`) THEN
390 [ALL_TAC; MATCH_MP_TAC REFLECT_INJ] THEN
391 ASM_MESON_TAC[SQUAREMOD_INJ]; ALL_TAC] THEN
393 FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
394 `(x = p - 1 - y) ==> y < p ==> (x + y + 1 = p)`)) THEN
395 ANTS_TAC THENL [ASM_MESON_TAC[DIVISION]; ALL_TAC] THEN
396 DISCH_THEN(MP_TAC o C AP_THM `p:num` o AP_TERM `(MOD)`) THEN
398 `((x EXP 2 + a) MOD p + (y EXP 2 + 0) MOD p + 1) MOD p =
399 (x EXP 2 + y EXP 2 + a + 1) MOD p`
401 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_EQ THEN
402 EXISTS_TAC `(x EXP 2 + a) DIV p + (y EXP 2) DIV p` THEN
403 REWRITE_TAC[ADD_CLAUSES] THEN
404 MATCH_MP_TAC(ARITH_RULE
405 `(x2 + a = xd * p + xm) /\ (y2 = yd * p + ym)
406 ==> (x2 + y2 + a + 1 = (xm + ym + 1) + (xd + yd) * p)`) THEN
407 ASM_MESON_TAC[DIVISION]; ALL_TAC] THEN
408 SUBGOAL_THEN `p MOD p = 0` SUBST1_TAC THENL
409 [MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `1` THEN
410 UNDISCH_TAC `~(p = 0)` THEN ARITH_TAC; ALL_TAC] THEN
411 DISCH_TAC THEN MAP_EVERY EXISTS_TAC
412 [`(x EXP 2 + y EXP 2 + a + 1) DIV p`; `x:num`; `y:num`] THEN
413 ASM_REWRITE_TAC[] THEN
414 FIRST_ASSUM(MP_TAC o SPEC `x EXP 2 + y EXP 2 + a + 1` o
415 MATCH_MP DIVISION) THEN
416 ASM_REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN MESON_TAC[]);;
418 (* ------------------------------------------------------------------------- *)
419 (* Avoid the additional conditions. *)
420 (* ------------------------------------------------------------------------- *)
422 let LAGRANGE_LEMMA = prove
424 ==> ?n x y. 2 * x <= p /\ 2 * y <= p /\
425 (n * p = x EXP 2 + y EXP 2 + a)`,
426 REPEAT STRIP_TAC THEN ASM_CASES_TAC `EVEN(p)` THENL
427 [FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [prime]) THEN
428 DISCH_THEN(MP_TAC o SPEC `2` o CONJUNCT2) THEN
429 ANTS_TAC THENL [ASM_MESON_TAC[EVEN_EXISTS; divides]; ALL_TAC] THEN
430 REWRITE_TAC[ARITH_EQ] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
431 ASM_CASES_TAC `EVEN(a)` THENL
432 [UNDISCH_TAC `EVEN a` THEN REWRITE_TAC[EVEN_EXISTS] THEN
433 DISCH_THEN(X_CHOOSE_THEN `k:num` SUBST_ALL_TAC) THEN
434 MAP_EVERY EXISTS_TAC [`k:num`; `0`; `0`] THEN
435 REWRITE_TAC[ARITH; ADD_CLAUSES] THEN ARITH_TAC;
436 UNDISCH_TAC `~(EVEN(a))` THEN REWRITE_TAC[NOT_EVEN; ODD_EXISTS] THEN
437 DISCH_THEN(X_CHOOSE_THEN `k:num` SUBST_ALL_TAC) THEN
438 MAP_EVERY EXISTS_TAC [`k + 1`; `1`; `0`] THEN
439 REWRITE_TAC[ARITH; ADD_CLAUSES] THEN ARITH_TAC];
440 ASM_CASES_TAC `a = 0` THENL
441 [MAP_EVERY EXISTS_TAC [`0`; `0`; `0`] THEN
442 ASM_REWRITE_TAC[LE_0; ADD_CLAUSES; MULT_CLAUSES; EXP_2]; ALL_TAC] THEN
443 FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
444 `~(a = 0) ==> (a = (a - 1) + 1)`)) THEN
445 MP_TAC(SPECL [`a - 1`; `p:num`] LAGRANGE_LEMMA_ODD) THEN
446 ASM_REWRITE_TAC[GSYM NOT_EVEN] THEN MESON_TAC[LT_IMP_LE]]);;
448 (* ------------------------------------------------------------------------- *)
449 (* Aubrey's lemma showing that rationals suffice for sums of 4 squares. *)
450 (* ------------------------------------------------------------------------- *)
454 let REAL_INTEGER_CLOSURES = prove
455 (`(!n. ?p. abs(&n) = &p) /\
456 (!x y. (?m. abs(x) = &m) /\ (?n. abs(y) = &n) ==> ?p. abs(x + y) = &p) /\
457 (!x y. (?m. abs(x) = &m) /\ (?n. abs(y) = &n) ==> ?p. abs(x - y) = &p) /\
458 (!x y. (?m. abs(x) = &m) /\ (?n. abs(y) = &n) ==> ?p. abs(x * y) = &p) /\
459 (!x r. (?n. abs(x) = &n) ==> ?p. abs(x pow r) = &p) /\
460 (!x. (?n. abs(x) = &n) ==> ?p. abs(--x) = &p) /\
461 (!x. (?n. abs(x) = &n) ==> ?p. abs(abs x) = &p)`,
463 `x /\ c /\ d /\ e /\ f /\ (a /\ e ==> b) /\ a
464 ==> x /\ a /\ b /\ c /\ d /\ e /\ f`) THEN
465 REPEAT CONJ_TAC THENL
466 [REWRITE_TAC[REAL_ABS_NUM] THEN MESON_TAC[];
467 REWRITE_TAC[REAL_ABS_MUL] THEN MESON_TAC[REAL_OF_NUM_MUL];
468 REWRITE_TAC[REAL_ABS_POW] THEN MESON_TAC[REAL_OF_NUM_POW];
469 REWRITE_TAC[REAL_ABS_NEG]; REWRITE_TAC[REAL_ABS_ABS];
470 REWRITE_TAC[real_sub] THEN MESON_TAC[]; ALL_TAC] THEN
471 SIMP_TAC[REAL_ARITH `&0 <= a ==> ((abs(x) = a) <=> (x = a) \/ (x = --a))`;
473 REPEAT STRIP_TAC THEN
474 ASM_REWRITE_TAC[GSYM REAL_NEG_ADD; REAL_OF_NUM_ADD] THENL
475 [MESON_TAC[]; ALL_TAC; ALL_TAC; MESON_TAC[]] THEN
476 REWRITE_TAC[REAL_ARITH `(--a + b = c) <=> (a + c = b)`;
477 REAL_ARITH `(a + --b = c) <=> (b + c = a)`] THEN
478 REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
479 MESON_TAC[LE_EXISTS; ADD_SYM; LE_CASES]);;
481 let REAL_NUM_ROUND = prove
482 (`!x. &0 <= x ==> ?n. abs(x - &n) <= &1 / &2`,
483 REPEAT STRIP_TAC THEN
484 FIRST_ASSUM(MP_TAC o MATCH_MP (MATCH_MP REAL_ARCH_LEAST REAL_LT_01)) THEN
485 REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_MUL_RID] THEN
486 DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
487 DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
488 `a <= x /\ x < a + &1
489 ==> abs(x - a) * &2 <= &1 \/ abs(x - (a + &1)) * &2 <= &1`)) THEN
490 SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
491 MESON_TAC[REAL_OF_NUM_ADD]);;
493 let REAL_POS_ABS_MIDDLE = prove
494 (`!x n. &0 <= x /\ (abs(x - &n) = &1 / &2)
495 ==> (x = &(n - 1) + &1 / &2) \/ (x = &n + &1 / &2)`,
497 MP_TAC(SPECL [`1`; `n:num`] REAL_OF_NUM_SUB) THEN
498 DISJ_CASES_TAC(ARITH_RULE `(n = 0) \/ 1 <= n`) THEN
499 ASM_REWRITE_TAC[ARITH] THENL
500 [MP_TAC(REAL_RAT_REDUCE_CONV `&0 <= &1 / &2`) THEN REAL_ARITH_TAC;
501 DISCH_THEN(SUBST1_TAC o SYM) THEN
502 REWRITE_TAC[REAL_ARITH `n - &1 + a = n - (&1 - a)`] THEN
503 CONV_TAC REAL_RAT_REDUCE_CONV THEN REAL_ARITH_TAC]);;
505 let REAL_RAT_ABS_MIDDLE = prove
506 (`!m n p. (abs(&m / &p - &n) = &1 / &2)
507 ==> (&m / &p = &(n - 1) + &1 / &2) \/ (&m / &p = &n + &1 / &2)`,
508 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_POS_ABS_MIDDLE THEN
509 ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS]);;
511 let AUBREY_LEMMA_4 = prove
513 ~(m = 0) /\ ~(m = 1) /\
514 ((&n / &m) pow 2 + (&p / &m) pow 2 +
515 (&q / &m) pow 2 + (&r / &m) pow 2 = &N)
517 ~(m' = 0) /\ m' < m /\
518 ((&n' / &m') pow 2 + (&p' / &m') pow 2 +
519 (&q' / &m') pow 2 + (&r' / &m') pow 2 = &N)`,
520 REPEAT STRIP_TAC THEN
521 MATCH_MP_TAC(TAUT `(~p ==> p) ==> p`) THEN
522 REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_TAC THEN
525 (&n / &m - &n') pow 2 + (&p / &m - &p') pow 2 +
526 (&q / &m - &q') pow 2 + (&r / &m - &r') pow 2 < &1 \/
527 (((&n / &m - &n') pow 2 + (&p / &m - &p') pow 2 +
528 (&q / &m - &q') pow 2 + (&r / &m - &r') pow 2 = &1) /\
529 (m = 2) /\ (EVEN(n' + p' + q' + r') = EVEN(N)))`
532 `?n' p' q' r'. (&n / &m = &n' + &1 / &2) /\
533 (&p / &m = &p' + &1 / &2) /\
534 (&q / &m = &q' + &1 / &2) /\
535 (&r / &m = &r' + &1 / &2)` THENL
536 [FIRST_X_ASSUM(CHOOSE_THEN STRIP_ASSUME_TAC) THEN
537 MAP_EVERY EXISTS_TAC [`n':num`; `p':num`; `q':num`] THEN
538 SUBGOAL_THEN `m = 2` SUBST_ALL_TAC THENL
539 [FIRST_X_ASSUM(MP_TAC o SPECL
540 [`2`; `2 * n' + 1`; `2 * p' + 1`; `2 * q' + 1`; `2 * r' + 1`]) THEN
541 REWRITE_TAC[ARITH_EQ; GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
542 REWRITE_TAC[real_div; REAL_ADD_RDISTRIB; GSYM REAL_MUL_ASSOC] THEN
543 REWRITE_TAC[GSYM real_div] THEN
544 SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH_EQ] THEN
545 REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN
546 REWRITE_TAC[] THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
547 ARITH_TAC; ALL_TAC] THEN
548 SUBGOAL_THEN `(EVEN(n' + p' + q' + r') <=> EVEN(N)) \/
549 (EVEN(n' + p' + q' + r' + 1) <=> EVEN(N))`
551 [REWRITE_TAC[EVEN_ADD; ARITH_EVEN] THEN CONV_TAC TAUT;
552 EXISTS_TAC `r':num` THEN DISJ2_TAC THEN ASM_REWRITE_TAC[] THEN
553 REWRITE_TAC[REAL_ARITH `(a + b) - a = b`] THEN
554 CONV_TAC REAL_RAT_REDUCE_CONV;
555 EXISTS_TAC `r' + 1` THEN DISJ2_TAC THEN ASM_REWRITE_TAC[] THEN
556 REWRITE_TAC[REAL_ARITH `(a + b) - a = b`] THEN
557 REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
558 REWRITE_TAC[REAL_ARITH `(a + b) - (a + c) = b - c`] THEN
559 CONV_TAC REAL_RAT_REDUCE_CONV];
561 MAP_EVERY (fun t -> MP_TAC(SPEC t REAL_NUM_ROUND))
562 [`&n / &m`; `&p / &m`; `&q / &m`; `&r / &m`] THEN
563 SIMP_TAC[REAL_LE_DIV; REAL_POS] THEN
564 MAP_EVERY (fun t -> DISCH_THEN(X_CHOOSE_TAC t))
565 [`r':num`; `q':num`; `p':num`; `n':num`] THEN
566 MAP_EVERY EXISTS_TAC [`n':num`; `p':num`; `q':num`; `r':num`] THEN
568 MATCH_MP_TAC(REAL_ARITH
569 `!m. a <= m /\ b <= m /\ c <= m /\ d <= m /\
570 ~((a = m) /\ (b = m) /\ (c = m) /\ (d = m)) /\
572 ==> a + b + c + d < &1`) THEN
573 EXISTS_TAC `(&1 / &2) pow 2` THEN
574 ONCE_REWRITE_TAC[SYM(SPEC `a - b` REAL_POW2_ABS)] THEN
575 ASM_SIMP_TAC[REAL_POW_LE2; REAL_ABS_POS; REAL_LE_DIV; REAL_POS] THEN
576 CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN
577 REWRITE_TAC[REAL_POW_2; REAL_ARITH
578 `(a * a = b * b) <=> ((a + b) * (a - b) = &0)`] THEN
579 REWRITE_TAC[REAL_ENTIRE] THEN
580 SIMP_TAC[REAL_ARITH `&0 <= x /\ &0 < y ==> ~(x + y = &0)`;
581 REAL_ABS_POS; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
582 REWRITE_TAC[REAL_SUB_0] THEN
583 FIRST_ASSUM(MP_TAC o check (is_neg o concl)) THEN
584 REWRITE_TAC[TAUT `~b ==> ~a <=> a ==> b`] THEN
585 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN
586 (MP_TAC o MATCH_MP REAL_RAT_ABS_MIDDLE)) THEN MESON_TAC[];
588 FIRST_X_ASSUM(K ALL_TAC o check (is_forall o concl)) THEN
589 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
590 MAP_EVERY X_GEN_TAC [`n':num`; `p':num`; `q':num`; `r':num`] THEN
592 ABBREV_TAC `s = &n - &m * &n'` THEN
593 ABBREV_TAC `t = &p - &m * &p'` THEN
594 ABBREV_TAC `u = &q - &m * &q'` THEN
595 ABBREV_TAC `v = &r - &m * &r'` THEN
596 ABBREV_TAC `N' = n' EXP 2 + p' EXP 2 + q' EXP 2 + r' EXP 2` THEN
597 UNDISCH_TAC `n' EXP 2 + p' EXP 2 + q' EXP 2 + r' EXP 2 = N'` THEN
598 DISCH_THEN(ASSUME_TAC o REWRITE_RULE
599 [GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_POW]) THEN
600 ABBREV_TAC `M = 2 * (n * n' + p * p' + q * q' + r * r')` THEN
601 UNDISCH_TAC `2 * (n * n' + p * p' + q * q' + r * r') = M` THEN
602 DISCH_THEN(ASSUME_TAC o REWRITE_RULE
603 [GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL;
604 GSYM REAL_OF_NUM_POW]) THEN
605 ASM_CASES_TAC `(&n / &m = &n') /\ (&p / &m = &p') /\
606 (&q / &m = &q') /\ (&r / &m = &r')` THENL
607 [MAP_EVERY EXISTS_TAC [`1`; `n':num`; `p':num`; `q':num`; `r':num`] THEN
608 REWRITE_TAC[ARITH_EQ; REAL_DIV_1] THEN CONJ_TAC THENL
609 [UNDISCH_TAC `~(m = 0)` THEN UNDISCH_TAC `~(m = 1)` THEN ARITH_TAC;
611 `(&n / &m) pow 2 + (&p / &m) pow 2 +
612 (&q / &m) pow 2 + (&r / &m) pow 2 = &N`
613 (SUBST1_TAC o SYM) THEN
616 SUBGOAL_THEN `&0 < (&n / &m - &n') pow 2 + (&p / &m - &p') pow 2 +
617 (&q / &m - &q') pow 2 + (&r / &m - &r') pow 2`
619 [MATCH_MP_TAC(REAL_ARITH
620 `&0 <= w /\ &0 <= x /\ &0 <= y /\ &0 <= z /\
621 ~((w = &0) /\ (x = &0) /\ (y = &0) /\ (z = &0))
622 ==> &0 < w + x + y + z`) THEN
623 REWRITE_TAC[REAL_POW_2; REAL_ENTIRE; REAL_LE_SQUARE] THEN
624 ASM_REWRITE_TAC[REAL_SUB_0];
626 FIRST_X_ASSUM(MP_TAC o check (is_disj o concl)) THEN
628 `(&n / &m - &n') pow 2 + (&p / &m - &p') pow 2 +
629 (&q / &m - &q') pow 2 + (&r / &m - &r') pow 2 =
630 (s pow 2 + t pow 2 + u pow 2 + v pow 2) / &m pow 2`
632 [MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `&m pow 2` THEN
633 ASM_SIMP_TAC[REAL_POW_EQ_0; REAL_DIV_RMUL; REAL_OF_NUM_EQ] THEN
634 REWRITE_TAC[REAL_ADD_RDISTRIB; GSYM REAL_POW_MUL; REAL_SUB_RDISTRIB] THEN
635 ASM_SIMP_TAC[REAL_POW_EQ_0; REAL_DIV_RMUL; REAL_OF_NUM_EQ] THEN
636 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
637 SUBGOAL_THEN `(&n / &m - &n') pow 2 + (&p / &m - &p') pow 2 +
638 (&q / &m - &q') pow 2 + (&r / &m - &r') pow 2 =
639 (&N + &N') - &M / &m`
641 [MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `&m pow 2` THEN
642 ASM_SIMP_TAC[REAL_POW_EQ_0; REAL_DIV_RMUL; REAL_OF_NUM_EQ] THEN
643 REWRITE_TAC[GSYM(ASSUME `(&n / &m) pow 2 + (&p / &m) pow 2 +
644 (&q / &m) pow 2 + (&r / &m) pow 2 = &N`);
645 GSYM(ASSUME `&n' pow 2 + &p' pow 2 + &q' pow 2 + &r' pow 2 = &N'`);
647 `&2 * (&n * &n' + &p * &p' + &q * &q' + &r * &r') = &M`)] THEN
648 REWRITE_TAC[REAL_ADD_RDISTRIB; GSYM REAL_POW_MUL; REAL_SUB_RDISTRIB] THEN
649 REWRITE_TAC[REAL_POW_2; REAL_MUL_ASSOC] THEN
650 SIMP_TAC[REAL_DIV_RMUL; REAL_OF_NUM_EQ; ASSUME `~(m = 0)`] THEN
651 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
652 SIMP_TAC[REAL_DIV_RMUL; REAL_OF_NUM_EQ; ASSUME `~(m = 0)`] THEN
653 REAL_ARITH_TAC; ALL_TAC] THEN
654 ASM_REWRITE_TAC[] THEN
655 REWRITE_TAC[REAL_ARITH `(a + b) - c < &1 <=> (a + b) - &1 < c`;
656 REAL_ARITH `((a + b) - c = &1) <=> ((a + b) - &1 = c)`;
657 REAL_ARITH `&0 < a - b <=> b < a`] THEN
658 SIMP_TAC[REAL_LT_LDIV_EQ; REAL_LT_RDIV_EQ; REAL_EQ_RDIV_EQ; REAL_OF_NUM_LT;
659 ARITH_RULE `0 < n <=> ~(n = 0)`; ASSUME `~(m = 0)`] THEN
660 REWRITE_TAC[REAL_ARITH `(a - &1) * m < M <=> a * m - M < m`;
661 REAL_ARITH `((a - &1) * m = M) <=> (a * m - M = m)`] THEN
662 REPEAT DISCH_TAC THEN
663 UNDISCH_TAC `(&N + &N') - &M / &m =
664 (s pow 2 + t pow 2 + u pow 2 + v pow 2) / &m pow 2` THEN
665 ASM_SIMP_TAC[REAL_EQ_RDIV_EQ; REAL_POW_LT; REAL_OF_NUM_LT;
666 ARITH_RULE `0 < a <=> ~(a = 0)`] THEN
667 REWRITE_TAC[REAL_POW_2; REAL_SUB_RDISTRIB; REAL_MUL_ASSOC] THEN
668 ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_OF_NUM_EQ; GSYM REAL_POW_2] THEN
669 ABBREV_TAC `m':num = (N + N') * m - M` THEN
670 SUBGOAL_THEN `(&N + &N') * &m - &M = &m'`
671 (fun th -> SUBST_ALL_TAC th THEN ASSUME_TAC th)
673 [EXPAND_TAC "m'" THEN
674 REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL] THEN
675 MATCH_MP_TAC REAL_OF_NUM_SUB THEN
676 REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_ADD; GSYM
677 REAL_OF_NUM_MUL] THEN
678 ASM_SIMP_TAC[REAL_LT_IMP_LE]; ALL_TAC] THEN
679 ASM_REWRITE_TAC[GSYM REAL_SUB_RDISTRIB] THEN
680 DISCH_THEN(ASSUME_TAC o GSYM) THEN
681 SUBGOAL_THEN `~(m' = 0)` ASSUME_TAC THENL
682 [REWRITE_TAC[GSYM REAL_OF_NUM_EQ] THEN
683 REWRITE_TAC[GSYM(ASSUME `(&N + &N') * &m - &M = &m'`)] THEN
684 MATCH_MP_TAC(REAL_ARITH `b < a ==> ~(a - b = &0)`) THEN
685 ASM_REWRITE_TAC[]; ALL_TAC] THEN
687 `!z. (&n' + s * z) pow 2 + (&p' + t * z) pow 2 +
688 (&q' + u * z) pow 2 + (&r' + v * z) pow 2 - &N =
689 (&m * z - &1) * (&m' * z + &N - &N')`
691 [GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
692 EXISTS_TAC `&m * &m' * z pow 2 + (&M - &2 * &m * &N') * z + &N' - &N` THEN
694 [REWRITE_TAC[REAL_POW_2; REAL_ARITH
695 `(n + s * z) * (n + s * z) + (p + t * z) * (p + t * z) +
696 (q + u * z) * (q + u * z) + (r + v * z) * (r + v * z) - N =
697 (s * s + t * t + u * u + v * v) * (z * z) +
698 (&2 * (n * s + p * t + q * u + r * v)) * z +
699 ((n * n + p * p + q * q + r * r) - N)`] THEN
700 ASM_REWRITE_TAC[GSYM REAL_POW_2] THEN
701 MATCH_MP_TAC(REAL_ARITH
702 `(a = c) /\ (b = d) ==> (a + b + n - m = c + d + n - m)`) THEN
703 CONJ_TAC THENL [REWRITE_TAC[REAL_MUL_AC]; ALL_TAC] THEN
704 AP_THM_TAC THEN AP_TERM_TAC THEN
705 REWRITE_TAC[GSYM(ASSUME
706 `&n' pow 2 + &p' pow 2 + &q' pow 2 + &r' pow 2 = &N'`);
708 `&2 * (&n * &n' + &p * &p' + &q * &q' + &r * &r') = &M`)] THEN
709 MAP_EVERY EXPAND_TAC ["s"; "t"; "u"; "v"] THEN
710 REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC;
711 REWRITE_TAC[REAL_POW_2; REAL_ARITH
712 `(m * z - &1) * (m' * z + nn) = m * m' * z * z +
713 (m * z * nn - m' * z) - nn`] THEN
714 REWRITE_TAC[REAL_EQ_ADD_LCANCEL] THEN
715 REWRITE_TAC[REAL_ARITH `(a + n' - n = b - (n - n')) <=> (a = b)`] THEN
716 REWRITE_TAC[REAL_ARITH `a * z * b - c * z = (a * b - c) * z`] THEN
717 AP_THM_TAC THEN AP_TERM_TAC THEN
718 REWRITE_TAC[GSYM(ASSUME `(&N + &N') * &m - &M = &m'`)] THEN
721 ABBREV_TAC `w = &n' + s * (&N' - &N) / &m'` THEN
722 ABBREV_TAC `x = &p' + t * (&N' - &N) / &m'` THEN
723 ABBREV_TAC `y = &q' + u * (&N' - &N) / &m'` THEN
724 ABBREV_TAC `z = &r' + v * (&N' - &N) / &m'` THEN
725 SUBGOAL_THEN `w pow 2 + x pow 2 + y pow 2 + z pow 2 = &N`
726 (SUBST1_TAC o SYM) THENL
727 [MAP_EVERY EXPAND_TAC ["w"; "x"; "y"; "z"] THEN
728 ONCE_REWRITE_TAC[REAL_ARITH
729 `(a + b + c + d = e) <=> (a + b + c + d - e = &0)`] THEN
730 FIRST_ASSUM(SUBST1_TAC o SPEC `(&N' - &N) / &m'`) THEN
731 REWRITE_TAC[REAL_ENTIRE] THEN DISJ2_TAC THEN
732 ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ] THEN REAL_ARITH_TAC;
734 FIRST_X_ASSUM(DISJ_CASES_THEN2 ASSUME_TAC MP_TAC) THENL
735 [EXISTS_TAC `m':num` THEN
737 `?a b c d. (abs(&n' * &m' + s * (&N' - &N)) = &a) /\
738 (abs(&p' * &m' + t * (&N' - &N)) = &b) /\
739 (abs(&q' * &m' + u * (&N' - &N)) = &c) /\
740 (abs(&r' * &m' + v * (&N' - &N)) = &d)`
742 [MAP_EVERY EXPAND_TAC ["s"; "t"; "u"; "v"] THEN
743 REWRITE_TAC[RIGHT_EXISTS_AND_THM; LEFT_EXISTS_AND_THM] THEN
744 MESON_TAC[REAL_INTEGER_CLOSURES]; ALL_TAC] THEN
745 MAP_EVERY (fun t -> MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC t)
746 [`a:num`; `b:num`; `c:num`; `d:num`] THEN
747 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN
748 RULE_ASSUM_TAC(REWRITE_RULE[REAL_OF_NUM_LT]) THEN
749 REWRITE_TAC[REAL_POW_DIV; REAL_POW2_ABS] THEN
750 REWRITE_TAC[GSYM REAL_POW_DIV] THEN
751 REWRITE_TAC[real_div; REAL_ADD_RDISTRIB; GSYM REAL_MUL_ASSOC] THEN
752 ASM_SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ] THEN
753 REWRITE_TAC[GSYM real_div; REAL_MUL_RID] THEN
754 ASM_REWRITE_TAC[]; ALL_TAC] THEN
755 REWRITE_TAC[REAL_OF_NUM_EQ] THEN
756 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC MP_TAC)) THEN
758 SUBGOAL_THEN `?n. abs((&N' - &N) / &2) = &n` ASSUME_TAC THENL
759 [REWRITE_TAC[GSYM(ASSUME
760 `&n' pow 2 + &p' pow 2 + &q' pow 2 + &r' pow 2 = &N'`)] THEN
761 REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_ADD] THEN
762 SUBGOAL_THEN `EVEN(n' EXP 2 + p' EXP 2 + q' EXP 2 + r' EXP 2) =
765 [FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
766 REWRITE_TAC[EVEN_ADD; EVEN_EXP; ARITH_EQ];
768 DISJ_CASES_THEN MP_TAC (TAUT `EVEN(N) \/ ~EVEN(N)`) THEN SIMP_TAC[] THEN
769 REWRITE_TAC[NOT_EVEN; EVEN_EXISTS; ODD_EXISTS] THEN
770 REPEAT(DISCH_THEN(CHOOSE_THEN SUBST1_TAC)) THEN
771 REWRITE_TAC[GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_MUL] THEN
772 REWRITE_TAC[REAL_ARITH `(&2 * x + &1) - (&2 * y + &1) = &2 * (x - y)`] THEN
773 REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN
774 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
775 REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
776 CONV_TAC REAL_RAT_REDUCE_CONV THEN
777 REWRITE_TAC[REAL_MUL_RID] THEN MESON_TAC[REAL_INTEGER_CLOSURES];
779 EXISTS_TAC `1` THEN REWRITE_TAC[ARITH_EQ] THEN
781 `?a b c d. (abs(&n' + s * (&N' - &N) / &2) = &a) /\
782 (abs(&p' + t * (&N' - &N) / &2) = &b) /\
783 (abs(&q' + u * (&N' - &N) / &2) = &c) /\
784 (abs(&r' + v * (&N' - &N) / &2) = &d)`
786 [MAP_EVERY EXPAND_TAC ["s"; "t"; "u"; "v"] THEN
787 REWRITE_TAC[RIGHT_EXISTS_AND_THM; LEFT_EXISTS_AND_THM] THEN
788 UNDISCH_TAC `?n. abs ((&N' - &N) / &2) = &n` THEN
789 MESON_TAC[REAL_INTEGER_CLOSURES]; ALL_TAC] THEN
790 REWRITE_TAC[ARITH; REAL_DIV_1] THEN
791 MAP_EVERY (fun t -> MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC t)
792 [`a:num`; `b:num`; `c:num`; `d:num`] THEN
793 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN
794 ASM_REWRITE_TAC[REAL_POW2_ABS]);;
796 (* ------------------------------------------------------------------------- *)
797 (* Hence the main result. *)
798 (* ------------------------------------------------------------------------- *)
800 let AUBREY_THM_4 = prove
803 (&a / &q) pow 2 + (&b / &q) pow 2 +
804 (&c / &q) pow 2 + (&d / &q) pow 2 = &N)
805 ==> ?a b c d. &a pow 2 + &b pow 2 + &c pow 2 + &d pow 2 = &N`,
806 GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
807 DISCH_THEN(X_CHOOSE_THEN `m:num` MP_TAC) THEN
808 ASM_CASES_TAC `m = 1` THENL
809 [ASM_REWRITE_TAC[REAL_DIV_1; ARITH_EQ] THEN MESON_TAC[];
810 STRIP_TAC THEN MP_TAC(SPEC `m:num` AUBREY_LEMMA_4) THEN
811 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]]);;
813 (* ------------------------------------------------------------------------- *)
814 (* The algebraic lemma. *)
815 (* ------------------------------------------------------------------------- *)
817 let LAGRANGE_IDENTITY = REAL_ARITH
818 `(w1 pow 2 + x1 pow 2 + y1 pow 2 + z1 pow 2) *
819 (w2 pow 2 + x2 pow 2 + y2 pow 2 + z2 pow 2) =
820 (w1 * w2 - x1 * x2 - y1 * y2 - z1 * z2) pow 2 +
821 (w1 * x2 + x1 * w2 + y1 * z2 - z1 * y2) pow 2 +
822 (w1 * y2 - x1 * z2 + y1 * w2 + z1 * x2) pow 2 +
823 (w1 * z2 + x1 * y2 - y1 * x2 + z1 * w2) pow 2`;;
825 (* ------------------------------------------------------------------------- *)
826 (* Now sum of 4 squares. *)
827 (* ------------------------------------------------------------------------- *)
829 let LAGRANGE_REAL_NUM = prove
830 (`!n. ?w x y z. &n = &w pow 2 + &x pow 2 + &y pow 2 + &z pow 2`,
832 (`(?a. abs(w) = &a) /\ (?b. abs(x) = &b) /\
833 (?c. abs(y) = &c) /\ (?d. abs(z) = &d)
834 ==> ?a b c d. w pow 2 + x pow 2 + y pow 2 + z pow 2 =
835 &a pow 2 + &b pow 2 + &c pow 2 + &d pow 2`,
836 STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
837 ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ABS_NUM] THEN
839 MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
840 ASM_CASES_TAC `n = 0` THENL
841 [REPEAT(EXISTS_TAC `0`) THEN ASM_REWRITE_TAC[] THEN
842 CONV_TAC REAL_RAT_REDUCE_CONV;
844 ASM_CASES_TAC `n = 1` THENL
845 [EXISTS_TAC `1` THEN REPEAT(EXISTS_TAC `0`) THEN
846 ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV;
848 FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_FACTOR) THEN
849 DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
850 UNDISCH_TAC `p divides n` THEN REWRITE_TAC[divides] THEN
851 DISCH_THEN(X_CHOOSE_THEN `m:num` MP_TAC) THEN
852 ASM_CASES_TAC `m = 1` THENL
854 DISCH_THEN SUBST_ALL_TAC THEN
855 FIRST_X_ASSUM(fun th ->
856 MP_TAC(SPEC `p:num` th) THEN MP_TAC(SPEC `m:num` th)) THEN
857 ONCE_REWRITE_TAC[ARITH_RULE `m < p * m <=> 1 * m < p * m`] THEN
858 REWRITE_TAC[LT_MULT_RCANCEL] THEN
859 ONCE_REWRITE_TAC[ARITH_RULE `p < p * m <=> p * 1 < p * m`] THEN
860 REWRITE_TAC[LT_MULT_LCANCEL] THEN
861 UNDISCH_TAC `~(p * m = 0)` THEN REWRITE_TAC[MULT_EQ_0] THEN
862 ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[] THEN
863 ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[] THEN
864 SUBGOAL_THEN `~(p = 1)` ASSUME_TAC THENL
865 [ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN
866 ASM_REWRITE_TAC[ARITH_RULE `1 < x <=> ~(x = 0) /\ ~(x = 1)`] THEN
867 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
868 MAP_EVERY X_GEN_TAC [`w1:num`; `x1:num`; `y1:num`; `z1:num`] THEN
870 MAP_EVERY X_GEN_TAC [`w2:num`; `x2:num`; `y2:num`; `z2:num`] THEN
871 DISCH_TAC THEN ASM_REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
872 REWRITE_TAC[LAGRANGE_IDENTITY] THEN
873 MATCH_MP_TAC lemma THEN REWRITE_TAC[REAL_OF_NUM_MUL] THEN
874 MESON_TAC[REAL_INTEGER_CLOSURES]] THEN
875 UNDISCH_TAC `m = 1` THEN DISCH_THEN SUBST_ALL_TAC THEN
876 REWRITE_TAC[MULT_CLAUSES] THEN DISCH_THEN SUBST_ALL_TAC THEN
877 FIRST_ASSUM(MP_TAC o MATCH_MP LAGRANGE_LEMMA) THEN
878 DISCH_THEN(MP_TAC o SPEC `1 EXP 2 + 0 EXP 2`) THEN
879 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
880 MAP_EVERY X_GEN_TAC [`q:num`; `x:num`; `y:num`] THEN STRIP_TAC THEN
881 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN MATCH_MP_TAC AUBREY_THM_4 THEN
882 SUBGOAL_THEN `q * p < p EXP 2` MP_TAC THENL
883 [ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN
884 MATCH_MP_TAC(ARITH_RULE
885 `(2 * x) * (2 * x) <= p * p /\ (2 * y) * (2 * y) <= p * p /\
887 ==> x * x + y * y + 1 < p * p`) THEN
888 REPEAT CONJ_TAC THEN MATCH_MP_TAC LE_MULT2 THEN ASM_REWRITE_TAC[] THEN
889 MAP_EVERY UNDISCH_TAC [`~(p = 0)`; `~(p = 1)`] THEN ARITH_TAC;
891 REWRITE_TAC[EXP_2; LT_MULT_RCANCEL] THEN ASM_REWRITE_TAC[] THEN
892 DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `q:num`) THEN
893 ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
894 MAP_EVERY X_GEN_TAC [`a:num`; `b:num`; `c:num`; `d:num`] THEN DISCH_TAC THEN
895 SUBGOAL_THEN `~(q = 0)` ASSUME_TAC THENL
896 [DISCH_THEN SUBST_ALL_TAC THEN
897 UNDISCH_TAC `0 * p = x EXP 2 + y EXP 2 + 1 EXP 2 + 0 EXP 2` THEN
898 DISCH_THEN(MP_TAC o SYM) THEN REWRITE_TAC[MULT_CLAUSES; EXP_2] THEN
899 REWRITE_TAC[ADD_EQ_0; ARITH_EQ]; ALL_TAC] THEN
900 SUBGOAL_THEN `&p = &q * &(q * p) / &q pow 2` SUBST1_TAC THENL
901 [REWRITE_TAC[GSYM REAL_OF_NUM_MUL; REAL_MUL_ASSOC; real_div] THEN
902 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
903 REWRITE_TAC[GSYM REAL_POW_2] THEN
904 SIMP_TAC[REAL_MUL_ASSOC; REAL_POW_EQ_0; REAL_MUL_LINV; REAL_MUL_LID;
905 ASSUME `~(q = 0)`; REAL_OF_NUM_EQ];
907 ASM_REWRITE_TAC[] THEN
908 REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_POW] THEN
909 REWRITE_TAC[real_div; REAL_MUL_ASSOC; LAGRANGE_IDENTITY] THEN
910 SUBST1_TAC(SYM(ASSUME
911 `&q = &a pow 2 + &b pow 2 + &c pow 2 + &d pow 2`)) THEN
912 REWRITE_TAC[REAL_ADD_RDISTRIB] THEN
913 REWRITE_TAC[GSYM real_div; GSYM REAL_POW_DIV] THEN
914 EXISTS_TAC `q:num` THEN REWRITE_TAC[ASSUME `~(q = 0)`] THEN
915 REWRITE_TAC[REAL_POW_DIV] THEN
916 REWRITE_TAC[real_div; GSYM REAL_ADD_RDISTRIB] THEN
917 REWRITE_TAC[REAL_EQ_MUL_RCANCEL] THEN
918 REWRITE_TAC[REAL_INV_EQ_0; REAL_POW_EQ_0; REAL_OF_NUM_EQ;
919 ASSUME `~(q = 0)`] THEN
920 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN MATCH_MP_TAC lemma THEN
921 REWRITE_TAC[REAL_OF_NUM_MUL] THEN MESON_TAC[REAL_INTEGER_CLOSURES]);;
923 (* ------------------------------------------------------------------------- *)
924 (* Also prove it for the natural numbers. *)
925 (* ------------------------------------------------------------------------- *)
927 let LAGRANGE_NUM = prove
928 (`!n. ?w x y z. n = w EXP 2 + x EXP 2 + y EXP 2 + z EXP 2`,
929 GEN_TAC THEN MP_TAC(SPEC `n:num` LAGRANGE_REAL_NUM) THEN
930 REWRITE_TAC[REAL_POS; REAL_OF_NUM_POW; REAL_OF_NUM_ADD; REAL_OF_NUM_EQ]);;
932 (* ------------------------------------------------------------------------- *)
933 (* And for the integers. *)
934 (* ------------------------------------------------------------------------- *)
938 let LAGRANGE_INT = prove
939 (`!a. &0 <= a <=> ?w x y z. a = w pow 2 + x pow 2 + y pow 2 + z pow 2`,
940 GEN_TAC THEN EQ_TAC THENL
941 [SPEC_TAC(`a:int`,`a:int`) THEN REWRITE_TAC[GSYM INT_FORALL_POS] THEN
942 X_GEN_TAC `n:num` THEN MP_TAC(SPEC `n:num` LAGRANGE_REAL_NUM) THEN
943 REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
944 SIMP_TAC[GSYM INT_OF_NUM_EQ; GSYM INT_OF_NUM_POW; GSYM INT_OF_NUM_ADD] THEN
946 STRIP_TAC THEN ASM_SIMP_TAC[INT_LE_SQUARE; INT_LE_ADD; INT_POW_2]]);;