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
|
prioritize_num();;
let FORSTER_PUZZLE = prove
(`(!n. f(n + 1) > f(f(n))) ==> !n. f(n) = n`,
REWRITE_TAC[GT; GSYM ADD1] THEN STRIP_TAC THEN
SUBGOAL_THEN `!n m. f(m) < n ==> m <= f m` ASSUME_TAC THENL
[INDUCT_TAC THEN REWRITE_TAC[LT] THEN
INDUCT_TAC THEN ASM_MESON_TAC[LE_0; LE_SUC_LT; LET_TRANS]; ALL_TAC] THEN
SUBGOAL_THEN `!n. n <= f n` ASSUME_TAC THENL
[ASM_MESON_TAC[LT]; ALL_TAC] THEN
SUBGOAL_THEN `!n. f(n) < f(SUC n)` ASSUME_TAC THENL
[ASM_MESON_TAC[LET_TRANS]; ALL_TAC] THEN
SUBGOAL_THEN `!m n. m < n ==> f(m) < f(n)` ASSUME_TAC THENL
[GEN_TAC THEN INDUCT_TAC THEN ASM_MESON_TAC[LT; LT_TRANS]; ALL_TAC] THEN
SUBGOAL_THEN `!m n. (f m < f n) <=> m < n` ASSUME_TAC THENL
[ASM_MESON_TAC[LT_CASES; LT_ANTISYM; LT_REFL]; ALL_TAC] THEN
ASM_MESON_TAC[LE_ANTISYM; LT_SUC_LE]);;
(* ------------------------------------------------------------------------- *)
(* Alternative; shorter but less transparent and taking longer to run. *)
(* ------------------------------------------------------------------------- *)
let FORSTER_PUZZLE = prove
(`(!n. f(n + 1) > f(f(n))) ==> !n. f(n) = n`,
REWRITE_TAC[GT; GSYM ADD1] THEN STRIP_TAC THEN
SUBGOAL_THEN `!n m. f(m) < n ==> m <= f m` ASSUME_TAC THENL
[INDUCT_TAC THEN REWRITE_TAC[LT] THEN
INDUCT_TAC THEN ASM_MESON_TAC[LE_0; LE_SUC_LT; LET_TRANS]; ALL_TAC] THEN
SUBGOAL_THEN `!n. n <= f n` ASSUME_TAC THENL
[ASM_MESON_TAC[LT]; ALL_TAC] THEN
SUBGOAL_THEN `!n. f(n) < f(SUC n)` ASSUME_TAC THENL
[ASM_MESON_TAC[LET_TRANS]; ALL_TAC] THEN
SUBGOAL_THEN `!m n. m < n ==> f(m) < f(n)` ASSUME_TAC THENL
[GEN_TAC THEN INDUCT_TAC THEN ASM_MESON_TAC[LT; LT_TRANS]; ALL_TAC] THEN
ASM_MESON_TAC[LE_ANTISYM; LT_CASES; LT_ANTISYM; LT_REFL; LT_SUC_LE]);;
(* ------------------------------------------------------------------------- *)
(* Robin Milner's proof. *)
(* ------------------------------------------------------------------------- *)
let FORSTER_PUZZLE = prove
(`(!n. f(n + 1) > f(f(n))) ==> !n. f(n) = n`,
REWRITE_TAC[GT; GSYM ADD1] THEN STRIP_TAC THEN
SUBGOAL_THEN `!m n. m <= f(n + m)` ASSUME_TAC THENL
[INDUCT_TAC THEN REWRITE_TAC[LE_0; ADD_CLAUSES; LE_SUC_LT] THEN
ASM_MESON_TAC[LET_TRANS; SUB_ADD]; ALL_TAC] THEN
SUBGOAL_THEN `!n. f(n) < f(SUC n)` ASSUME_TAC THENL
[ASM_MESON_TAC[LET_TRANS; LE_TRANS; ADD_CLAUSES]; ALL_TAC] THEN
SUBGOAL_THEN `!m n. m <= n ==> f(m) <= f(n)` ASSUME_TAC THENL
[GEN_TAC THEN INDUCT_TAC THEN
ASM_MESON_TAC[LE; LE_REFL; LT_IMP_LE; LE_TRANS]; ALL_TAC] THEN
ASM_REWRITE_TAC[GSYM LE_ANTISYM] THEN
ASM_MESON_TAC[LT_SUC_LE; NOT_LT; ADD_CLAUSES]);;
(* ------------------------------------------------------------------------- *)
(* A variant of Robin's proof avoiding explicit use of addition. *)
(* ------------------------------------------------------------------------- *)
let FORSTER_PUZZLE = prove
(`(!n. f(n + 1) > f(f(n))) ==> !n. f(n) = n`,
REWRITE_TAC[GT; GSYM ADD1] THEN STRIP_TAC THEN
SUBGOAL_THEN `!m n. m <= n ==> m <= f(n)` ASSUME_TAC THENL
[INDUCT_TAC THEN REWRITE_TAC[LE_0] THEN
INDUCT_TAC THEN REWRITE_TAC[LE; NOT_SUC] THEN
ASM_MESON_TAC[LE_SUC_LT; LET_TRANS; LE_REFL; LT_IMP_LE; LE_TRANS];
ALL_TAC] THEN
SUBGOAL_THEN `!n. f(n) < f(SUC n)` ASSUME_TAC THENL
[ASM_MESON_TAC[NOT_LE]; ALL_TAC] THEN
SUBGOAL_THEN `!m n. m <= n ==> f(m) <= f(n)` ASSUME_TAC THENL
[GEN_TAC THEN INDUCT_TAC THEN
ASM_MESON_TAC[LE; LE_REFL; LT_IMP_LE; LE_TRANS]; ALL_TAC] THEN
ASM_REWRITE_TAC[GSYM LE_ANTISYM] THEN
ASM_MESON_TAC[LT_SUC_LE; NOT_LT; ADD_CLAUSES]);;
(* ------------------------------------------------------------------------- *)
(* The shortest? *)
(* ------------------------------------------------------------------------- *)
let FORSTER_PUZZLE = prove
(`(!n. f(n + 1) > f(f(n))) ==> !n. f(n) = n`,
REWRITE_TAC[GT; GSYM ADD1] THEN STRIP_TAC THEN
SUBGOAL_THEN `!m n. m <= f(n + m)` ASSUME_TAC THENL
[INDUCT_TAC THEN REWRITE_TAC[LE_0; ADD_CLAUSES; LE_SUC_LT] THEN
ASM_MESON_TAC[LET_TRANS; SUB_ADD]; ALL_TAC] THEN
SUBGOAL_THEN `!n. f(n) < f(SUC n)` ASSUME_TAC THENL
[ASM_MESON_TAC[LET_TRANS; LE_TRANS; ADD_CLAUSES]; ALL_TAC] THEN
SUBGOAL_THEN `!m n. f(m) < f(n) ==> m < n` ASSUME_TAC THENL
[INDUCT_TAC THEN ASM_MESON_TAC[LT_LE; LE_0; LTE_TRANS; LE_SUC_LT];
ALL_TAC] THEN
ASM_MESON_TAC[LE_ANTISYM; ADD_CLAUSES; LT_SUC_LE]);;
|
