3 let FORSTER_PUZZLE = prove
4 (`(!n. f(n + 1) > f(f(n))) ==> !n. f(n) = n`,
5 REWRITE_TAC[GT; GSYM ADD1] THEN STRIP_TAC THEN
6 SUBGOAL_THEN `!n m. f(m) < n ==> m <= f m` ASSUME_TAC THENL
7 [INDUCT_TAC THEN REWRITE_TAC[LT] THEN
8 INDUCT_TAC THEN ASM_MESON_TAC[LE_0; LE_SUC_LT; LET_TRANS]; ALL_TAC] THEN
9 SUBGOAL_THEN `!n. n <= f n` ASSUME_TAC THENL
10 [ASM_MESON_TAC[LT]; ALL_TAC] THEN
11 SUBGOAL_THEN `!n. f(n) < f(SUC n)` ASSUME_TAC THENL
12 [ASM_MESON_TAC[LET_TRANS]; ALL_TAC] THEN
13 SUBGOAL_THEN `!m n. m < n ==> f(m) < f(n)` ASSUME_TAC THENL
14 [GEN_TAC THEN INDUCT_TAC THEN ASM_MESON_TAC[LT; LT_TRANS]; ALL_TAC] THEN
15 SUBGOAL_THEN `!m n. (f m < f n) <=> m < n` ASSUME_TAC THENL
16 [ASM_MESON_TAC[LT_CASES; LT_ANTISYM; LT_REFL]; ALL_TAC] THEN
17 ASM_MESON_TAC[LE_ANTISYM; LT_SUC_LE]);;
19 (* ------------------------------------------------------------------------- *)
20 (* Alternative; shorter but less transparent and taking longer to run. *)
21 (* ------------------------------------------------------------------------- *)
23 let FORSTER_PUZZLE = prove
24 (`(!n. f(n + 1) > f(f(n))) ==> !n. f(n) = n`,
25 REWRITE_TAC[GT; GSYM ADD1] THEN STRIP_TAC THEN
26 SUBGOAL_THEN `!n m. f(m) < n ==> m <= f m` ASSUME_TAC THENL
27 [INDUCT_TAC THEN REWRITE_TAC[LT] THEN
28 INDUCT_TAC THEN ASM_MESON_TAC[LE_0; LE_SUC_LT; LET_TRANS]; ALL_TAC] THEN
29 SUBGOAL_THEN `!n. n <= f n` ASSUME_TAC THENL
30 [ASM_MESON_TAC[LT]; ALL_TAC] THEN
31 SUBGOAL_THEN `!n. f(n) < f(SUC n)` ASSUME_TAC THENL
32 [ASM_MESON_TAC[LET_TRANS]; ALL_TAC] THEN
33 SUBGOAL_THEN `!m n. m < n ==> f(m) < f(n)` ASSUME_TAC THENL
34 [GEN_TAC THEN INDUCT_TAC THEN ASM_MESON_TAC[LT; LT_TRANS]; ALL_TAC] THEN
35 ASM_MESON_TAC[LE_ANTISYM; LT_CASES; LT_ANTISYM; LT_REFL; LT_SUC_LE]);;
37 (* ------------------------------------------------------------------------- *)
38 (* Robin Milner's proof. *)
39 (* ------------------------------------------------------------------------- *)
41 let FORSTER_PUZZLE = prove
42 (`(!n. f(n + 1) > f(f(n))) ==> !n. f(n) = n`,
43 REWRITE_TAC[GT; GSYM ADD1] THEN STRIP_TAC THEN
44 SUBGOAL_THEN `!m n. m <= f(n + m)` ASSUME_TAC THENL
45 [INDUCT_TAC THEN REWRITE_TAC[LE_0; ADD_CLAUSES; LE_SUC_LT] THEN
46 ASM_MESON_TAC[LET_TRANS; SUB_ADD]; ALL_TAC] THEN
47 SUBGOAL_THEN `!n. f(n) < f(SUC n)` ASSUME_TAC THENL
48 [ASM_MESON_TAC[LET_TRANS; LE_TRANS; ADD_CLAUSES]; ALL_TAC] THEN
49 SUBGOAL_THEN `!m n. m <= n ==> f(m) <= f(n)` ASSUME_TAC THENL
50 [GEN_TAC THEN INDUCT_TAC THEN
51 ASM_MESON_TAC[LE; LE_REFL; LT_IMP_LE; LE_TRANS]; ALL_TAC] THEN
52 ASM_REWRITE_TAC[GSYM LE_ANTISYM] THEN
53 ASM_MESON_TAC[LT_SUC_LE; NOT_LT; ADD_CLAUSES]);;
55 (* ------------------------------------------------------------------------- *)
56 (* A variant of Robin's proof avoiding explicit use of addition. *)
57 (* ------------------------------------------------------------------------- *)
59 let FORSTER_PUZZLE = prove
60 (`(!n. f(n + 1) > f(f(n))) ==> !n. f(n) = n`,
61 REWRITE_TAC[GT; GSYM ADD1] THEN STRIP_TAC THEN
62 SUBGOAL_THEN `!m n. m <= n ==> m <= f(n)` ASSUME_TAC THENL
63 [INDUCT_TAC THEN REWRITE_TAC[LE_0] THEN
64 INDUCT_TAC THEN REWRITE_TAC[LE; NOT_SUC] THEN
65 ASM_MESON_TAC[LE_SUC_LT; LET_TRANS; LE_REFL; LT_IMP_LE; LE_TRANS];
67 SUBGOAL_THEN `!n. f(n) < f(SUC n)` ASSUME_TAC THENL
68 [ASM_MESON_TAC[NOT_LE]; ALL_TAC] THEN
69 SUBGOAL_THEN `!m n. m <= n ==> f(m) <= f(n)` ASSUME_TAC THENL
70 [GEN_TAC THEN INDUCT_TAC THEN
71 ASM_MESON_TAC[LE; LE_REFL; LT_IMP_LE; LE_TRANS]; ALL_TAC] THEN
72 ASM_REWRITE_TAC[GSYM LE_ANTISYM] THEN
73 ASM_MESON_TAC[LT_SUC_LE; NOT_LT; ADD_CLAUSES]);;
75 (* ------------------------------------------------------------------------- *)
77 (* ------------------------------------------------------------------------- *)
79 let FORSTER_PUZZLE = prove
80 (`(!n. f(n + 1) > f(f(n))) ==> !n. f(n) = n`,
81 REWRITE_TAC[GT; GSYM ADD1] THEN STRIP_TAC THEN
82 SUBGOAL_THEN `!m n. m <= f(n + m)` ASSUME_TAC THENL
83 [INDUCT_TAC THEN REWRITE_TAC[LE_0; ADD_CLAUSES; LE_SUC_LT] THEN
84 ASM_MESON_TAC[LET_TRANS; SUB_ADD]; ALL_TAC] THEN
85 SUBGOAL_THEN `!n. f(n) < f(SUC n)` ASSUME_TAC THENL
86 [ASM_MESON_TAC[LET_TRANS; LE_TRANS; ADD_CLAUSES]; ALL_TAC] THEN
87 SUBGOAL_THEN `!m n. f(m) < f(n) ==> m < n` ASSUME_TAC THENL
88 [INDUCT_TAC THEN ASM_MESON_TAC[LT_LE; LE_0; LTE_TRANS; LE_SUC_LT];
90 ASM_MESON_TAC[LE_ANTISYM; ADD_CLAUSES; LT_SUC_LE]);;