Examples/dickson.ml

   1 (* ========================================================================= *)
   2 (* Dickson's lemma.                                                          *)
   3 (* ========================================================================= *)
   4
   5 let MINIMIZING_CHOICE = prove
   6  (`!(m:A->num) s. (?x. P x) ==> ?a. P a /\ !b. P b ==> m(a) <= m(b)`,
   7   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM NOT_LT] THEN
   8   MP_TAC(ISPEC `\n. ?x. P x /\ (m:A->num) x = n` num_WOP) THEN
   9   ASM_MESON_TAC[]);;
  10
  11 (* ------------------------------------------------------------------------- *)
  12 (* The Nash-Williams minimal bad sequence argument for some predicate `bad`  *)
  13 (* that is a "safety property" in the Lamport/Alpern/Schneider sense.        *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let MINIMAL_BAD_SEQUENCE = prove
  17  (`!(bad:(num->A)->bool) (m:A->num).
  18      (!x. ~bad x ==> ?n. !y. (!k. k < n ==> y k = x k) ==> ~bad y) /\
  19      (?x. bad x)
  20       ==> ?y. bad y /\
  21               !z n. bad z /\ (!k. k < n ==> z k = y k) ==> m(y n) <= m(z n)`,
  22   REPEAT GEN_TAC THEN DISCH_TAC THEN SUBGOAL_THEN
  23    `?x. !n. (x:num->A) n =
  24              @a. (?y. bad y /\ (!k. k < n ==> y k = x k) /\ y n = a) /\
  25                  !z. bad z /\ (!k. k < n ==> z k = x k)
  26                      ==> (m:A->num)(a) <= m(z n)`
  27   STRIP_ASSUME_TAC THENL
  28    [MATCH_MP_TAC(MATCH_MP WF_REC WF_num) THEN SIMP_TAC[]; ALL_TAC] THEN
  29   SUBGOAL_THEN
  30    `!n. (?y:num->A. bad y /\ (!k. k < n ==> y k = x k) /\ y n = x n) /\
  31         !z. bad z /\ (!k. k < n ==> z k = x k) ==> m(x n):num <= m(z n)`
  32   ASSUME_TAC THENL [ALL_TAC; EXISTS_TAC `x:num->A` THEN ASM_MESON_TAC[]] THEN
  33   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
  34   FIRST_X_ASSUM(fun th -> DISCH_TAC THEN SUBST1_TAC(SPEC `n:num` th)) THEN
  35   CONV_TAC SELECT_CONV THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
  36   REWRITE_TAC[TAUT `(p /\ q /\ r) /\ s <=> r /\ p /\ q /\ s`] THEN
  37   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM1] THEN
  38   REWRITE_TAC[CONJ_ASSOC] THEN MATCH_MP_TAC MINIMIZING_CHOICE THEN
  39   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN SPEC_TAC(`n:num`,`n:num`) THEN
  40   INDUCT_TAC THEN SIMP_TAC[LT] THEN MESON_TAC[]);;
  41
  42 (* ------------------------------------------------------------------------- *)
  43 (* Dickson's Lemma itself.                                                   *)
  44 (* ------------------------------------------------------------------------- *)
  45
  46 let DICKSON = prove
  47  (`!n x:num->num->num. ?i j. i < j /\ (!k. k < n ==> x i k <= x j k)`,
  48   ABBREV_TAC
  49    `bad = \n x:num->num->num. !i j. i < j ==> ?k. k < n /\ x j k < x i k` THEN
  50   SUBGOAL_THEN `!n:num x:num->num->num. ~(bad n x)` MP_TAC THENL
  51    [ALL_TAC; EXPAND_TAC "bad" THEN MESON_TAC[NOT_LT]] THEN
  52   INDUCT_TAC THENL [EXPAND_TAC "bad" THEN MESON_TAC[LT]; ALL_TAC] THEN
  53   REWRITE_TAC[GSYM NOT_EXISTS_THM] THEN DISCH_TAC THEN
  54   SUBGOAL_THEN
  55    `?x. bad (SUC n) (x:num->num->num) /\
  56         !y j. bad (SUC n) y /\ (!i. i < j ==> y i = x i)
  57               ==> x j n <= y j n`
  58   STRIP_ASSUME_TAC THENL
  59    [MATCH_MP_TAC MINIMAL_BAD_SEQUENCE THEN ASM_REWRITE_TAC[] THEN
  60     X_GEN_TAC `x:num->num->num` THEN EXPAND_TAC "bad" THEN
  61     REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; LEFT_IMP_EXISTS_THM] THEN
  62     MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN STRIP_TAC THEN
  63     EXISTS_TAC `SUC j` THEN X_GEN_TAC `y:num->num->num` THEN
  64     GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [LT_SUC_LE] THEN
  65     REWRITE_TAC[LE_LT] THEN STRIP_TAC THEN
  66     MAP_EVERY EXISTS_TAC [`i:num`; `j:num`] THEN ASM_MESON_TAC[];
  67     SUBGOAL_THEN `~(bad (n:num) (x:num->num->num))` MP_TAC THENL
  68      [ASM_MESON_TAC[]; EXPAND_TAC "bad" THEN REWRITE_TAC[]] THEN
  69     MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN DISCH_TAC THEN
  70     MP_TAC(ASSUME `bad (SUC n) (x:num->num->num):bool`) THEN
  71     EXPAND_TAC "bad" THEN REWRITE_TAC[] THEN
  72     DISCH_THEN(MP_TAC o SPECL [`i:num`; `j:num`]) THEN
  73     ASM_REWRITE_TAC[LT] THEN MATCH_MP_TAC MONO_EXISTS THEN
  74     X_GEN_TAC `k:num` THEN STRIP_TAC THEN ASM_REWRITE_TAC[LT_REFL] THEN
  75     FIRST_X_ASSUM SUBST_ALL_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC
  76      `\k. if k < i then (x:num->num->num) k else x (j + k - i)`) THEN
  77     DISCH_THEN(MP_TAC o SPEC `i:num`) THEN
  78     ASM_REWRITE_TAC[LT_REFL; SUB_REFL; ADD_CLAUSES; NOT_IMP; NOT_LE] THEN
  79     SIMP_TAC[] THEN UNDISCH_TAC `bad (SUC n) (x:num->num->num):bool` THEN
  80     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN EXPAND_TAC "bad" THEN
  81     REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; LEFT_IMP_EXISTS_THM] THEN
  82     REPEAT GEN_TAC THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
  83     ASM_MESON_TAC[LT_TRANS; ARITH_RULE
  84       `(a:num < i /\ ~(b < i) /\ i < j ==> a < j + b - i) /\
  85        (~(a < i) /\ a < b /\ i < j ==> j + a - i < j + b - i)`]]);;