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]);;