(* ========================================================================= *)
(* #73: Erdos-Szekeres theorem on ascending / descending subsequences.       *)
(* ========================================================================= *)

let lemma = prove
 (`!f s. s = UNIONS (IMAGE (\a. {x | x IN s /\ f(x) = a}) (IMAGE f s))`,
  REPEAT GEN_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN GEN_TAC THEN 
  REWRITE_TAC[IN_UNIONS; IN_ELIM_THM; IN_IMAGE] THEN
  REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
  GEN_REWRITE_TAC RAND_CONV [SWAP_EXISTS_THM] THEN
  REWRITE_TAC[UNWIND_THM2; GSYM CONJ_ASSOC; IN_ELIM_THM] THEN SET_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Pigeonhole lemma.                                                         *)
(* ------------------------------------------------------------------------- *)

let PIGEONHOLE_LEMMA = prove
 (`!f:A->B s n. 
        FINITE s /\ (n - 1) * CARD(IMAGE f s) < CARD s
        ==> ?t a. t SUBSET s /\ t HAS_SIZE n /\ (!x. x IN t ==> f(x) = a)`,
  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  MP_TAC(ISPECL [`f:A->B`; `s:A->bool`] lemma) THEN DISCH_THEN(fun th -> 
    GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV) [th]) THEN
  ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[NOT_LT] THEN
  STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN MATCH_MP_TAC
   (REWRITE_RULE[SET_RULE `{t x | x IN s} = IMAGE t s`] CARD_UNIONS_LE) THEN
  ASM_SIMP_TAC[HAS_SIZE; FINITE_IMAGE] THEN REWRITE_TAC[FORALL_IN_IMAGE] THEN
  X_GEN_TAC `x:A` THEN DISCH_TAC THEN
  MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
   [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `s:A->bool` THEN
    ASM_SIMP_TAC[SUBSET; IN_ELIM_THM];
    ALL_TAC] THEN
  DISCH_TAC THEN MATCH_MP_TAC(ARITH_RULE `~(n <= x) ==> x <= n - 1`) THEN
  DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN
  REWRITE_TAC[] THEN
  MP_TAC(ISPEC `{y | y IN s /\ (f:A->B) y = f x}` CHOOSE_SUBSET) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `n:num`) THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN SET_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Abbreviation for "monotonicity of f on s w.r.t. ordering r".              *)
(* ------------------------------------------------------------------------- *)

let mono_on = define
 `mono_on (f:num->real) r s <=> 
    !i j. i IN s /\ j IN s /\ i <= j ==> r (f i) (f j)`;;

let MONO_ON_SUBSET = prove
 (`!s t. t SUBSET s /\ mono_on f r s ==> mono_on f r t`,
  REWRITE_TAC[mono_on; SUBSET] THEN MESON_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* The main result.                                                          *)
(* ------------------------------------------------------------------------- *)

let ERDOS_SZEKERES = prove
 (`!f:num->real m n.
        (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE (m + 1) /\ mono_on f (<=) s) \/
        (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE (n + 1) /\ mono_on f (>=) s)`,
  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN
   `!i. i IN (1..m*n+1)
        ==> ?k. (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE k /\ 
                     mono_on f (<=) s /\ i IN s /\ (!j. j IN s ==> i <= j)) /\
                (!l. (?s. s SUBSET (1..m*n+1) /\ s HAS_SIZE l /\
                     mono_on f (<=) s /\ i IN s /\ (!j. j IN s ==> i <= j))
                     ==> l <= k)`
  MP_TAC THENL
   [REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM num_MAX] THEN CONJ_TAC THENL
     [MAP_EVERY EXISTS_TAC [`1`; `{i:num}`] THEN
      ASM_SIMP_TAC[SUBSET; IN_SING; LE_REFL; HAS_SIZE; FINITE_INSERT] THEN
      SIMP_TAC[FINITE_RULES; CARD_CLAUSES; NOT_IN_EMPTY; ARITH] THEN
      SIMP_TAC[mono_on; IN_SING; REAL_LE_REFL];
      EXISTS_TAC `CARD(1..m*n+1)` THEN
      ASM_MESON_TAC[CARD_SUBSET; FINITE_NUMSEG; HAS_SIZE]];
    REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
    DISCH_THEN(X_CHOOSE_THEN `t:num->num` (LABEL_TAC "*" ))] THEN
  ASM_CASES_TAC `?i. i IN (1..m*n+1) /\ m + 1 <= t(i)` THENL
   [FIRST_X_ASSUM(X_CHOOSE_THEN `i:num` STRIP_ASSUME_TAC) THEN
    FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
    DISCH_THEN(X_CHOOSE_THEN `s:num->bool` STRIP_ASSUME_TAC o CONJUNCT1) THEN
    MP_TAC(ISPEC `s:num->bool` CHOOSE_SUBSET) THEN
    ASM_MESON_TAC[HAS_SIZE; MONO_ON_SUBSET; SUBSET_TRANS];
    ALL_TAC] THEN
  SUBGOAL_THEN `!i. i IN (1..m*n+1) ==> 1 <= t i /\ t i <= m` ASSUME_TAC THENL
   [FIRST_X_ASSUM(fun th -> MP_TAC th THEN MATCH_MP_TAC MONO_FORALL) THEN
    X_GEN_TAC `i:num` THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
    ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `1` o CONJUNCT2) THEN
    STRIP_TAC THEN CONJ_TAC THENL
     [ALL_TAC; ASM_MESON_TAC[ARITH_RULE `~(m + 1 <= n) ==> n <= m`]] THEN
    FIRST_X_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `{i:num}` THEN
    ASM_SIMP_TAC[SUBSET; IN_SING; LE_REFL; HAS_SIZE; FINITE_INSERT] THEN
    SIMP_TAC[FINITE_RULES; CARD_CLAUSES; NOT_IN_EMPTY; ARITH] THEN
    SIMP_TAC[mono_on; IN_SING; REAL_LE_REFL];
    ALL_TAC] THEN
  DISJ2_TAC THEN
  SUBGOAL_THEN
   `?s k:num. s SUBSET (1..m*n+1) /\ s HAS_SIZE (n + 1) /\
              !i. i IN s ==> t(i) = k`
  MP_TAC THENL
   [MATCH_MP_TAC PIGEONHOLE_LEMMA THEN
    REWRITE_TAC[FINITE_NUMSEG; CARD_NUMSEG_1; ADD_SUB] THEN
    MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `n * CARD(1..m)` THEN 
    CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[CARD_NUMSEG_1] THEN ARITH_TAC] THEN
    REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN 
    MATCH_MP_TAC CARD_SUBSET THEN REWRITE_TAC[FINITE_NUMSEG] THEN
    ASM_REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN ASM_MESON_TAC[IN_NUMSEG];
    ALL_TAC] THEN
  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:num->bool` THEN
  DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN 
  ASM_REWRITE_TAC[mono_on] THEN MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN
  REWRITE_TAC[LE_LT; real_ge] THEN STRIP_TAC THEN 
  ASM_REWRITE_TAC[REAL_LE_REFL] THEN
  REMOVE_THEN "*" (fun th -> 
    MP_TAC(SPEC `i:num` th) THEN MP_TAC(SPEC `j:num` th)) THEN
  ANTS_TAC THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `s:num->bool` STRIP_ASSUME_TAC o CONJUNCT1) THEN
  ANTS_TAC THENL [ASM_MESON_TAC[SUBSET]; ALL_TAC] THEN
  DISCH_THEN(MP_TAC o SPEC `k + 1` o CONJUNCT2) THEN
  ASM_SIMP_TAC[ARITH_RULE `~(k + 1 <= k)`; GSYM REAL_NOT_LT] THEN
  REWRITE_TAC[CONTRAPOS_THM] THEN 
  DISCH_TAC THEN EXISTS_TAC `(i:num) INSERT s` THEN REPEAT CONJ_TAC THENL
   [ASM SET_TAC[];
    REWRITE_TAC[HAS_SIZE_CLAUSES; GSYM ADD1] THEN ASM_MESON_TAC[NOT_LT];
    ALL_TAC;
    REWRITE_TAC[IN_INSERT];
    ASM_MESON_TAC[IN_INSERT; LE_REFL; LT_IMP_LE; LE_TRANS]] THEN
  RULE_ASSUM_TAC(REWRITE_RULE[mono_on]) THEN
  REWRITE_TAC[mono_on; IN_INSERT] THEN
  ASM_MESON_TAC[REAL_LE_REFL; REAL_LE_TRANS; REAL_LT_IMP_LE; NOT_LE;
                LT_REFL; LE_TRANS]);;