1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Author: Thomas C. Hales *)
6 (* ========================================================================== *)
13 module Basics = struct
19 let BETA_ORDERED_PAIR_THM = prove_by_refinement(
21 ((\ ( u, v). g u v) x = g (FST x) (SND x))`,
25 INTRO_TAC (GSYM PAIR) [`x`];
26 DISCH_THEN SUBST1_TAC;
27 BY(REWRITE_TAC[GABS_DEF;GEQ_DEF])
33 let SURJ_IMAGE = prove_by_refinement(
34 `!(f:A->B) a b. SURJ f a b ==> (b = (IMAGE f a))`,
37 REWRITE_TAC[SURJ;IMAGE];
38 REPEAT WEAKER_STRIP_TAC;
39 REWRITE_TAC[EXTENSION;IN_ELIM_THM];
45 let SURJ_FINITE = prove_by_refinement(
46 `!a b (f:A->B). FINITE a /\ (SURJ f a b) ==> FINITE b`,
49 ASM_MESON_TAC[SURJ_IMAGE;FINITE_IMAGE]
53 let BIJ_INVERSE = prove_by_refinement(
54 `!a b (f:A->B). (SURJ f a b) ==> (?(g:B->A). (INJ g b a))`,
57 REPEAT WEAKER_STRIP_TAC;
58 TYPIFY `!y. ?u. ((y IN b) ==> ((u IN a) /\ ((f:A->B) u = y)))` (C SUBGOAL_THEN ASSUME_TAC);
59 BY(ASM_MESON_TAC[SURJ]);
60 FIRST_X_ASSUM (MP_TAC o (REWRITE_RULE[SKOLEM_THM]));
61 REPEAT WEAKER_STRIP_TAC;
69 let BIJ_SUM = prove_by_refinement(
70 `!(A:A->bool) (B:B->bool) f ab.
71 BIJ ab A B ==> (sum A (f o ab) = sum B f)`,
75 BY(ASM_MESON_TAC[ SUM_IMAGE ; SURJ_IMAGE ])
81 let EL_EXPLICIT = prove_by_refinement(
82 `!h t. EL 0 (CONS (h:a) t) = h /\
83 EL 1 (CONS h t) = EL 0 t /\
84 EL 2 (CONS h t) = EL 1 t /\
85 EL 3 (CONS h t) = EL 2 t /\
86 EL 4 (CONS h t) = EL 3 t /\
87 EL 5 (CONS h t) = EL 4 t /\
88 EL 6 (CONS h t) = EL 5 t`,
91 BY(REWRITE_TAC[EL;HD;TL;arith `6 = SUC 5 /\ 5 = SUC 4 /\ 4 = SUC 3 /\ 3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`])
95 let LENGTH1 = prove_by_refinement(
96 `!ul:(A) list. LENGTH ul = 1 ==> ul = [EL 0 ul]`,
99 REWRITE_TAC[LENGTH_EQ_CONS;arith `1 = SUC 0`;LENGTH_EQ_NIL];
100 REPEAT WEAK_STRIP_TAC;
101 BY(ASM_REWRITE_TAC[EL;HD])
105 let LENGTH2 = prove_by_refinement(
106 `!ul:(A) list. LENGTH ul = 2 ==> ul = [EL 0 ul;EL 1 ul]`,
109 REWRITE_TAC[LENGTH_EQ_CONS;arith `2 = SUC 1`];
110 REPEAT WEAK_STRIP_TAC;
112 FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH1));
113 BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;TL])
117 let LENGTH3 = prove_by_refinement(
118 `!(ul:(A)list). LENGTH ul = 3 ==> ul = [EL 0 ul; EL 1 ul; EL 2 ul]`,
121 REWRITE_TAC[LENGTH_EQ_CONS;arith `3 = SUC 2`];
122 REPEAT WEAK_STRIP_TAC;
124 FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH2));
125 BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;arith `2 = SUC 1`;TL])
129 let LENGTH4 = prove_by_refinement(
130 `!(ul:(A)list). LENGTH ul = 4 ==> ul = [EL 0 ul; EL 1 ul; EL 2 ul; EL 3 ul]`,
133 REWRITE_TAC[LENGTH_EQ_CONS;arith `4 = SUC 3`];
134 REPEAT WEAK_STRIP_TAC;
136 FIRST_X_ASSUM (unlist ONCE_REWRITE_TAC o (MATCH_MP LENGTH3));
137 BY(REWRITE_TAC[EL;HD;arith `1 = SUC 0`;arith `2 = SUC 1`;arith `3 = SUC 2`;TL])
141 let set_of_list2_explicit = prove_by_refinement(
142 `!(a:A) b. set_of_list [a;b] = {a,b}`,
145 BY(REWRITE_TAC[set_of_list])
149 let set_of_list2 = prove_by_refinement(
150 `!(ul:(A) list). LENGTH ul = 2 ==> set_of_list ul = {EL 0 ul, EL 1 ul}`,
153 REPEAT WEAK_STRIP_TAC;
154 FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH2));
155 ABBREV_TAC `a:A = EL 0 ul`;
156 ABBREV_TAC `b:A = EL 1 ul`;
157 DISCH_THEN SUBST1_TAC;
158 BY(REWRITE_TAC[set_of_list])
162 let set_of_list3_explicit = prove_by_refinement(
163 `!(a:A) b c. set_of_list [a;b;c] = {a,b,c}`,
166 BY(REWRITE_TAC[set_of_list])
170 let set_of_list3 = prove_by_refinement(
171 `!(ul:(A) list). LENGTH ul = 3 ==> set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul}`,
174 REPEAT WEAK_STRIP_TAC;
175 FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH3));
176 ABBREV_TAC `a:A = EL 0 ul`;
177 ABBREV_TAC `b:A = EL 1 ul`;
178 ABBREV_TAC `c:A = EL 2 ul`;
179 DISCH_THEN SUBST1_TAC;
180 BY(REWRITE_TAC[set_of_list])
184 let set_of_list4_explicit = prove_by_refinement(
185 `!(a:A) b c d. set_of_list [a;b;c;d] = {a,b,c,d}`,
188 BY(REWRITE_TAC[set_of_list])
192 let set_of_list4 = prove_by_refinement(
193 `!(ul:(A) list). LENGTH ul = 4 ==> set_of_list ul = {EL 0 ul, EL 1 ul, EL 2 ul, EL 3 ul}`,
196 REPEAT WEAK_STRIP_TAC;
197 FIRST_X_ASSUM (MP_TAC o (MATCH_MP LENGTH4));
198 ABBREV_TAC `a:A = EL 0 ul`;
199 ABBREV_TAC `b:A = EL 1 ul`;
200 ABBREV_TAC `c:A = EL 2 ul`;
201 ABBREV_TAC `d:A = EL 3 ul`;
202 DISCH_THEN SUBST1_TAC;
203 BY(REWRITE_TAC[set_of_list])
207 let INITIAL_SUBLIST_NIL = prove(`!(zl:(A)list). initial_sublist [] zl`,
208 REWRITE_TAC[Sphere.INITIAL_SUBLIST; APPEND] THEN MESON_TAC[]);;
210 let INITIAL_SUBLIST_CONS = prove_by_refinement(
211 `!(a:A) b x y. initial_sublist (CONS a x) (CONS b y) <=> (a = b) /\ initial_sublist x y`,
214 REWRITE_TAC[Sphere.INITIAL_SUBLIST];
215 REPEAT WEAKER_STRIP_TAC;
217 REWRITE_TAC[CONS_11];
222 let INITIAL_SUBLIST_TRANS = prove(`!(xl:(A)list) yl zl. initial_sublist xl yl /\ initial_sublist yl zl ==> initial_sublist xl zl`,
223 REWRITE_TAC[Sphere.INITIAL_SUBLIST] THEN
224 REPEAT STRIP_TAC THEN
225 ASM_MESON_TAC[APPEND_ASSOC]);;
228 (* truncate simplex *)
231 let BUTLAST_INITIAL_SUBLIST = prove(`!ul:(A)list. 1 <= LENGTH ul ==> initial_sublist (BUTLAST ul) ul`,
232 REPEAT STRIP_TAC THEN
233 MP_TAC (ISPEC `ul:(A)list` APPEND_BUTLAST_LAST) THEN
234 REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
235 ASM_SIMP_TAC[ARITH_RULE `1 <= a ==> ~(a = 0)`] THEN
236 REWRITE_TAC[Sphere.INITIAL_SUBLIST] THEN
238 EXISTS_TAC `[LAST ul:A]` THEN
241 let LENGTH_BUTLAST = prove(`!ul:(A)list. 1 <= LENGTH ul ==> LENGTH (BUTLAST ul) = LENGTH ul - 1`,
242 REPEAT STRIP_TAC THEN
243 MP_TAC (ISPEC `ul:(A)list` APPEND_BUTLAST_LAST) THEN
244 REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
245 ASM_SIMP_TAC[ARITH_RULE `1 <= a ==> ~(a = 0)`] THEN
246 DISCH_THEN (fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [GSYM th]) THEN
247 REWRITE_TAC[LENGTH_APPEND; LENGTH] THEN
250 let LENGTH_IMP_CONS = prove(`!l:(A)list. 1 <= LENGTH l ==> ?h t. l = CONS h t`,
251 REPEAT STRIP_TAC THEN
252 MP_TAC (ISPECL [`l:(A)list`; `PRE (LENGTH (l:(A)list))`] LENGTH_EQ_CONS) THEN
253 ASM_SIMP_TAC[ARITH_RULE `1 <= n ==> SUC (PRE n) = n`] THEN
255 MAP_EVERY EXISTS_TAC [`h:A`; `t:(A)list`] THEN
258 let INITIAL_SUBLIST_REFL = prove(`!ul. initial_sublist ul ul`, MESON_TAC[Sphere.INITIAL_SUBLIST; APPEND_NIL]);;
260 let TRUNCATE_SIMPLEX_EXISTS = prove_by_refinement(
261 `!k ul:(A)list. k+1 <= LENGTH ul ==> (?vl.
262 LENGTH vl = k+1 /\ initial_sublist vl ul)`,
265 TYPIFY `!r k (ul:(A)list). k + 1 <= LENGTH ul /\ LENGTH ul = r ==> (?vl. LENGTH vl = k + 1 /\ initial_sublist vl ul)` ENOUGH_TO_SHOW_TAC;
268 REPEAT WEAKER_STRIP_TAC;
269 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
270 REPEAT WEAKER_STRIP_TAC;
271 TYPIFY `SUC r = k + 1` ASM_CASES_TAC;
272 TYPIFY `ul` EXISTS_TAC;
273 REWRITE_TAC[INITIAL_SUBLIST_REFL];
274 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
275 FIRST_X_ASSUM (C INTRO_TAC [`k`;`BUTLAST ul`]);
277 INTRO_TAC LENGTH_BUTLAST [`ul`];
278 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
279 REPEAT WEAKER_STRIP_TAC;
280 TYPIFY `vl` EXISTS_TAC;
282 MATCH_MP_TAC INITIAL_SUBLIST_TRANS;
283 TYPIFY `BUTLAST ul` EXISTS_TAC;
285 MATCH_MP_TAC BUTLAST_INITIAL_SUBLIST;
286 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
290 let TRUNCATE_SIMPLEX_PROP = prove_by_refinement(
291 `!k ul:(A)list. k + 1 <= LENGTH ul ==>
292 LENGTH (truncate_simplex k ul) = k + 1 /\ initial_sublist (truncate_simplex k ul) ul`,
295 REPEAT WEAKER_STRIP_TAC;
296 INTRO_TAC TRUNCATE_SIMPLEX_EXISTS [`k`;`ul`];
298 REPEAT WEAKER_STRIP_TAC;
299 REWRITE_TAC[Sphere.TRUNCATE_SIMPLEX];
300 SELECT_TAC THEN ASM_REWRITE_TAC[];
306 let LENGTH_TRUNCATE_SIMPLEX = prove_by_refinement(
307 `!k ul. k + 1 <= LENGTH ul ==> LENGTH (truncate_simplex k ul) = k + 1`,
310 BY(ASM_MESON_TAC[TRUNCATE_SIMPLEX_PROP])
314 let INITIAL_SUBLIST_OF_NIL = prove_by_refinement(
315 `!ul:(A) list. initial_sublist ul [] <=> (ul = [])`,
318 REWRITE_TAC[Sphere.INITIAL_SUBLIST];
319 BY(MESON_TAC[APPEND_EQ_NIL])
323 let INITIAL_SUBLIST_INJ = prove_by_refinement(
324 `!ul:(A) list vl wl. LENGTH ul = LENGTH vl /\ initial_sublist ul wl /\ initial_sublist vl wl ==>
328 TYPIFY `!k (ul:(A) list) vl wl. k = LENGTH ul /\ k = LENGTH vl /\ initial_sublist ul wl /\ initial_sublist vl wl ==> (ul = vl)` ENOUGH_TO_SHOW_TAC;
331 BY(MESON_TAC[LENGTH_EQ_NIL]);
332 REPEAT WEAKER_STRIP_TAC;
333 INTRO_TAC LENGTH_IMP_CONS [`ul`];
334 INTRO_TAC LENGTH_IMP_CONS [`vl`];
336 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
339 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
341 TYPIFY `LENGTH wl = 0` ASM_CASES_TAC;
342 BY(ASM_MESON_TAC[LENGTH_EQ_NIL;INITIAL_SUBLIST_OF_NIL;NOT_CONS_NIL]);
343 INTRO_TAC LENGTH_IMP_CONS [`wl`];
345 BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
346 REPEAT WEAKER_STRIP_TAC;
347 ASM_REWRITE_TAC[CONS_11];
349 REPEAT (FIRST_X_ASSUM_ST `initial_sublist` MP_TAC);
350 ASM_REWRITE_TAC[INITIAL_SUBLIST_CONS];
351 REPEAT WEAKER_STRIP_TAC;
352 FIRST_X_ASSUM (C INTRO_TAC [`t`;`t'`;`t''`]);
355 REPEAT (FIRST_X_ASSUM_ST `LENGTH` MP_TAC);
356 ASM_REWRITE_TAC[LENGTH;SUC_INJ];
359 FIRST_X_ASSUM_ST `~` MP_TAC;
360 BY(ASM_REWRITE_TAC[])
364 let TRUNCATE_SIMPLEX_UNIQUE = prove_by_refinement(
365 `!k ul:(A) list vl. k+1 <= LENGTH ul /\ LENGTH vl = k+ 1 /\ initial_sublist vl ul ==>
366 vl = truncate_simplex k ul`,
369 BY(ASM_MESON_TAC[INITIAL_SUBLIST_INJ;TRUNCATE_SIMPLEX_PROP])
373 let INITIAL_SUBLIST_LENGTH_LE = prove_by_refinement(
374 `!xl:(A)list zl. initial_sublist xl zl ==> LENGTH xl <= LENGTH zl`,
377 REWRITE_TAC[Sphere.INITIAL_SUBLIST];
378 REPEAT WEAKER_STRIP_TAC;
379 ASM_REWRITE_TAC[LENGTH_APPEND];
384 let TRUNCATE_SIMPLEX_INITIAL_SUBLIST = prove_by_refinement(
386 truncate_simplex k zl = xl /\ k + 1 <= LENGTH zl <=>
387 initial_sublist xl zl /\ LENGTH xl = k + 1`,
390 REPEAT WEAKER_STRIP_TAC;
391 MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a = b)`);
393 BY(ASM_MESON_TAC[TRUNCATE_SIMPLEX_PROP]);
394 REPEAT WEAKER_STRIP_TAC;
395 INTRO_TAC TRUNCATE_SIMPLEX_PROP [`k`;`zl`];
397 BY(ASM_MESON_TAC[INITIAL_SUBLIST_LENGTH_LE]);
398 REPEAT WEAKER_STRIP_TAC;
399 TYPIFY `k + 1 <= LENGTH zl` (C SUBGOAL_THEN ASSUME_TAC);
400 BY(ASM_MESON_TAC[INITIAL_SUBLIST_LENGTH_LE]);
403 MATCH_MP_TAC TRUNCATE_SIMPLEX_UNIQUE;
408 let TRUNCATE_SIMPLEX0 = prove_by_refinement(
409 `!(x:A) y. truncate_simplex 0 (CONS x y) = [x]`,
412 REPEAT WEAKER_STRIP_TAC;
413 INTRO_TAC TRUNCATE_SIMPLEX_INITIAL_SUBLIST [`0`;`[x]`;`(CONS x y)`];
414 REWRITE_TAC[LENGTH (* _CONS *);INITIAL_SUBLIST_CONS;INITIAL_SUBLIST_NIL];
415 BY(REWRITE_TAC[arith `SUC 0 = 0 + 1`;arith `0 + 1 <= SUC i`])
419 let LENGTH_TRUNCATE_SIMPLEX = prove_by_refinement(
420 `!k (ul:(A)list). SUC k <= LENGTH ul ==> LENGTH (truncate_simplex k ul) = SUC k`,
423 BY(ASM_MESON_TAC[LENGTH_TRUNCATE_SIMPLEX;arith `SUC k = k + 1`])
427 let TRUNCATE_SIMPLEX_CONS = prove_by_refinement(
428 `!(x:A) y k. SUC k <= LENGTH y ==> truncate_simplex (SUC k) (CONS x y) = CONS x (truncate_simplex k y)`,
431 REPEAT WEAKER_STRIP_TAC;
432 INTRO_TAC TRUNCATE_SIMPLEX_INITIAL_SUBLIST [`SUC k`;`CONS x (truncate_simplex k y)`;`(CONS x y)`];
433 REWRITE_TAC[LENGTH (* _CONS *);INITIAL_SUBLIST_CONS];
434 ASM_SIMP_TAC[arith `SUC k <= n ==> SUC k + 1 <= SUC n`];
435 ASM_SIMP_TAC[ LENGTH_TRUNCATE_SIMPLEX];
437 REWRITE_TAC[arith `SUC (SUC k) = SUC k + 1`];
438 INTRO_TAC TRUNCATE_SIMPLEX_INITIAL_SUBLIST [`k`;`truncate_simplex k y`;`y`];
439 BY(ASM_SIMP_TAC[LENGTH_TRUNCATE_SIMPLEX;arith `k+1 = SUC k`])
443 let TRUNCATE_SIMPLEX_EXPLICIT = prove_by_refinement(
444 `!(x1:A) x2 x3 x4. truncate_simplex 3 [x1;x2;x3;x4] = [x1;x2;x3;x4] /\
445 truncate_simplex 2 [x1;x2;x3;x4] = [x1;x2;x3] /\
446 truncate_simplex 2 [x1;x2;x3] = [x1;x2;x3] /\
447 truncate_simplex 1 [x1;x2;x3;x4] = [x1;x2] /\
448 truncate_simplex 1 [x1;x2;x3] = [x1;x2] /\
449 truncate_simplex 1 [x1;x2] = [x1;x2]`,
452 REPEAT WEAKER_STRIP_TAC;
453 REWRITE_TAC[arith `3 = SUC 2 /\ 2 = SUC 1 /\ 1 = SUC 0`];
454 REPEAT (GMATCH_SIMP_TAC TRUNCATE_SIMPLEX_CONS);
455 REWRITE_TAC[LENGTH;TRUNCATE_SIMPLEX0];
460 let ADD_C_UNIV = prove_by_refinement(
461 `(:A) +_c (:B) = (:A+B)`,
465 REWRITE_TAC[EXTENSION;IN_UNION;IN_UNIV;IN_ELIM_THM];
466 BY(MESON_TAC[sum_CASES])
470 let SUM_HAS_SIZE = prove_by_refinement(
471 `!a b. (:A) HAS_SIZE a /\ (:B) HAS_SIZE b ==>
472 (:A+B) HAS_SIZE (a+b)`,
475 REWRITE_TAC[HAS_SIZE];
476 REPEAT WEAKER_STRIP_TAC;
477 REWRITE_TAC[GSYM ADD_C_UNIV];
479 BY(ASM_MESON_TAC[CARD_ADD_C]);
480 BY(ASM_MESON_TAC[CARD_ADD_FINITE])
484 let DIMINDEX_4 = prove_by_refinement(
485 `dimindex(:2 + 2) = 4`,
488 MATCH_MP_TAC DIMINDEX_UNIQUE;
489 REWRITE_TAC[arith `4 = 2+ 2`];
490 MATCH_MP_TAC SUM_HAS_SIZE;
491 BY(REWRITE_TAC[HAS_SIZE_2])
495 let DIMINDEX_5 = prove_by_refinement(
496 `dimindex(:2 + 3) = 5`,
499 MATCH_MP_TAC DIMINDEX_UNIQUE;
500 REWRITE_TAC[arith `5 = 2+ 3`];
501 REPEAT (GMATCH_SIMP_TAC SUM_HAS_SIZE);
502 BY(REWRITE_TAC[HAS_SIZE_2;HAS_SIZE_3])
506 let DIMINDEX_6 = prove_by_refinement(
507 `dimindex(:3 + 3) = 6`,
510 MATCH_MP_TAC DIMINDEX_UNIQUE;
511 REWRITE_TAC[arith `6 = 3+ 3`];
512 REPEAT (GMATCH_SIMP_TAC SUM_HAS_SIZE);
513 BY(REWRITE_TAC[HAS_SIZE_2;HAS_SIZE_3])