(* Set Implicit Arguments. *)
Require Import BasicDefs.
Require Import FinType.
Require Import Seqs.

Open Scope string_scope.

Ramseyan Properties


Definition associative (X: finType) (add: X -> X -> X) := forall x y z, add x (add y z) = add (add x y) z.

Class FiniteSemigroup := mkSG {
   elements : finType;
   add : elements -> elements -> elements;
   Assoc: associative add
}.

Coercion elements : FiniteSemigroup >-> finType.

Finite Semigroups

Section FiniteSemiGroup.

  Context {X : FiniteSemigroup}.
  Implicit Types (x y z : X).

  Fixpoint ADD' (w: Seq X)(l : nat) : X := match l with
    | 0 => w 0
    | S n => add (w 0) (ADD' ( drop 1 w) n)
  end.

  Definition ADD (v:String X) := ADD' (seq v) (|v|).

  Lemma ADD'_extensional w w' l : (forall n, n <= l -> w n = w' n) -> ADD' w l = ADD' w' l.
  Proof.
    revert w w'. induction l; intros w w' Ew.
    - cbn. apply Ew. comega.
    - cbn. specialize (IHl (drop 1 w) (drop 1 w')). cbn in IHl. rewrite IHl.
      + f_equal. apply Ew. comega.
      + intros n L. cbn. apply Ew. cbn in L. comega.
  Qed.

  Global Instance ADD_Proper: Proper (strings_equal ==> eq) ADD.
  Proof.
    intros [w l] [w' l'] [El Ew]. unfold ADD. cbn in El. subst l'. now apply ADD'_extensional.
  Qed.

  Lemma ADD_split u v : ADD (u ++ v) = add (ADD u) (ADD v).
  Proof.
    revert v. destruct u as [w l]. revert w. induction l; intros w v.
    - now cbn.
    - unfold ADD. simpl lastindex. simpl.
      specialize (IHl (drop 1 w) v). unfold ADD in IHl. simpl in IHl. rewrite <-Assoc. rewrite <- IHl.
      f_equal.
      + now rewrite prepend_string_begin by omega.
      + apply ADD'_extensional. intros n L. decide (n <= l).
        * now rewrite !prepend_string_begin by comega.
        * now rewrite !prepend_string_rest by comega.
  Qed.

  Lemma ADD'_last w n : ADD' w (S n) = add (ADD' w n) (w (S n)).
  Proof.
    revert w. induction n; intros w; auto.
    cbn. specialize (IHn (drop 1 w)). cbn in IHn.
    rewrite IHn. now rewrite Assoc.
  Qed.

  Fixpoint mul (x:X) n {struct n} := match n with
     | 0 => x
     | 1 => x
     | S n => add x (mul x n)
  end.

  Lemma mul_step x n : n > 0 -> mul x (S n) = add x (mul x n).
  Proof.
    intros L. cbn. destruct n; auto. exfalso. omega.
  Qed.

  Lemma mul_comm x n : n > 0 -> add (mul x n) x = add x (mul x n).
  Proof.
    intros L. induction n; auto.
    destruct n; auto. remember (S n) as N.
    rewrite mul_step by omega. rewrite <-IHn at 2 by omega. now rewrite Assoc.
  Qed.

  Lemma mul_distr x n m : n > 0 -> m > 0 -> (mul x (n + m)) = add (mul x n) (mul x m).
  Proof.
    intros Ln Lm.
    induction m.
    - exfalso. omega.
    - destruct m.
      + cbn. rewrite_eq (n+1 = S n). rewrite mul_step by omega.
        now rewrite mul_comm.
      + rewrite_eq (n + S(S m) = S (n + S m)). rewrite !mul_step by omega.
        rewrite IHm by omega. rewrite !Assoc. f_equal.
        now rewrite mul_comm.
  Qed.

  Lemma mul_mult x n m : n > 0 -> m > 0 -> (mul x (n * m)) = (mul (mul x n) m).
  Proof.
    intros Ln Lm.
    induction m.
    - exfalso. omega.
    - destruct m.
      + cbn. now rewrite Nat.mul_1_r.
      + remember (S m) as M. rewrite mul_step by omega.
        rewrite <-IHm by omega.
        rewrite Nat.mul_succ_r.
        rewrite_eq (n*M + n = n + n* M). rewrite mul_distr; auto.
        apply mul_ge_0; omega.
  Qed.

Idempotent Elements


  Definition idempotent x := add x x = x.

  Lemma idempotent_mul x n : idempotent x -> mul x n = x.
  Proof.
    intros Idem. induction n; auto.
    cbn. destruct n; auto.
    now rewrite IHn.
  Qed.

  Lemma mul_yields_idempotent x : Sigma k, k > 0 /\ idempotent (mul x k).
  Proof.
    unfold idempotent.
    destruct (can_find_duplicate (S(Cardinality X)) (fun n => (mul x (Nat.pow 2 n)))) as [[i [j [L D]]]|D].
    - remember (j - i) as k. assert (j = i + k) by omega. subst j. assert (k > 0) by omega.
      decide (k = 1).
      + subst k. exists (Nat.pow 2 i). split. apply pow_ge_zero.
        rewrite Nat.pow_add_r in D. rewrite mul_mult in D; auto; apply pow_ge_zero.
      + exists ( (Nat.pow 2 i) * ((Nat.pow 2 k)-1)). rewrite Nat.pow_add_r in D.
        remember (Nat.pow 2 i) as I. remember (Nat.pow 2 k) as K.
        assert (K > 2). { subst K. destruct k.
           - exfalso. omega.
           - cbn. enough (Nat.pow 2 k >1 ) by omega.
             destruct k.
             + exfalso. omega.
             + cbn. enough(Nat.pow 2 k > 0) by omega. apply pow_ge_zero. }
        assert (I > 0). { subst I. apply pow_ge_zero. } clear HeqI HeqK.
        split. { apply mul_ge_0; omega. }
        rewrite <-mul_distr; auto.
        * rewrite <-Nat.mul_add_distr_l. rewrite_eq ((K-1) +(K-1) = K + (K -2) ).
          rewrite Nat.mul_add_distr_l. rewrite mul_distr; auto.
          -- rewrite <-D. rewrite <-mul_distr; auto.
             ++ f_equal. enough ( I = I * 1) as H'.
                ** rewrite H' at 1. rewrite <-Nat.mul_add_distr_l. f_equal. omega.
                ** symmetry. apply Nat.mul_1_r.
             ++ apply mul_ge_0; omega.
          -- apply mul_ge_0; omega.
          -- apply mul_ge_0; omega.
        * apply mul_ge_0; omega.
        * apply mul_ge_0; omega.
     - exfalso. omega.
  Qed.

  Lemma ADD_iter v k : ADD (fin_iter v k) = mul (ADD v) (S k).
  Proof.
    induction k; auto. destruct k.
    - simpl fin_iter. rewrite ADD_split; auto.
    - remember (S k) as K. assert (K > 0). { subst K. omega. }
      simpl fin_iter. rewrite mul_step; auto. rewrite <-IHk; auto.
      rewrite ADD_split; auto.
  Qed.

  Lemma ADD_single_extract w i: (ADD (extract i (S i) w)) = w i.
  Proof.
    cbn. rewrite_eq (i - i = 0). cbn. rewrite drop_correct'. now cbn.
  Qed.

  Lemma ADD_extract_last w n m : n < m -> ADD (extract n (S m) w) = add (ADD (extract n m w)) (w m).
  Proof.
    intros L. unfold ADD. cbn.
    remember (m - S n) as k. rewrite_eq (m - n = S k).
    rewrite_eq ( m = n + S k).
    rewrite <-drop_correct.
     apply ADD'_last.
  Qed.

End FiniteSemiGroup.

Equivalence of Additive Ramsey and Ramseyan Factorizations


Definition InfinitePigeonholePrinciple (X: finType) := forall (f: Seq X), exists (x:X), infinite x f.

Section AdditiveRamsey.

  Context {X:FiniteSemigroup}.
  Implicit Types (f: nat -> nat -> X).
  Implicit Types (g: nat -> X).

  Definition coloring_additive (f: nat -> nat -> X):= (forall i j k, i < j < k -> add (f i j) (f j k) = f i k).

  Definition has_monochromatic_subsequence f := exists h, s_monotone h /\ forall n m, n < m -> f(h 0) (h 1) = f (h n) (h m).


  Definition AdditiveRamsey : Prop := forall f, coloring_additive f -> has_monochromatic_subsequence f.

  Definition is_ramseyan_factorization g h:= s_monotone h /\ forall n, ADD (extract (h 0)(h 1) g) = ADD (extract (h n) (h (S n)) g).

  Definition admits_ramseyan_factorization g := exists h, is_ramseyan_factorization g h.
  Definition admits_idempotent_ramseyan_factorization g := exists h, is_ramseyan_factorization g h /\ idempotent (ADD (extract (h 0)(h 1) g)).

  Lemma sum_ramseyan_fac g h n m: n < m -> is_ramseyan_factorization g h -> mul (ADD (extract (h 0) (h 1) g)) (m - n) = ADD (extract (h n) (h m) g).
  Proof.
    intros L [Mon RF].
    remember (m - n) as k. assert (m = n + k) by omega. subst m. clear Heqk. induction k.
    - exfalso. omega.
    - decide (k > 0).
      + rewrite <-concat_extract with (i_1 := h n) (i_2 := h(n + k)).
        * rewrite ADD_split.
          rewrite_eq ( n + (S k) = S(n + k)). rewrite <-(RF (n + k)).
          rewrite_eq (S k = k +1). rewrite mul_distr by omega.
          simpl. now rewrite IHk by omega.
        * apply s_monotone_strict_order_preserving; oauto.
        * apply s_monotone_strict_order_preserving; oauto.
      + rewrite_eq (k = 0). rewrite_eq (n + 1 = S n). simpl. apply RF.
  Qed.

  Hint Unfold is_ramseyan_factorization.

  Lemma admits_ramseyan_fac_iff_idem_ramseyan_fac g : admits_ramseyan_factorization g <-> admits_idempotent_ramseyan_factorization g.
  Proof.
    split.
    - intros [h [Mon RF]].
      destruct (mul_yields_idempotent (ADD (extract (h 0)(h 1) g))) as [k [G Idem]].
      exists (fun n => h (k * n)). split.
      + split.
        * apply compose_s_monotone.
          -- intros n. rewrite Nat.mul_comm. setoid_rewrite Nat.mul_comm at 2. simpl. omega.
          -- apply Mon.
        * clear Idem. intros n. setoid_rewrite Nat.mul_comm at 1 2 3 4.
          rewrite <-sum_ramseyan_fac; oauto.
          setoid_rewrite <-sum_ramseyan_fac at 2; oauto.
          f_equal. simpl. omega.
      + rewrite <-sum_ramseyan_fac; oauto.
        setoid_rewrite Nat.mul_comm at 1 2. simpl.
        now rewrite_eq (k + 0 - 0 = k).
    - intros [h [RF _]]. now exists h.
  Qed.

  Definition RamseyFac: Prop:=forall g, admits_ramseyan_factorization g.


  Lemma compact_f f n m : coloring_additive f -> n < m -> ADD (extract n m (fun n => f n (S n))) = f n m.
  Proof.
    intros Col L; unfold ADD. induction L; unfold extract.
    - rewrite_eq (S n - S n = 0). cbn. now rewrite drop_correct'.
    - cbn. cbn in IHL. remember (m - S n) as k. rewrite_eq (m - n = S k).
      rewrite ADD'_last; auto. rewrite <-(Col n m (S m)) by omega.
      rewrite IHL, drop_correct. f_equal. f_equal; subst k; omega.
  Qed.

  Lemma RamseyFac_iff_AdditiveRamsey : RamseyFac <-> AdditiveRamsey.
  Proof.
    split.
    - intros RF f Additive.
      specialize (RF (fun n => f n (S n))).
      apply admits_ramseyan_fac_iff_idem_ramseyan_fac in RF.
      destruct RF as [h [[Mon RF] Idem]].
      exists h. split; auto.
      intros n m L. rewrite <-2compact_f; auto.
      + setoid_rewrite <-sum_ramseyan_fac at 2; auto.
        now rewrite idempotent_mul by assumption.
      + apply s_monotone_strict_order_preserving; oauto.
    - intros AR g.
      specialize (AR (fun n m => ADD (extract n m g))).
      destruct AR as [h [Mon Mono]].
      + intros i j k L. now rewrite <-ADD_split, concat_extract.
      + exists h. split; auto.
  Qed.

  Lemma loop_admits_ramseyan_fac v: admits_ramseyan_factorization (v to_omega).
  Proof.
    exists (fun n => n* S(|v|)). split.
    - intros n. simpl. setoid_rewrite Nat.mul_comm at 1 2. simpl. omega.
    - intros n. now rewrite 2extract_omega_iter.
  Qed.

  Lemma prefix_admits_ramseyan_fac v w: admits_ramseyan_factorization w -> admits_ramseyan_factorization (v +++ w).
  Proof.
    intros [h [Mon RF]].
    exists (fun n => h n + S(|v|)). split.
    - intros n. specialize (Mon n). omega.
    - intros n. rewrite 2extract_prepend. apply RF.
  Qed.

  Lemma up_admits_ramseyan_fac v w: admits_ramseyan_factorization (v +++ w to_omega).
  Proof.
    apply prefix_admits_ramseyan_fac, loop_admits_ramseyan_fac.
  Qed.

End AdditiveRamsey.

Arguments AdditiveRamsey X : clear implicits.
Arguments RamseyFac X : clear implicits.

Excluded Middle Implies Ramseyan Factorizations

Section DeriveRamseyFac.

Constructive Choice for (i,j) with i < j
  Section ConstructiveChoiceNcrossN.

     Definition Pairs := drop 1 (fun j => mkstring (fun i => (j, i)) (pred j)).

     Lemma find_pos_begin i j : i < j -> exists n, concat_inf Pairs n = (j, i).
     Proof.
       intros L. destruct j.
       - exfalso. omega.
       - exists (i + begin_in Pairs j).
         rewrite concat_inf_correct; cbn; oauto.
     Qed.

     Definition pair_to_nat : (nat * nat ) -> nat.
     Proof.
       intros [i j]. decide (i < j) as [D|D].
       - apply find_pos_begin in D. apply cc_nat in D.
         + destruct D as [n _]. exact n.
         + auto.
       - exact 0.
     Defined.

     Definition nat_to_pair : nat -> (nat*nat) := fun n => swap (concat_inf Pairs n).

     Lemma nat_to_pair_halfspace n : fst (nat_to_pair n) < snd (nat_to_pair n).
     Proof.
       unfold nat_to_pair. unfold concat_inf.
       destruct (concat_inf_indices Pairs n) as [i j] eqn:H.
       apply concat_inf_index_to_begin in H. destruct H as [H1 H2].
       cbn. rewrite H1 in H2. cbn in H2.
       remember (begin_in (fun n : nat => mkstring (fun i : nat => (S n, i)) n) i) as K.
       omega.
     Qed.

     Lemma inv_nat_to_pair i j : i < j -> nat_to_pair (pair_to_nat (i,j)) = (i,j).
     Proof.
       intros L. unfold pair_to_nat, nat_to_pair, swap.
       destruct decision as [D|D].
       - destruct cc_nat as[n P]. now rewrite P.
       - exfalso. auto.
     Qed.

     Lemma pair_nat_choice (P : nat -> nat -> Prop ) (decP: forall i j, dec (P i j)):
       (exists i j , i < j /\ P i j) -> Sigma i, {j |i < j /\ P i j}.
     Proof.
       intros E.
       enough (exists k, P (fst (nat_to_pair k)) (snd (nat_to_pair k))) as H.
       - apply cc_nat in H; auto. destruct H as [k Q].
         exists (fst (nat_to_pair k)), (snd (nat_to_pair k)). split; auto.
         apply nat_to_pair_halfspace.
       - destruct E as [i [j Q]].
        exists (pair_to_nat (i, j)). now rewrite inv_nat_to_pair by omega.
     Qed.

  End ConstructiveChoiceNcrossN.

    Context (X:FiniteSemigroup).

    Variable (f: nat -> X).

    Implicit Types (x y : X)(n m : nat).

    Notation F i j := (ADD (extract i j f)).

    Notation "i '~~@' j 'at' m" :=((m > i /\ m > j) /\ F i m = F j m) (at level 58).

    Instance dec_merge_at k1 k2 m : dec (k1 ~~@ k2 at m).
    Proof. auto. Qed.

    Definition tilde_w_equiv (k k' : nat) := exists m, k ~~@ k' at m.

    Notation "k1 '~~#' k2" := (tilde_w_equiv k1 k2) (at level 60).

    Variable (IPP_DM: forall (w: Seq X), (exists x, infinite x w) \/ (forall x, exists n, forall i, n < i -> w i <> x)).
    Variable (INF_DM: (exists i, forall j, exists k, j < k /\ i ~~# k) \/ (forall i, exists j, forall k, j >= k \/ ~ i~~# k)).


    Lemma tilde_w_extend k k' m: (k ~~@ k' at m) -> forall m', m' >= m -> k ~~@ k' at m'.
    Proof.
      intros [G W] m' L. destruct L; auto.
      repeat split; oauto.
      rewrite <-(concat_extract f (i_1 := k)(i_2 := m)(i_3:=S m0)); oauto.
      rewrite <-(concat_extract f (i_1 := k')(i_2 := m)(i_3:=S m0)); oauto.
      rewrite !ADD_split; auto.
      rewrite W. f_equal.
    Qed.

    Lemma tilde_w_index_reflexive k n : k < n -> k ~~@ k at n.
    Proof. split; oauto. Qed.

    Lemma tilde_w_index_symmetric k1 k2 m: k1 ~~@ k2 at m -> k2 ~~@ k1 at m.
    Proof. split. omega. now symmetry. Qed.

    Lemma tilde_w_index_transitive i j k m n:
        i ~~@ j at m -> j ~~@ k at n -> i ~~@ k at (max m n).
    Proof.
      intros P1 P2. split.
      - split; [apply max_le_left | apply max_le_right]; omega.
      - apply tilde_w_extend with (m':= max m n) in P1.
        apply tilde_w_extend with (m':= max m n) in P2.
        + destruct P2 as [H H']. now rewrite <-H'.
        + now apply max_le_right.
        + now apply max_le_left.
    Qed.

    Instance tilde_w_equivalence: Equivalence tilde_w_equiv.
    Proof.
      repeat split.
      - intros n. exists (S n). apply tilde_w_index_reflexive. omega.
      - intros i j [m E]. exists m. now apply tilde_w_index_symmetric.
      - intros i j k [m Em] [n En]. exists (max m n). now apply tilde_w_index_transitive with (j:=j).
    Qed.


  Definition finiteIndex (X:Type) (R: X -> X -> Prop) := (exists n, forall (L : String X), |L| > n -> exists i j, i < j < |L| /\ R (L[i]) (L[j])).

Fixpoint max_of_nat_string w l:= match l with
  | 0 => w 0
  | S l => max (w (S l)) (max_of_nat_string w l) end.

Lemma max_of_nat_string_correct v l: forall n , n<=l -> (v n) <= max_of_nat_string v l.
Proof.
  induction l; intros n L.
  - now rewrite_eq (n = 0).
  - simpl. decide (n = S l) as[D|D].
    + apply max_le_left. rewrite D. omega.
    + apply max_le_right. apply IHl. omega.
Qed.


  Lemma tilde_w_equiv_finite_index: finiteIndex tilde_w_equiv.
    Proof.
      exists (S(Cardinality X)). intros L O.
      destruct (can_find_duplicate (S(Cardinality X)) (fun n => F (L[n]) (S(max_of_nat_string (seq L) (|L|) )))) as [[i [j [G E]]]|N].
      - exists i , j. split.
        + omega.
        + exists (S (max_of_nat_string (seq L) (| L |))). repeat split.
          * enough (L [i] <= max_of_nat_string (seq L) (| L |)) by omega. apply max_of_nat_string_correct. omega.
          * enough (L [j] <= max_of_nat_string (seq L) (| L |)) by omega. apply max_of_nat_string_correct. omega.
          * assumption.
      - exfalso. omega.
    Qed.

    Lemma not_tilde_w_equiv_sym i j :~ i ~~# j -> ~ j ~~# i.
    Proof.
      intros N [n [[O1 O2] E]]. apply N. exists n. repeat split; auto.
    Qed.

    Lemma infinite_equiv_indices' :exists i, forall j, exists k, j < k /\ i ~~# k.
    Proof.
      destruct INF_DM as [D|D].
      - exact D.
      - exfalso.
        enough (forall i, exists j, i < j /\ forall k, j < k -> ~ i~~# k) as H.
        + enough (forall n, exists (l: String nat) m,
                     | l| >= n /\
                     (forall i j, i < j < |l| -> ~ l[i] ~~# l[j]) /\
                     (forall j k, j < |l| -> m <= k -> ~ k ~~# l[j]) ) as H'.
          * destruct tilde_w_equiv_finite_index as [m FinIn].
            destruct (H' (S m)) as [l [m' [G [NEq _]]]].
            specialize (FinIn l G). destruct FinIn as [i [j [O E]]].
            apply (NEq i j); oauto.
          * intros n. induction n.
            -- exists (mkstring (fun n => 0) 0), 0. simpl; repeat split; auto; intros * I; exfalso; omega.
            -- destruct IHn as [l [m [L [P N]]]].
               specialize (H m). destruct H as [j [H1 H2]].
               exists ( mkstring (prepend m l) (S(|l|))), (S j). repeat split.
               ++ cbn. omega.
               ++ simpl. intros i k R. destruct i.
                  ** simpl. destruct k. {exfalso. omega. } simpl. apply N; omega.
                  ** destruct k. {exfalso. omega. } simpl. apply P. omega.
               ++ simpl. intros i k L1 L2. destruct i.
                  ** simpl. apply not_tilde_w_equiv_sym. apply H2. omega.
                  ** simpl. apply N; omega.
        + intros i. destruct (D i) as [j P]. exists (i + S j). split; oauto.
          intros k L. specialize (P k). destruct P as [P|P]; auto. exfalso. omega.
    Qed.

    Lemma tilde_w_equiv_cc_nat i n : (exists j, n < j /\ i ~~# j) -> Sigma j, {k | n < j < k /\ i ~~@ j at k}.
    Proof.
      intros E.
      enough (exists j k, j < k /\ i < k /\ n < j /\ F i k = F j k) as H.
      - apply pair_nat_choice in H; auto.
        destruct H as [j [k [O1 [O2 [O3 P]]]]].
        exists j. exists k. split; auto.
      - destruct E as [j [O1 [k [[O2 O3] P]]]].
        exists j,k. repeat split; oauto.
    Qed.

    Fixpoint equiv_merge_subseq i (P : forall j, exists k, j < k /\ i ~~# k) (n:nat) {struct n} : nat * nat :=
       match n with
        | 0 => (i, S i)
        | S n => match (equiv_merge_subseq P n) with (j, k) =>
                  match (tilde_w_equiv_cc_nat (P k)) with (existT _ j' (exist _ k' _)) => (j', k') end
                 end
       end.

    Lemma equiv_merge_subseq_s_monotone i (P : forall j, exists k, j < k /\ i ~~# k) : s_monotone (seq_map fst (equiv_merge_subseq P)).
    Proof.
      unfold seq_map. intros n. destruct n; cbn.
      - destruct tilde_w_equiv_cc_nat as [j [k Q]]. simpl. omega.
      - destruct (equiv_merge_subseq P n) as [j k].
        destruct tilde_w_equiv_cc_nat as [j' [k' Q]].
        destruct tilde_w_equiv_cc_nat as [j'' [k'' Q']]. simpl. omega.
    Qed.

    Lemma equiv_merge_subseq_merge_at_next i (P : forall j, exists k, j < k /\ i ~~# k):
       forall n, (seq_map fst (equiv_merge_subseq P)) 0 ~~@ (seq_map fst (equiv_merge_subseq P)) n at ((seq_map fst (equiv_merge_subseq P)) (S n)).
    Proof.
      intros n. unfold seq_map. destruct n.
      - simpl. destruct tilde_w_equiv_cc_nat as [j [k Q]]. apply tilde_w_index_reflexive. comega.
      - simpl. destruct equiv_merge_subseq as [j k].
        destruct tilde_w_equiv_cc_nat as [j' [k' [O Q]]]. simpl.
        destruct tilde_w_equiv_cc_nat as [j'' [k'' [O' Q']]]. simpl.
        apply (tilde_w_extend Q). omega.
    Qed.

    Lemma infinite_merge_at_next : exists g, s_monotone g /\ forall n, forall m, m > n -> g 0 ~~@ g n at g m.
    Proof.
      destruct infinite_equiv_indices' as [i P].
      exists (seq_map fst (equiv_merge_subseq P)). split.
      - apply equiv_merge_subseq_s_monotone.
      - intros n m L. apply tilde_w_extend with (m:= (seq_map fst (equiv_merge_subseq P)) (S n)).
        + apply equiv_merge_subseq_merge_at_next.
        + apply s_monotone_order_preserving.
          * apply equiv_merge_subseq_s_monotone.
          * omega.
    Qed.


  Lemma ipp : InfinitePigeonholePrinciple X.
  Proof.
    intros w.
    destruct (IPP_DM w) as [D|D].
    - assumption.
    - exfalso.
      enough (exists n, forall m, m > n -> forall x, x el (elem X) -> w m <> x) as H'''.
      + destruct H''' as [n H'''].
        specialize (H''' (S n)). assert (S n > n) as G by omega.
        now apply (H''' G (w (S n))).
      + induction (elem X).
        * exists 0. intros m G x L. now exfalso.
        * destruct IHl as [n IHl]; auto.
          specialize (D a). destruct D as [m H].
          exists (max n m). intros k G x [P | P].
          -- subst x. apply H. pose (Nat.le_max_r n m). omega.
          -- apply IHl; auto. pose (Nat.le_max_l n m). omega.
  Qed.

    Lemma infinite_merge_at_next_same_color: exists g, s_monotone g /\ (forall n, g 0 ~~@ g n at g (S n)) /\ (forall n, F(g 0) (g 1) = F (g 0) (g (S n))).
    Proof.
      destruct infinite_merge_at_next as [g [Mon Merge]].
      destruct (ipp (fun n => F (g 0) (g ( n)))) as [x Inf].
      exists (fun n => g (fix_first_zero (infinite_filter Inf) n)). split.
      - apply compose_s_monotone.
        + apply fix_first_zero_s_monotone. apply infinite_filter_s_monotone.
        + apply Mon.
      - split.
        + intros n. simpl fix_first_zero. apply Merge. destruct n.
          * simpl. pose proof (next_position_exists_increasing (Inf (S (next_position_exists (Inf 0))))). omega.
          * simpl. pose proof (next_position_exists_increasing (Inf (S (next_position_exists (Inf (S (infinite_filter Inf n))))))). omega.
        + intros n. unfold fix_first_zero.
          now rewrite 2(infinite_filter_correct Inf).
    Qed.

    Lemma ramseyan_factorization : admits_ramseyan_factorization f.
    Proof.
      destruct infinite_merge_at_next_same_color as [g [Mon [Merge Same]]].
      exists g. split.
      - apply Mon.
      - intros n. destruct (Merge n) as [M1 M2]. rewrite <-M2.
        apply Same.
    Qed.

End DeriveRamseyFac.

Corollary XM_implies_RamseyFac: (forall p, p \/ ~ p) -> (forall X, RamseyFac X).
Proof.
  Require Import Classical.
  intros XM X f.
  apply ramseyan_factorization.
  - intros w. destruct (XM (exists x, infinite x w)) as [D|D].
    + now left.
    + right. unfold infinite in D.
      intros x. apply not_all_not_ex. intros D'.
      apply D. exists x. intros n.
      apply not_all_not_ex. intros D''.
      specialize (D' n). apply D'. intros i L.
      specialize (D'' i). apply not_and_or in D''.
      destruct D'' as [H|H].
      * exfalso. omega.
      * assumption.
  - destruct (XM (exists i : nat, forall j : nat, exists k : nat, j < k /\ tilde_w_equiv f i k)) as [D|D].
    + now left.
    + right. intros i.
      apply not_all_not_ex. intros D'.
      apply D. apply not_all_not_ex. intros D''.

      specialize (D'' i). apply not_all_ex_not in D''.
      destruct D'' as[j D''].
      apply D''. apply not_all_not_ex. intros D'''.
      specialize (D' j). apply D'.
      intros k. specialize (D''' k). apply not_and_or in D'''.
      destruct D''' as [H|H].
      * left. omega.
      * right. assumption.
Qed.

Ramseyan Factorizations Imply Markov's Principle

Section RamseyanFactorizationMarkov.

  Definition Markov := forall (f:nat -> bool), ~(forall n, f n = true) -> exists n, f n = false.

  Definition sgBoolAnd := mkSG Bool.andb_assoc.

  Lemma big_and_true f i j: true = ADD (X:=sgBoolAnd) (extract i j f) ->i < j -> forall n, i <=n < j -> f n = true.
  Proof.
    intros T O n [L G].
    remember (j - i) as k. assert (j = i + k) by omega. subst j.
    clear Heqk.
    induction k.
    - exfalso. omega.
    - decide (k = 0).
      + subst k. rewrite_eq (i + 1 = S i) in T. rewrite ADD_single_extract in T.
         assert (n = i) by omega. now subst n.
      + rewrite_eq (i + S k = S (i + k)) in T. rewrite ADD_extract_last in T by omega.
        decide (n < i + k).
        * apply IHk; oauto.
          destruct (ADD (extract i (i + k) f)); auto.
        * assert (n = i +k ) by omega. subst n.
          destruct (f(i + k)); auto.
          destruct ((ADD (extract i (i + k) f))); cbn in T; auto.
  Qed.

  Lemma big_and_false f i j: false = ADD (X:=sgBoolAnd) (extract i j f) -> i < j -> exists n, i <=n < j /\ f n = false.
  Proof.
    intros F O .
    remember (j - i) as k. assert (j = i + k) by omega. subst j.
    clear Heqk.
    induction k.
    - exfalso. omega.
    - decide ( k = 0).
      + subst k. exists i. split; oauto.
        rewrite_eq (i + 1 = S i) in F.
        now rewrite ADD_single_extract in F.
      + rewrite_eq (i + S k =S (i + k)) in F.
        rewrite ADD_extract_last in F by omega.
        destruct (ADD (extract i (i + k) f)).
        * exists (i + k). split; oauto.
        * destruct IHk as [j [L F']]; oauto.
          exists j. split; oauto.
  Qed.

  Lemma slot_in_smonotone g k : s_monotone g -> g 0 <= k -> exists n, g n <= k < g (S n).
  Proof.
    intros Mon G.
    destruct (s_monotone_unbouded_ge Mon k) as [m P].
    assert (k < g m) as H by omega.
    assert (0 <= m) as H2 by omega.
    exists (pred (next_position H2 H)).
    pose proof (next_position_correct H2 H).
    pose proof (next_position_all (L:=H2) (F:=H)).
    destruct ((next_position H2 H)).
    - simpl. exfalso. omega.
    - simpl. split; oauto.
      specialize (H1 n). omega.
  Qed.

  Lemma RamseyFacImpliesMarkov : RamseyFac sgBoolAnd -> Markov.
  Proof.
    intros RF f.
    destruct (RF f) as [g [Mon Hom]].
    destruct (ADD (extract (X:=sgBoolAnd) (g 0) (g 1) f)) eqn:E.
    - decide (exists n, n < g 0 /\ f n = false) as [D|D].
      + intros _. firstorder.
      + intros N. exfalso. apply N.
        intros n. decide (n < g 0).
        * decide (f n = true) as [D'|D']; auto.
          exfalso. apply D. exists n. split; auto.
          destruct (f n); congruence.
        * assert (exists k, g k <= n < g (S k)) as H2. {apply slot_in_smonotone; oauto. }
          destruct H2 as [k H2].
          specialize (Hom k).
          apply (big_and_true Hom); omega.
    - intros _. specialize (Hom 0).
      destruct (big_and_false Hom) as [n [O F]]; oauto.
     now exists n.
  Qed.
End RamseyanFactorizationMarkov.