Require Import Utils.
Require Import Strings.
Require Import FiniteSemigroups.
Require Import Sequences.

Ramseyan Factorizations

This file is on Ramseyan Factorization and proves the following:
  • Definition of Ramseyan factorizations
  • Sequences have Ramseyan factorizations if and only if they have Ramseyan factorization of idempotent color
  • UP sequences always have Ramseyan factorizations
  • Ramseyan factorizations for semigroup homomorphisms
  • RF: Every sequence over a finite semigroup has a Ramseyan factorization
  • RF implies the infinite pigenhole priniciple (IP)
  • IP implies Markov's principle (MP)

Section RamseyanFactorizations.

Definition of Ramseyan Factorizations

A Ramseyan factorisation is a factorization where all factors apart the first have the same color.
  Section DefinitionAndBasics.

    Context {Gamma:FiniteSemigroup}.

    Implicit Types (sigma: Seq Gamma).
    Implicit Types (tau: Seq (NStr Gamma)).

    Definition is_ramseyan_factorization sigma tau := sigma == flatten tau /\ forall n, n > 0 -> SUM(tau n) = SUM (tau 1).
    Definition admits_ramseyan_factorization sigma := exists tau, is_ramseyan_factorization sigma tau.
    Definition admits_idempotent_ramseyan_factorization sigma := exists tau, is_ramseyan_factorization sigma tau /\ idempotent (SUM (tau 1)).


    Global Instance admits_ramseyan_factorization_proper: Proper (@seq_equiv _ Gamma ==> iff) admits_ramseyan_factorization .
    Proof.
      intros sigma sigma' E. split; intros [tau [F R]]; exists tau; split; auto; [rewrite <-E |rewrite E]; apply F.
    Qed.

Ramseyan Factorizations of Idempotent Color

We show that a Ramseyan factorization can always be turned into a Ramseyan factorisation of idempotent color. As for every element of the finite semigroup a there is a number n such that a * n is idempotent, we just group every n adjacent factors of the Ramseyan factorization.

    Lemma combine_sum tau k n: n > 0 -> SUM (map nstr_flatten (cut tau (const k)) n) = SUM (cut (map SUM tau) (const k) n).
    Proof.
      intros L. revert tau. induction n;intros tau.
      - exfalso. omega.
      - rewrite map_nth. setoid_rewrite cut_correct at 1 2. rewrite !nth_step.
        setoid_rewrite const_correct at 1 2 3 4. rewrite !hd_correct, !tl_correct. destruct n.
        + setoid_rewrite cut_correct at 1 2. rewrite !nth_first. rewrite const_correct, hd_correct.
          simpl. rewrite map_correct, tl_correct.
          now rewrite SUM_flatten, drop_map, closed_prefix_map.
        + simpl. rewrite map_correct, tl_correct, drop_map. rewrite <-IHn, map_nth; auto.
    Qed.

    Lemma ramseyan_fac_combine sigma tau k n:is_ramseyan_factorization sigma tau
        -> n > 0 -> SUM ( (map nstr_flatten (cut tau (const k)))n) = mul (SUM (tau 1)) (S k).
    Proof.
      intros [_ R] L'.
      rewrite combine_sum by auto.
      revert tau R . induction n; intros tau R .
      - exfalso. omega.
      - destruct n.
        + rewrite 2cut_correct, nth_step, nth_first. rewrite const_correct, hd_correct, tl_correct, const_correct, hd_correct.
          simpl. rewrite map_correct, tl_correct.
          revert tau R . induction k; intros tau R .
          * simpl. now rewrite map_correct, hd_correct.
          * simpl. f_equal.
            -- rewrite <-nth_first_hd, drop_nth'. simpl. rewrite map_correct, tl_correct, map_nth. apply (R (S (S k))). omega.
            -- rewrite drop_tl, 2map_correct, !tl_correct. rewrite IHk.
               ++ destruct k; repeat ( (apply (R 3);omega) + f_equal).
               ++ intros L. now exfalso.
               ++ intros n L. rewrite <-!nth_step_tl. setoid_rewrite R at 1 2; auto.
        + rewrite cut_correct, nth_step, const_correct, hd_correct, tl_correct, drop_map, IHn.
          * f_equal. rewrite drop_nth'. apply R. omega.
          * omega.
          * intros m L. rewrite !drop_nth'. setoid_rewrite R at 1 2; auto.
    Qed.

    Hint Unfold is_ramseyan_factorization.

    Lemma admits_ramseyan_fac_iff_idem_ramseyan_fac sigma : admits_ramseyan_factorization sigma <-> admits_idempotent_ramseyan_factorization sigma.
    Proof.
      split.
      - intros [tau RF].
        destruct (mul_yields_idempotent (SUM ( tau 1))) as [k [G Idem]].
        exists (map nstr_flatten (cut tau (const (pred k)))). repeat split.
        + rewrite double_flatten_cut_inv. apply RF.
        + intros n L. erewrite 2ramseyan_fac_combine; auto; apply RF.
        + destruct k; auto.
          simpl. erewrite ramseyan_fac_combine; auto.
          apply RF.
      - intros [tau RF]. now exists tau.
    Qed.


UP Sequences have Ramseyan Factorizations

For sequences an general we cannot show that they always have Ramseyan factorizations, but for UP sequences this is easy.

    Lemma cons_admits_ramseyan_fac a sigma: admits_ramseyan_factorization sigma -> admits_ramseyan_factorization (a ::: sigma).
    Proof.
      intros [tau [F R]]. exists ((ncons a (hd tau)) ::: tl tau). split.
      - rewrite flatten_correct, hd_correct. simpl. rewrite flatten_prepend, tl_correct. simpl. now rewrite <-scons_correct, F.
      - intros [|n] L. now exfalso.
        rewrite !nth_step,<-!nth_step_tl. now apply R.
    Qed.

    Lemma prefix_admits_ramseyan_fac x sigma: admits_ramseyan_factorization sigma -> admits_ramseyan_factorization (x +++ sigma).
    Proof.
      revert sigma. induction x; intros sigma.
      - now simpl.
      - intros H. simpl. apply cons_admits_ramseyan_fac, IHx, H.
    Qed.

    Lemma loop_admits_ramseyan_fac v: admits_ramseyan_factorization (omega_iter v).
    Proof.
      exists (const v). split.
      - reflexivity.
      - intros n _. now rewrite !const_nth.
    Qed.

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

  End DefinitionAndBasics.


We define the propositions RF stating that every sequence in a finite semigroup has a Ramseyan factorization.
  Definition RF := forall (Gamma: FiniteSemigroup), forall (sigma: Seq Gamma), admits_ramseyan_factorization sigma.

Ramseyan Factorizations for Semigroup Homomorphisms

Given a semigroup homomorphism NStr Sigma -> Gamma into a finite semigroup, sequences over Sigma can have Ramseyan factorizations in Gamma using the homomorphism. We introduce RF', which is RF for semigroup homomorphisms and show it equivalent to RF. Using RF' instead of RF is easier for e.g. Büchi's complement construction.

  Definition RF' := forall (Gamma: FiniteSemigroup) Sigma, forall (f: NStr Sigma -> Gamma) sigma,
                    is_homomorphism f -> exists (tau: Seq (NStr Sigma)), sigma == flatten tau /\ forall n, n > 0 -> map f tau n = map f tau 1.

  Lemma homomorphism_singletons (Gamma: FiniteSemigroup) (Sigma:Type) (f: NStr Sigma -> Gamma) x :
      is_homomorphism f -> f x = SUM (nstr_map (fun y => f (sing y)) x).
  Proof.
    intros Hom. induction x.
    - reflexivity.
    - simpl. replace (ncons a x) with (nstr_concat' (sing a) x) by reflexivity.
      now rewrite Hom, IHx.
  Qed.

  Lemma RamseyFac_iff_RamseyFac': RF <-> RF'.
  Proof.
    split; intros Rf Gamma.
    - intros Y f sigma Hom.
      destruct (Rf Gamma (map (fun y => f (sing y)) sigma)) as [tau [F R]].
      exists (cut sigma (map delta tau)). split.
      + now rewrite flatten_cut_inv.
      + intros n L. rewrite !map_nth.
        setoid_rewrite homomorphism_singletons at 1 2; auto.
        setoid_rewrite <-map_nth at 1 2.
        rewrite <-!cut_map, !F, !cut_flatten_inv. now apply R.
    - intros sigma. specialize (Rf Gamma Gamma (SUM (Gamma:=Gamma)) sigma).
      destruct Rf as [tau [F R]].
      + intros x y. apply SUM_concat.
      + exists tau. split; auto. intros n L. specialize (R n L). now rewrite 2map_nth in R.
  Qed.

End RamseyanFactorizations.

RF Implies IP and MP

We show that RF implies IP and that IP implies MP.
Section RF_impl_IP_impl_MP.

Definitions of the infinite pigeonhole principle and Markov's principle:
  Definition IP := forall (Sigma: finType)(sigma: Seq Sigma), exists (x:Sigma), inf_often (fun y => y = x) sigma.

  Definition MP := forall (sigma : Seq bool), ~(forall n, sigma n = false) -> exists n, sigma n = true.

To show that RF implies IP, we use fun a b => a as semigroup operation on some finite type Sigma.

  Lemma left_assoc (Sigma:finType) : associative (fun (a b:Sigma) => a).
  Proof. now intros *. Qed.

  Lemma left_assoc_sum (Sigma: finType) (x: NStr Sigma) : SUM (Gamma:= (mkSG (@left_assoc Sigma))) x = x 0.
  Proof.
    induction x; cbn; auto.
  Qed.

  Lemma RF_implies_IP : RF -> IP .
  Proof.
    intros RF Sigma sigma.
    destruct (RF (mkSG (@left_assoc Sigma)) sigma) as [tau [H1 H2]].
    exists (tau 1 0).
    rewrite H1.
    apply inf_often_flatten.
    intros n. exists (S n). split; auto.
    exists 0. simpl; split; auto.
    specialize (H2 (S n)).
    rewrite !left_assoc_sum in H2. apply H2. omega.
  Qed.

To show that IP implies MP we use the semigroup over bool with or as operations.

  Lemma big_or_true (x: NStr bool) : SUM (Gamma:= mkSG Bool.orb_assoc) x = true -> once (fun b => b = true) x.
  Proof.
    intros H. induction x as [a|[|] x].
    - cbn in H. subst a. exists 0. split; cbn; auto.
    - exists 0. split; cbn; auto.
    - destruct (IHx H) as [n [H1 H2]]. exists (S n). split; cbn; auto.
  Qed.

  Lemma big_or_false (x: NStr bool) : SUM (Gamma:= mkSG Bool.orb_assoc) x = false -> forall n, n <= delta x -> x n = false.
  Proof.
    intros H. induction x as [a|[|] x]; intros n L.
    - now rewrite <-H.
    - cbn in H. now exfalso.
    - destruct n; [reflexivity|].
      cbn. apply IHx. apply H. cbn in L. omega.
  Qed.

  Lemma IP_implies_MP : IP -> MP.
  Proof.
    intros IPP sigma N.
    destruct (IPP finType_bool (wrap (fun n => SUM (Gamma := mkSG Bool.orb_assoc) (closed_prefix sigma n)))) as [b H]. destruct b.
    - destruct (H 0) as [m [H1 H2]]. rewrite wrap_correct in H2.
      apply big_or_true in H2. destruct H2 as [n [Q1 Q2]].
      exists n. rewrite closed_prefix_delta in Q1.
      now rewrite <-Q2, closed_prefix_nth.
    - exfalso. apply N. intros n.
      destruct (H n) as [m [H1 H2]].
      rewrite <-closed_prefix_nth with (n := m) by assumption.
      apply big_or_false.
      + now rewrite wrap_correct in H2.
      + now rewrite closed_prefix_delta.
  Qed.

End RF_impl_IP_impl_MP.