Library Combi.Erdos_Szekeres.Erdos_Szekeres: The Erdös-Szekeres theorem

The Erdös-Szekeres theorem on monotonic subsequences.

A proof of the Erdös Szekeres theorem about longest increasing and decreasing subsequences. The theorem is Erdos_Szekeres and says that any sequence s of length at least n*m+1 over a totally ordered type contains

either a nondecreasing subsequence of length n+1;
or a strictly decreasing subsequence of length m+1.

We prove it as a corollary of Greene's theorem on the Robinson-Schensted correspondance. Note that there are other proofs which require less theory.

From Corelib Require Import Setoid.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype.
From mathcomp Require Import tuple finfun finset bigop path order.

Require Import partition tableau Schensted ordtype Greene Greene_inv.

Set Implicit Arguments.

Import Order.TTheory.
Open Scope N.

Lemma Greene_rel_one (T : eqType) (s : seq T) (R : rel T) :
  exists t : seq T , subseq t s /\ sorted R t /\ size t = (Greene_rel R s) 1.

Theorem Erdos_Szekeres disp (T : inhOrderType disp) (m n : nat) (s : seq T) :
  size s > m * n ->
  (exists t , subseq t s /\ sorted <=%O t /\ size t > m ) \/
  (exists t , subseq t s /\ sorted >%O t /\ size t > n ).