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
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
|
(* ========================================================================= *)
(* Euler's partition theorem and other elementary partition theorems. *)
(* ========================================================================= *)
loadt "Library/binary.ml";;
(* ------------------------------------------------------------------------- *)
(* Some lemmas. *)
(* ------------------------------------------------------------------------- *)
let NSUM_BOUND_LEMMA = prove
(`!f a b n. nsum(a..b) f = n ==> !i. a <= i /\ i <= b ==> f(i) <= n`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[GSYM IN_NUMSEG] THEN
MATCH_MP_TAC NSUM_POS_BOUND THEN ASM_REWRITE_TAC[LE_REFL; FINITE_NUMSEG]);;
let CARD_EQ_LEMMA = prove
(`!f:A->B g s t.
FINITE s /\ FINITE t /\
(!x. x IN s ==> f(x) IN t) /\
(!y. y IN t ==> g(y) IN s) /\
(!x. x IN s ==> g(f x) = x) /\
(!y. y IN t ==> f(g y) = y)
==> FINITE s /\ FINITE t /\ CARD s = CARD t`,
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC CARD_IMAGE_INJ_EQ THEN
EXISTS_TAC `g:B->A` THEN ASM_MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Breaking a number up into 2^something * odd_number. *)
(* ------------------------------------------------------------------------- *)
let index = define
`index n = if n = 0 then 0 else if ODD n then 0 else SUC(index(n DIV 2))`;;
let oddpart = define
`oddpart n = if n = 0 then 0 else if ODD n then n else oddpart(n DIV 2)`;;
let INDEX_ODDPART_WORK = prove
(`!n. n = 2 EXP (index n) * oddpart n /\ (ODD(oddpart n) <=> ~(n = 0))`,
MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
ONCE_REWRITE_TAC[index; oddpart] THEN
ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[ARITH] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH; MULT_CLAUSES] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_ODD]) THEN
SIMP_TAC[EVEN_EXISTS; LEFT_IMP_EXISTS_THM; EXP; GSYM MULT_ASSOC;
ARITH; ARITH_RULE `(2 * x) DIV 2 = x`; EQ_MULT_LCANCEL] THEN
ASM_MESON_TAC[ARITH_RULE `~(n = 0) /\ n = 2 * m ==> m < n /\ ~(m = 0)`]);;
let INDEX_ODDPART_DECOMPOSITION = prove
(`!n. n = 2 EXP (index n) * oddpart n`,
MESON_TAC[INDEX_ODDPART_WORK]);;
let ODD_ODDPART = prove
(`!n. ODD(oddpart n) <=> ~(n = 0)`,
MESON_TAC[INDEX_ODDPART_WORK]);;
let ODDPART_LE = prove
(`!n. oddpart n <= n`,
GEN_TAC THEN GEN_REWRITE_TAC RAND_CONV [INDEX_ODDPART_DECOMPOSITION] THEN
MATCH_MP_TAC(ARITH_RULE `1 * x <= y * x ==> x <= y * x`) THEN
REWRITE_TAC[LE_MULT_RCANCEL; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
REWRITE_TAC[EXP_EQ_0; ARITH]);;
let INDEX_ODDPART_UNIQUE = prove
(`!i m i' m'. ODD m /\ ODD m'
==> (2 EXP i * m = 2 EXP i' * m' <=> i = i' /\ m = m')`,
REWRITE_TAC[ODD_EXISTS; ADD1] THEN
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[GSYM NUMPAIR; NUMPAIR_INJ] THEN
ARITH_TAC);;
let INDEX_ODDPART = prove
(`!i m. ODD m ==> index(2 EXP i * m) = i /\ oddpart(2 EXP i * m) = m`,
REPEAT GEN_TAC THEN STRIP_TAC THEN
MP_TAC(SPECL [`i:num`; `m:num`; `index(2 EXP i * m)`; `oddpart(2 EXP i * m)`]
INDEX_ODDPART_UNIQUE) THEN
REWRITE_TAC[GSYM INDEX_ODDPART_DECOMPOSITION; ODD_ODDPART] THEN
ASM_REWRITE_TAC[MULT_EQ_0; EXP_EQ_0; ARITH] THEN ASM_MESON_TAC[ODD]);;
(* ------------------------------------------------------------------------- *)
(* Partitions. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("partitions",(12,"right"));;
let partitions = new_definition
`p partitions n <=> (!i. ~(p i = 0) ==> 1 <= i /\ i <= n) /\
nsum(1..n) (\i. p(i) * i) = n`;;
let PARTITIONS_BOUND = prove
(`!p n. p partitions n ==> !i. p(i) <= n`,
REWRITE_TAC[GSYM NOT_LT] THEN SIMP_TAC[partitions] THEN REPEAT STRIP_TAC THEN
SUBGOAL_THEN `1 <= i /\ i <= n` STRIP_ASSUME_TAC THENL
[ASM_MESON_TAC[ARITH_RULE `m < n ==> ~(n = 0)`]; ALL_TAC] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
`m = n ==> n < m ==> F`)) THEN
MATCH_MP_TAC LET_TRANS THEN
EXISTS_TAC `nsum(1..n) (\j. if j = i then n else 0)` THEN CONJ_TAC THENL
[ASM_REWRITE_TAC[NSUM_DELTA; IN_NUMSEG; LE_REFL]; ALL_TAC] THEN
MATCH_MP_TAC NSUM_LT THEN REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
CONJ_TAC THENL
[GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[LE_0] THEN
MATCH_MP_TAC LT_IMP_LE;
EXISTS_TAC `i:num` THEN ASM_REWRITE_TAC[]] THEN
MATCH_MP_TAC(ARITH_RULE `n < p /\ p * 1 <= p * k ==> n < p * k`) THEN
ASM_REWRITE_TAC[LE_MULT_LCANCEL]);;
let FINITE_PARTITIONS_LEMMA = prove
(`!m n. FINITE {p | (!i. p(i) <= n) /\ !i. m <= i ==> p(i) = 0}`,
INDUCT_TAC THEN GEN_TAC THENL
[SIMP_TAC[LE_0; TAUT `a /\ b <=> ~(b ==> ~a)`] THEN
SUBGOAL_THEN `{p | !i:num. p i = 0} = {(\n. 0)}`
(fun th -> SIMP_TAC[th; FINITE_RULES]) THEN
REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING] THEN REWRITE_TAC[FUN_EQ_THM];
ALL_TAC] THEN
SUBGOAL_THEN
`{p | (!i. p i <= n) /\ (!i. SUC m <= i ==> p i = 0)} =
IMAGE (\(a,p) j. if j = m then a else p(j))
{a,p | a IN 0..n /\
p IN {p | (!i. p i <= n) /\ (!i. m <= i ==> p i = 0)}}`
(fun t -> ASM_SIMP_TAC[t; FINITE_IMAGE; FINITE_PRODUCT; FINITE_NUMSEG]) THEN
REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; EXISTS_PAIR_THM] THEN
CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN X_GEN_TAC `p:num->num` THEN
EQ_TAC THENL
[STRIP_TAC THEN MAP_EVERY EXISTS_TAC
[`(p:num->num) m`; `\i:num. if i = m then 0 else p i`] THEN
REWRITE_TAC[FUN_EQ_THM] THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
ONCE_REWRITE_TAC[CONJ_SYM] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
REWRITE_TAC[PAIR_EQ; UNWIND_THM1; GSYM CONJ_ASSOC; IN_NUMSEG; LE_0] THEN
ASM_MESON_TAC[LE; ARITH_RULE `m <= i /\ ~(i = m) ==> SUC m <= i`];
REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`a:num`; `q:num->num`] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
POP_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SYM) THEN
REWRITE_TAC[PAIR_EQ] THEN DISCH_THEN(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
ASM_MESON_TAC[ARITH_RULE `SUC m <= i ==> m <= i /\ ~(i = m)`]]);;
let FINITE_PARTITIONS = prove
(`!n. FINITE {p | p partitions n}`,
GEN_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
EXISTS_TAC `{p | (!i. p(i) <= n) /\ (!i. SUC n <= i ==> p(i) = 0)}` THEN
SIMP_TAC[FINITE_PARTITIONS_LEMMA; IN_ELIM_THM; SUBSET; PARTITIONS_BOUND] THEN
REWRITE_TAC[partitions; LE_SUC_LT] THEN MESON_TAC[NOT_LE]);;
let FINITE_SUBSET_PARTITIONS = prove
(`!P n. FINITE {p | p partitions n /\ P p}`,
REPEAT GEN_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
EXISTS_TAC `{p | p partitions n}` THEN
SIMP_TAC[FINITE_PARTITIONS; IN_ELIM_THM; SUBSET]);;
(* ------------------------------------------------------------------------- *)
(* Mappings between "odd only" and "all distinct" partitions. *)
(* ------------------------------------------------------------------------- *)
let odd_of_distinct = new_definition
`odd_of_distinct p =
\i. if ODD i then nsum {j | p(2 EXP j * i) = 1} (\j. 2 EXP j) else 0`;;
let distinct_of_odd = new_definition
`distinct_of_odd p = \i. if (index i) IN bitset (p(oddpart i)) then 1 else 0`;;
(* ------------------------------------------------------------------------- *)
(* The critical properties. *)
(* ------------------------------------------------------------------------- *)
let ODD_ODD_OF_DISTINCT = prove
(`!p i. ~(odd_of_distinct p i = 0) ==> ODD i`,
REWRITE_TAC[odd_of_distinct] THEN MESON_TAC[]);;
let DISTINCT_DISTINCT_OF_ODD = prove
(`!p i. distinct_of_odd p i <= 1`,
REWRITE_TAC[distinct_of_odd] THEN ARITH_TAC);;
let SUPPORT_ODD_OF_DISTINCT = prove
(`!p. (!i. ~(p i = 0) ==> i <= n)
==> !i. ~(odd_of_distinct p i = 0) ==> 1 <= i /\ i <= n`,
REPEAT STRIP_TAC THENL
[ASM_MESON_TAC[ODD; ARITH_RULE `1 <= i <=> ~(i = 0)`; ODD_ODD_OF_DISTINCT];
FIRST_X_ASSUM(MP_TAC o check (is_neg o concl))] THEN
REWRITE_TAC[odd_of_distinct] THEN
ASM_CASES_TAC `i = 0` THEN ASM_REWRITE_TAC[LE_0] THEN
SUBGOAL_THEN `FINITE {j | p (2 EXP j * i) = 1}` ASSUME_TAC THENL
[MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG; SUBSET] THEN X_GEN_TAC `j:num` THEN
REWRITE_TAC[IN_ELIM_THM; LE_0] THEN DISCH_TAC THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 EXP j * i` THEN
ASM_SIMP_TAC[ARITH_EQ] THEN
MATCH_MP_TAC(ARITH_RULE `j < ej /\ ej * 1 <= ej * i ==> j <= ej * i`) THEN
REWRITE_TAC[LT_POW2_REFL; LE_MULT_LCANCEL; EXP_EQ_0; ARITH] THEN
UNDISCH_TAC `~(i = 0)` THEN ARITH_TAC;
SIMP_TAC[ARITH_RULE `~((if p then x else 0) = 0) <=> p /\ ~(x = 0)`] THEN
ASM_SIMP_TAC[NSUM_EQ_0_IFF; EXP_EQ_0; ARITH] THEN
REWRITE_TAC[NOT_FORALL_THM; IN_ELIM_THM] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_TAC `j:num`)) THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 EXP j * i` THEN
ASM_SIMP_TAC[ARITH; ARITH_RULE `i <= j * i <=> 1 * i <= j * i`] THEN
REWRITE_TAC[LE_MULT_RCANCEL; ARITH_RULE `1 <= i <=> ~(i = 0)`] THEN
REWRITE_TAC[EXP_EQ_0; ARITH]]);;
let SUPPORT_DISTINCT_OF_ODD = prove
(`!p. (!i. p(i) * i <= n) /\
(!i. ~(p i = 0) ==> ODD i)
==> !i. ~(distinct_of_odd p i = 0) ==> 1 <= i /\ i <= n`,
REWRITE_TAC[distinct_of_odd] THEN
REWRITE_TAC[ARITH_RULE `(if a then 1 else 0) = 0 <=> ~a`] THEN
GEN_TAC THEN STRIP_TAC THEN X_GEN_TAC `i:num` THEN REPEAT STRIP_TAC THENL
[REWRITE_TAC[ARITH_RULE `1 <= i <=> ~(i = 0)`] THEN
DISCH_THEN SUBST_ALL_TAC THEN
UNDISCH_TAC `index 0 IN bitset (p (oddpart 0))` THEN
REWRITE_TAC[index; oddpart; ARITH] THEN
UNDISCH_THEN `!i. ~(p i = 0) ==> ODD i` (MP_TAC o SPEC `0`) THEN
SIMP_TAC[ARITH; BITSET_0; NOT_IN_EMPTY];
ALL_TAC] THEN
FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP BITSET_BOUND_LEMMA) THEN
MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `p(oddpart i) * oddpart i` THEN
ASM_REWRITE_TAC[] THEN
GEN_REWRITE_TAC LAND_CONV [INDEX_ODDPART_DECOMPOSITION] THEN
ASM_REWRITE_TAC[LE_MULT_RCANCEL]);;
let ODD_OF_DISTINCT_OF_ODD = prove
(`!p. (!i. ~(p(i) = 0) ==> ODD i)
==> odd_of_distinct (distinct_of_odd p) = p`,
REWRITE_TAC[IN_ELIM_THM; odd_of_distinct; distinct_of_odd] THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN
COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
ASM_SIMP_TAC[INDEX_ODDPART] THEN
GEN_REWRITE_TAC RAND_CONV [GSYM BINARYSUM_BITSET] THEN
REWRITE_TAC[binarysum] THEN
AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ]);;
let DISTINCT_OF_ODD_OF_DISTINCT = prove
(`!p. (!i. ~(p i = 0) ==> 1 <= i /\ i <= n) /\ (!i. p(i) <= 1)
==> distinct_of_odd (odd_of_distinct p) = p`,
REWRITE_TAC[distinct_of_odd; odd_of_distinct; IN_ELIM_THM] THEN
REWRITE_TAC[partitions; ODD_ODDPART] THEN REPEAT STRIP_TAC THEN
REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN
ASM_CASES_TAC `i = 0` THEN ASM_REWRITE_TAC[BITSET_0; NOT_IN_EMPTY] THENL
[ASM_MESON_TAC[ARITH_RULE `~(1 <= 0)`]; ALL_TAC] THEN
SUBGOAL_THEN `FINITE {j | p (2 EXP j * oddpart i) = 1}` ASSUME_TAC THENL
[MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG; SUBSET; IN_ELIM_THM] THEN
X_GEN_TAC `j:num` THEN DISCH_TAC THEN REWRITE_TAC[LE_0] THEN
MATCH_MP_TAC(ARITH_RULE `!x. y <= x /\ 1 <= x /\ x <= n ==> y <= n`) THEN
EXISTS_TAC `2 EXP j * oddpart i` THEN ASM_SIMP_TAC[ARITH] THEN
MATCH_MP_TAC(ARITH_RULE `j < ej /\ 1 * ej <= i * ej ==> j <= ej * i`) THEN
REWRITE_TAC[LT_POW2_REFL; LE_MULT_RCANCEL] THEN
ASM_MESON_TAC[ODD_ODDPART; ODD; ARITH_RULE `1 <= n <=> ~(n = 0)`];
ASM_SIMP_TAC[BITSET_BINARYSUM; GSYM binarysum; IN_ELIM_THM] THEN
REWRITE_TAC[GSYM INDEX_ODDPART_DECOMPOSITION] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ] THEN
ASM_MESON_TAC[ARITH_RULE `i <= 1 ==> i = 0 \/ i = 1`]]);;
let NSUM_DISTINCT_OF_ODD = prove
(`!p. (!i. ~(p i = 0) ==> 1 <= i /\ i <= n) /\
(!i. p(i) * i <= n) /\
(!i. ~(p(i) = 0) ==> ODD i)
==> nsum(1..n) (\i. distinct_of_odd p i * i) =
nsum(1..n) (\i. p i * i)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[distinct_of_odd] THEN
GEN_REWRITE_TAC (RAND_CONV o BINDER_CONV o LAND_CONV)
[GSYM BINARYSUM_BITSET] THEN
REWRITE_TAC[binarysum] THEN REWRITE_TAC[GSYM NSUM_RMUL] THEN
SIMP_TAC[NSUM_NSUM_PRODUCT; FINITE_BITSET; FINITE_NUMSEG] THEN
CONV_TAC SYM_CONV THEN ONCE_REWRITE_TAC[GSYM NSUM_SUPPORT] THEN
REWRITE_TAC[support; NEUTRAL_ADD] THEN
SUBGOAL_THEN
`{x | x IN {i,j | i IN 1..n /\ j IN bitset(p i)} /\
~((\(i,j). 2 EXP j * i) x = 0)} =
{i,j | i IN 1..n /\ j IN bitset(p i)}`
SUBST1_TAC THENL
[REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM; IN_ELIM_THM] THEN
CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
REWRITE_TAC[IN_NUMSEG; EXP_EQ_0; MULT_EQ_0; ARITH] THEN
MESON_TAC[ARITH_RULE `~(1 <= 0)`];
ALL_TAC] THEN
SUBGOAL_THEN
`{x | x IN 1 .. n /\
~((if index x IN bitset (p (oddpart x)) then 1 else 0) * x = 0)} =
{i | i IN 1..n /\ (index i) IN bitset (p(oddpart i))}`
SUBST1_TAC THENL
[REWRITE_TAC[EXTENSION; IN_ELIM_THM; MULT_EQ_0] THEN
REWRITE_TAC[IN_NUMSEG; ARITH_RULE `(if p then 1 else 0) = 0 <=> ~p`] THEN
MESON_TAC[ARITH_RULE `~(1 <= 0)`];
ALL_TAC] THEN
MATCH_MP_TAC NSUM_EQ_GENERAL THEN
EXISTS_TAC `\(i,b). 2 EXP b * i` THEN
SIMP_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
CONV_TAC(TOP_DEPTH_CONV GEN_BETA_CONV) THEN
REWRITE_TAC[ARITH_RULE
`(if p then 1 else 0) * x * y = (if p then x * y else 0)`] THEN
GEN_REWRITE_TAC (RAND_CONV o TOP_DEPTH_CONV) [IN_ELIM_THM] THEN
ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> a /\ b /\ (b ==> c)`] THEN
SIMP_TAC[] THEN REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
REWRITE_TAC[FORALL_PAIR_THM; EXISTS_PAIR_THM; IN_ELIM_PAIR_THM] THEN
CONV_TAC(TOP_DEPTH_CONV GEN_BETA_CONV) THEN
REWRITE_TAC[IN_ELIM_THM; IN_NUMSEG] THEN
SUBGOAL_THEN `!i j. j IN bitset(p i) ==> ODD i` ASSUME_TAC THENL
[ASM_MESON_TAC[BITSET_0; NOT_IN_EMPTY]; ALL_TAC] THEN
CONJ_TAC THENL
[X_GEN_TAC `m:num` THEN STRIP_TAC THEN CONJ_TAC THENL
[MAP_EVERY EXISTS_TAC [`oddpart m`; `index m`] THEN
ASM_REWRITE_TAC[GSYM INDEX_ODDPART_DECOMPOSITION] THEN
ASM_MESON_TAC[ODDPART_LE; LE_TRANS; ARITH_RULE `1 <= x <=> ~(x = 0)`;
ODD_ODDPART; ODD];
ASM_MESON_TAC[INDEX_ODDPART_UNIQUE]];
MAP_EVERY X_GEN_TAC [`m:num`; `i:num`] THEN STRIP_TAC THEN
CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[INDEX_ODDPART]] THEN CONJ_TAC THENL
[REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN
REWRITE_TAC[MULT_EQ_0; EXP_EQ_0; ARITH] THEN
ASM_MESON_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`];
ASM_MESON_TAC[BITSET_BOUND_LEMMA; LE_MULT_RCANCEL; LE_TRANS]]]);;
let DISTINCT_OF_ODD = prove
(`!p. p IN {p | p partitions n /\ !i. ~(p(i) = 0) ==> ODD i}
==> (distinct_of_odd p) IN {p | p partitions n /\ !i. p(i) <= 1}`,
GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM; partitions] THEN STRIP_TAC THEN
REWRITE_TAC[DISTINCT_DISTINCT_OF_ODD] THEN CONJ_TAC THENL
[MATCH_MP_TAC SUPPORT_DISTINCT_OF_ODD;
FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
MATCH_MP_TAC NSUM_DISTINCT_OF_ODD] THEN
ASM_REWRITE_TAC[] THEN
X_GEN_TAC `i:num` THEN ASM_CASES_TAC `(p:num->num) i = 0` THEN
ASM_REWRITE_TAC[MULT_CLAUSES; LE_0] THEN
ASM_MESON_TAC[NSUM_BOUND_LEMMA]);;
let ODD_OF_DISTINCT = prove
(`!p. p IN {p | p partitions n /\ !i. p(i) <= 1}
==> (odd_of_distinct p) IN
{p | p partitions n /\ !i. ~(p(i) = 0) ==> ODD i}`,
GEN_TAC THEN REWRITE_TAC[partitions; IN_ELIM_THM] THEN STRIP_TAC THEN
REWRITE_TAC[ODD_ODD_OF_DISTINCT] THEN
CONJ_TAC THENL [ASM_MESON_TAC[SUPPORT_ODD_OF_DISTINCT]; ALL_TAC] THEN
MATCH_MP_TAC EQ_TRANS THEN
EXISTS_TAC `nsum(1..n) (\i. distinct_of_odd(odd_of_distinct p) i * i)` THEN
CONJ_TAC THENL
[ALL_TAC;
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
AP_TERM_TAC THEN ABS_TAC THEN AP_THM_TAC THEN
ASM_MESON_TAC[DISTINCT_OF_ODD_OF_DISTINCT]] THEN
CONV_TAC SYM_CONV THEN MATCH_MP_TAC NSUM_DISTINCT_OF_ODD THEN
REWRITE_TAC[ODD_ODD_OF_DISTINCT] THEN
CONJ_TAC THENL [ASM_MESON_TAC[SUPPORT_ODD_OF_DISTINCT]; ALL_TAC] THEN
X_GEN_TAC `i:num` THEN REWRITE_TAC[odd_of_distinct] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[LE_0; MULT_CLAUSES] THEN
REWRITE_TAC[GSYM NSUM_RMUL] THEN
SUBGOAL_THEN `FINITE {i:num | p(i) = 1}` ASSUME_TAC THENL
[MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `1..n` THEN
REWRITE_TAC[FINITE_NUMSEG; SUBSET; IN_NUMSEG; IN_ELIM_THM] THEN
ASM_MESON_TAC[ARITH_RULE `~(1 = 0)`];
ALL_TAC] THEN
ONCE_REWRITE_TAC[GSYM(REWRITE_CONV[o_DEF]
`(\j. j) o (\j. 2 EXP j * i)`)] THEN
ASM_SIMP_TAC[GSYM NSUM_IMAGE; INDEX_ODDPART_UNIQUE] THEN
MATCH_MP_TAC LE_TRANS THEN
EXISTS_TAC `nsum {i | p(i) = 1} (\j. j)` THEN CONJ_TAC THENL
[MATCH_MP_TAC NSUM_SUBSET_SIMPLE THEN ASM_REWRITE_TAC[] THEN SET_TAC[];
ALL_TAC] THEN
MATCH_MP_TAC LE_TRANS THEN
EXISTS_TAC `nsum {i | p(i) = 1} (\j. p(j) * j)` THEN CONJ_TAC THENL
[MATCH_MP_TAC EQ_IMP_LE THEN MATCH_MP_TAC NSUM_EQ THEN
SIMP_TAC[IN_ELIM_THM; MULT_CLAUSES];
FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
MATCH_MP_TAC NSUM_SUBSET_SIMPLE THEN
REWRITE_TAC[FINITE_NUMSEG; SUBSET; IN_NUMSEG; IN_ELIM_THM] THEN
ASM_MESON_TAC[ARITH_RULE `~(1 = 0)`]]);;
(* ------------------------------------------------------------------------- *)
(* Euler's partition theorem: *)
(* *)
(* The number of partitions into distinct numbers is equal to the number of *)
(* partitions into odd numbers (and there are only finitely many of each). *)
(* ------------------------------------------------------------------------- *)
let EULER_PARTITION_THEOREM = prove
(`FINITE {p | p partitions n /\ !i. p(i) <= 1} /\
FINITE {p | p partitions n /\ !i. ~(p(i) = 0) ==> ODD i} /\
CARD {p | p partitions n /\ !i. p(i) <= 1} =
CARD {p | p partitions n /\ !i. ~(p(i) = 0) ==> ODD i}`,
MATCH_MP_TAC CARD_EQ_LEMMA THEN REWRITE_TAC[FINITE_SUBSET_PARTITIONS] THEN
MAP_EVERY EXISTS_TAC [`odd_of_distinct`; `distinct_of_odd`] THEN
REWRITE_TAC[ODD_OF_DISTINCT; DISTINCT_OF_ODD] THEN
CONJ_TAC THEN X_GEN_TAC `p:num->num` THEN
REWRITE_TAC[IN_ELIM_THM; partitions] THEN STRIP_TAC THENL
[MATCH_MP_TAC DISTINCT_OF_ODD_OF_DISTINCT;
MATCH_MP_TAC ODD_OF_DISTINCT_OF_ODD] THEN
ASM_REWRITE_TAC[]);;
|
