Examples/forster.ml

   1 prioritize_num();;
   2
   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]);;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* Alternative; shorter but less transparent and taking longer to run.       *)
  21 (* ------------------------------------------------------------------------- *)
  22
  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]);;
  36
  37 (* ------------------------------------------------------------------------- *)
  38 (* Robin Milner's proof.                                                     *)
  39 (* ------------------------------------------------------------------------- *)
  40
  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]);;
  54
  55 (* ------------------------------------------------------------------------- *)
  56 (* A variant of Robin's proof avoiding explicit use of addition.             *)
  57 (* ------------------------------------------------------------------------- *)
  58
  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];
  66     ALL_TAC] THEN
  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]);;
  74
  75 (* ------------------------------------------------------------------------- *)
  76 (* The shortest?                                                             *)
  77 (* ------------------------------------------------------------------------- *)
  78
  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];
  89     ALL_TAC] THEN
  90   ASM_MESON_TAC[LE_ANTISYM; ADD_CLAUSES; LT_SUC_LE]);;