100/subsequence.ml

   1 (* ========================================================================= *)
   2 (* #73: Erdos-Szekeres theorem on ascending / descending subsequences.       *)
   3 (* ========================================================================= *)
   4
   5 let lemma = prove
   6  (`!f s. s = UNIONS (IMAGE (\a. {x | x IN s /\ f(x) = a}) (IMAGE f s))`,
   7   REPEAT GEN_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN GEN_TAC THEN
   8   REWRITE_TAC[IN_UNIONS; IN_ELIM_THM; IN_IMAGE] THEN
   9   REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
  10   GEN_REWRITE_TAC RAND_CONV [SWAP_EXISTS_THM] THEN
  11   REWRITE_TAC[UNWIND_THM2; GSYM CONJ_ASSOC; IN_ELIM_THM] THEN SET_TAC[]);;
  12
  13 (* ------------------------------------------------------------------------- *)
  14 (* Pigeonhole lemma.                                                         *)
  15 (* ------------------------------------------------------------------------- *)
  16
  17 let PIGEONHOLE_LEMMA = prove
  18  (`!f:A->B s n.
  19         FINITE s /\ (n - 1) * CARD(IMAGE f s) < CARD s
  20         ==> ?t a. t SUBSET s /\ t HAS_SIZE n /\ (!x. x IN t ==> f(x) = a)`,
  21   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  22   MP_TAC(ISPECL [`f:A->B`; `s:A->bool`] lemma) THEN DISCH_THEN(fun th ->
  23     GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV) [th]) THEN
  24   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[NOT_LT] THEN
  25   STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN MATCH_MP_TAC
  26    (REWRITE_RULE[SET_RULE `{t x | x IN s} = IMAGE t s`] CARD_UNIONS_LE) THEN
  27   ASM_SIMP_TAC[HAS_SIZE; FINITE_IMAGE] THEN REWRITE_TAC[FORALL_IN_IMAGE] THEN
  28   X_GEN_TAC `x:A` THEN DISCH_TAC THEN
  29   MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
  30    [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `s:A->bool` THEN
  31     ASM_SIMP_TAC[SUBSET; IN_ELIM_THM];
  32     ALL_TAC] THEN
  33   DISCH_TAC THEN MATCH_MP_TAC(ARITH_RULE `~(n <= x) ==> x <= n - 1`) THEN
  34   DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN
  35   REWRITE_TAC[] THEN
  36   MP_TAC(ISPEC `{y | y IN s /\ (f:A->B) y = f x}` CHOOSE_SUBSET) THEN
  37   ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `n:num`) THEN
  38   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN SET_TAC[]);;
  39
  40 (* ------------------------------------------------------------------------- *)
  41 (* Abbreviation for "monotonicity of f on s w.r.t. ordering r".              *)
  42 (* ------------------------------------------------------------------------- *)
  43
  44 let mono_on = define
  45  `mono_on (f:num->real) r s <=>
  46     !i j. i IN s /\ j IN s /\ i <= j ==> r (f i) (f j)`;;
  47
  48 let MONO_ON_SUBSET = prove
  49  (`!s t. t SUBSET s /\ mono_on f r s ==> mono_on f r t`,
  50   REWRITE_TAC[mono_on; SUBSET] THEN MESON_TAC[]);;
  51
  52 (* ------------------------------------------------------------------------- *)
  53 (* The main result.                                                          *)
  54 (* ------------------------------------------------------------------------- *)
  55
  56 let ERDOS_SZEKERES = prove
  57  (`!f:num->real m n.
  58         (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE (m + 1) /\ mono_on f (<=) s) \/
  59         (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE (n + 1) /\ mono_on f (>=) s)`,
  60   REPEAT STRIP_TAC THEN
  61   SUBGOAL_THEN
  62    `!i. i IN (1..m*n+1)
  63         ==> ?k. (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE k /\
  64                      mono_on f (<=) s /\ i IN s /\ (!j. j IN s ==> i <= j)) /\
  65                 (!l. (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE l /\
  66                      mono_on f (<=) s /\ i IN s /\ (!j. j IN s ==> i <= j))
  67                      ==> l <= k)`
  68   MP_TAC THENL
  69    [REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM num_MAX] THEN CONJ_TAC THENL
  70      [MAP_EVERY EXISTS_TAC [`1`; `{i:num}`] THEN
  71       ASM_SIMP_TAC[SUBSET; IN_SING; LE_REFL; HAS_SIZE; FINITE_INSERT] THEN
  72       SIMP_TAC[FINITE_RULES; CARD_CLAUSES; NOT_IN_EMPTY; ARITH] THEN
  73       SIMP_TAC[mono_on; IN_SING; REAL_LE_REFL];
  74       EXISTS_TAC `CARD(1..m*n+1)` THEN
  75       ASM_MESON_TAC[CARD_SUBSET; FINITE_NUMSEG; HAS_SIZE]];
  76     REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
  77     DISCH_THEN(X_CHOOSE_THEN `t:num->num` (LABEL_TAC "*" ))] THEN
  78   ASM_CASES_TAC `?i. i IN (1..m*n+1) /\ m + 1 <= t(i)` THENL
  79    [FIRST_X_ASSUM(X_CHOOSE_THEN `i:num` STRIP_ASSUME_TAC) THEN
  80     FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
  81     DISCH_THEN(X_CHOOSE_THEN `s:num->bool` STRIP_ASSUME_TAC o CONJUNCT1) THEN
  82     MP_TAC(ISPEC `s:num->bool` CHOOSE_SUBSET) THEN
  83     ASM_MESON_TAC[HAS_SIZE; MONO_ON_SUBSET; SUBSET_TRANS];
  84     ALL_TAC] THEN
  85   SUBGOAL_THEN `!i. i IN (1..m*n+1) ==> 1 <= t i /\ t i <= m` ASSUME_TAC THENL
  86    [FIRST_X_ASSUM(fun th -> MP_TAC th THEN MATCH_MP_TAC MONO_FORALL) THEN
  87     X_GEN_TAC `i:num` THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
  88     ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `1` o CONJUNCT2) THEN
  89     STRIP_TAC THEN CONJ_TAC THENL
  90      [ALL_TAC; ASM_MESON_TAC[ARITH_RULE `~(m + 1 <= n) ==> n <= m`]] THEN
  91     FIRST_X_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `{i:num}` THEN
  92     ASM_SIMP_TAC[SUBSET; IN_SING; LE_REFL; HAS_SIZE; FINITE_INSERT] THEN
  93     SIMP_TAC[FINITE_RULES; CARD_CLAUSES; NOT_IN_EMPTY; ARITH] THEN
  94     SIMP_TAC[mono_on; IN_SING; REAL_LE_REFL];
  95     ALL_TAC] THEN
  96   DISJ2_TAC THEN
  97   SUBGOAL_THEN
  98    `?s k:num. s SUBSET (1..m*n+1) /\ s HAS_SIZE (n + 1) /\
  99               !i. i IN s ==> t(i) = k`
 100   MP_TAC THENL
 101    [MATCH_MP_TAC PIGEONHOLE_LEMMA THEN
 102     REWRITE_TAC[FINITE_NUMSEG; CARD_NUMSEG_1; ADD_SUB] THEN
 103     MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `n * CARD(1..m)` THEN
 104     CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[CARD_NUMSEG_1] THEN ARITH_TAC] THEN
 105     REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
 106     MATCH_MP_TAC CARD_SUBSET THEN REWRITE_TAC[FINITE_NUMSEG] THEN
 107     ASM_REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN ASM_MESON_TAC[IN_NUMSEG];
 108     ALL_TAC] THEN
 109   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:num->bool` THEN
 110   DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
 111   ASM_REWRITE_TAC[mono_on] THEN MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN
 112   REWRITE_TAC[LE_LT; real_ge] THEN STRIP_TAC THEN
 113   ASM_REWRITE_TAC[REAL_LE_REFL] THEN
 114   REMOVE_THEN "*" (fun th ->
 115     MP_TAC(SPEC `i:num` th) THEN MP_TAC(SPEC `j:num` th)) THEN
 116   ANTS_TAC THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
 117   DISCH_THEN(X_CHOOSE_THEN `s:num->bool` STRIP_ASSUME_TAC o CONJUNCT1) THEN
 118   ANTS_TAC THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
 119   DISCH_THEN(MP_TAC o SPEC `k + 1` o CONJUNCT2) THEN
 120   ASM_SIMP_TAC[ARITH_RULE `~(k + 1 <= k)`; GSYM REAL_NOT_LT] THEN
 121   REWRITE_TAC[CONTRAPOS_THM] THEN
 122   DISCH_TAC THEN EXISTS_TAC `(i:num) INSERT s` THEN REPEAT CONJ_TAC THENL
 123    [ASM SET_TAC[];
 124     REWRITE_TAC[HAS_SIZE_CLAUSES; GSYM ADD1] THEN ASM_MESON_TAC[NOT_LT];
 125     ALL_TAC;
 126     REWRITE_TAC[IN_INSERT];
 127     ASM_MESON_TAC[IN_INSERT; LE_REFL; LT_IMP_LE; LE_TRANS]] THEN
 128   RULE_ASSUM_TAC(REWRITE_RULE[mono_on]) THEN
 129   REWRITE_TAC[mono_on; IN_INSERT] THEN
 130   ASM_MESON_TAC[REAL_LE_REFL; REAL_LE_TRANS; REAL_LT_IMP_LE; NOT_LE;
 131                 LT_REFL; LE_TRANS]);;