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

Equivalence of RF and Additive Ramsey Theorem (RA)

We show that RF is equivalent to Additive Ramsey Theorem. To prove the equivalence, we first need to convert between infinite boolean sequences (sequences over bool that are infinitely often true) and factorizations, which is somehow tedious.

Section FactorizationToBooleanSequence.

Conversion of Factorisations to Infinite Boolean Sequences

The positions which are true in an infinite boolean sequence encode the positions where the factors start. As the first factor always start at position 0, we just ignore the first value in the boolean sequence instead of forcing it to be true.
The following is probably far away from an elegant solution ...

  Implicit Type(beta: Seq bool).
  Definition infinite beta:= inf_often (fun b => b = true) beta.

  Context {X: Type}.
  Implicit Type (x: NStr X) (sigma: Seq X) (tau: Seq (NStr X)).

We convert a nonempty string to a boolean string of the same length that is true in the begin and false everywhere else to build the boolean sequence from a factorization.

  Definition nstr_to_bnstr x :=
    match x with
     | sing a => sing true
     | ncons a x => ncons true (nstr_map (fun _ => false) x)
    end.

  Lemma nstr_to_bnstr_true x : nstr_to_bnstr x 0 = true.
  Proof.
    now destruct x.
  Qed.

  Lemma nstr_to_bnstr_false x n : n < delta x -> nstr_to_bnstr x (S n) = false.
  Proof.
    destruct x; cbn. now intros.
    intros H. rewrite nstr_map_nth; auto.
  Qed.

  Lemma nstr_to_bnstr_delta x : delta (nstr_to_bnstr x) = delta x.
  Proof.
    destruct x; simpl; auto.
    f_equal. apply nstr_map_delta.
  Qed.

  Definition factorisation_to_bseq tau := flatten (map nstr_to_bnstr tau).

We prove correctness of the construction:
  • The resulting boolean sequence is infinite
  • If there are two positions that are true such that there is not other true in between, this corresponds to one factor in the factorization.

  Lemma factorisation_to_bseq_infinite tau : infinite (factorisation_to_bseq tau).
  Proof.
    apply inf_often_flatten. intros n.
    exists n. split; auto.
    exists 0. split; auto.
    rewrite map_nth. apply nstr_to_bnstr_true.
  Qed.

  Fixpoint begin_pos tau n :=
    match n with
    | 0 => 0
    | S n => begin_pos (tl tau) n + S( delta (tau 0))
  end.

  Lemma begin_pos_smonotone tau : s_monotone (begin_pos tau).
  Proof.
    intros n. revert tau. induction n;intros tau;[|specialize (IHn (tl tau))]; cbn in *; auto.
  Qed.

  Lemma substr_flatten tau i j: i < j -> nstr_flatten (substr' tau i j) = substr' (flatten tau) (begin_pos tau i) (begin_pos tau j).
  Proof.
    intros L.
    remember (j - i - 1) as k. assert (j = i + S k ) by omega. subst j. clear Heqk.
    revert tau k L. induction i; intros tau k L.
    - rewrite plus_O_n. clear L. revert tau. induction k; intros tau.
      + simpl. rewrite flatten_correct.
        unfold substr'. simpl.
        rewrite closed_substr_begin. rewrite (nth_first_hd tau).
        symmetry. apply closed_prefix_eq.
      + rewrite (substr'_split (flatten tau)) with (j := begin_pos tau 1).
        * simpl nstr_flatten. f_equal.
          -- cbn. rewrite flatten_correct. unfold substr'.
             rewrite Nat.sub_0_r. simpl. now rewrite closed_prefix_eq.
          -- enough (substr' (flatten tau) (begin_pos tau 1) (begin_pos tau (S (S k))) = substr' (flatten (tl tau)) 0 (begin_pos (tl tau) (S k))) as H.
             ++ rewrite H. rewrite <-IHk. cbn. now rewrite Nat.sub_0_r.
             ++ rewrite flatten_correct. remember (S k) as k'.
                simpl begin_pos. rewrite !nstr_to_str_length, plus_comm.
                rewrite <-(Nat.add_0_r (|tau 0|)) at 1.
                rewrite substr'_prepend'; auto.
                subst k'. simpl. omega.
        * split; apply s_monotone_order_preserving; auto; apply begin_pos_smonotone.
    - specialize (IHi (tl tau) k).
      rewrite flatten_correct. simpl begin_pos.
      rewrite !nstr_to_str_length.
      setoid_rewrite plus_comm at 2.
      setoid_rewrite plus_comm at 3.
      rewrite substr'_prepend'.
      + rewrite <-IHi.
        * f_equal. unfold substr'.
          rewrite closed_substr_step. f_equal; auto.
        * omega.
      + apply s_monotone_order_preserving; auto.
        apply begin_pos_smonotone.
  Qed.

  Lemma mem_factorisation_to_bseq tau n : (factorisation_to_bseq tau) n = true -> exists i, (begin_pos tau) i = n.
  Proof.
    revert tau. apply complete_induction with (n:=n).
    - clear n. intros tau H. exists 0. reflexivity.
    - clear n. intros n IH tau H.
      decide (n < delta(tau 0)) as [D|D].
      + exfalso.
        unfold factorisation_to_bseq in H.
        rewrite flatten_correct, map_correct, hd_correct in H.
        rewrite prepend_nstr_nth_first in H.
        * rewrite nstr_to_bnstr_false in H. congruence. apply D.
        * rewrite nstr_to_bnstr_delta, <-nth_first_hd. omega.
      + assert ((S n - S (delta (tau 0))) <= n) as H2. { omega. }
        destruct (IH (S n - S (delta (tau 0))) H2 (tl tau)) as [i H3].
        * unfold factorisation_to_bseq in *.
          rewrite flatten_correct, map_correct, hd_correct, tl_correct in H.
          rewrite prepend_nstr_nth_rest_sub, nstr_to_bnstr_delta in H; auto.
          rewrite nstr_to_bnstr_delta, <-nth_first_hd; auto.
        * exists (S i). simpl. rewrite H3. omega.
 Qed.

  Lemma factorisation_to_bseq_correct tau i j:i < j -> (factorisation_to_bseq tau) i = true -> (factorisation_to_bseq tau) j = true -> exists m n, (m < n/\ (i > 0 -> m > 0) ) /\ substr' (flatten tau) i j = nstr_flatten (substr' tau m n).
  Proof.
    intros L [n <-]% mem_factorisation_to_bseq [m <-]%mem_factorisation_to_bseq.
    exists n, m. repeat split.
    - apply s_monotone_order_preserving in L; auto. apply begin_pos_smonotone.
    - destruct n; cbn; omega.
    - symmetry. apply substr_flatten. apply s_monotone_order_preserving in L; auto. apply begin_pos_smonotone.
  Qed.


Given an infinite boolean sequence and some sequence over X, we convert it to a factorization.

  Definition infinite_bseq_to_factorisation sigma beta (H: infinite beta): Seq (NStr X).
  Proof.
    apply (cut sigma).
    apply (map (delta (X:= bool))).
    eapply factorize with (sigma0 := tl beta). (* tl because the first value does not matter *)
    2: apply inf_often_tl, H.
    auto.
  Defined.

  Lemma infinite_bseq_to_factorisation_correct sigma beta (Inf: infinite beta): flatten (infinite_bseq_to_factorisation sigma Inf) == sigma.
  Proof.
    unfold infinite_bseq_to_factorisation. now apply flatten_cut_inv.
  Qed.

  Lemma infinite_bseq_to_factorisation_seg sigma beta (Inf: infinite beta) n :
       beta 0 = true -> exists i j, n <=i < j /\ beta i = true /\ beta j = true /\ (infinite_bseq_to_factorisation sigma Inf) n = substr' sigma i j.
  Proof.
    intros H. unfold infinite_bseq_to_factorisation.
    revert sigma beta Inf H. induction n; intros sigma beta Inf H.
    - exists 0. exists (cc_nat_first_geq_exists (Inf 1)). repeat split; auto.
      + now pose proof (cc_nat_first_geq_exists_increasing (Inf 1)).
      + apply cc_nat_first_geq_exists_correct.
      + rewrite cut_correct, nth_first. rewrite map_correct, hd_correct, factorize_correct, hd_correct.
        unfold substr'. rewrite closed_substr_begin, closed_prefix_delta. f_equal.
        apply cc_nat_first_geq_exists_eq; auto.
        * pose proof (cc_nat_first_geq_exists_increasing (Inf 1)).
          pose proof (cc_nat_first_geq_exists_correct (Inf 1)).
          destruct (cc_nat_first_geq_exists (Inf 1)).
          -- now exfalso.
          -- cbn. now rewrite <-nth_step_tl.
        * intros k L.
          rewrite <-nth_step_tl.
          apply (cc_nat_first_geq_exists_all (L:= Inf 1)). omega.
    - pose (k := cc_nat_first_geq_exists (inf_often_tl Inf 0)).
      pose proof (cc_nat_first_geq_exists_increasing (inf_often_tl Inf 0)) as Q1.
      pose proof (cc_nat_first_geq_exists_correct (inf_often_tl Inf 0)) as Q2.
      destruct (IHn (drop sigma (S k)) (drop beta (S k)) (inf_often_drop (S k) Inf)) as [i [j [H1 [H2 [H3 H4]]]]].
      + rewrite drop_nth'. cbn. subst k.
        rewrite nth_step_tl. apply Q2.
      + exists ( S k + i), ( S k + j). repeat split; auto.
        * now rewrite drop_nth in H2.
        * now rewrite drop_nth in H3.
        * unfold substr' in *.
          rewrite_eq (pred (S k + j) = S k + pred j).
          rewrite <-closed_substr_shift, <-H4.
          rewrite cut_correct, nth_step, map_correct, factorize_correct, !hd_correct, !tl_correct, closed_prefix_delta.
          subst k. erewrite factorize_proper.
          1: reflexivity.
          now rewrite drop_tl.
  Qed.

We later want to modify the head of an infinite boolean sequence to ensure that it is either false or true. We establish basic lemmas:

  Definition update_head beta b : Seq bool := b:::tl beta.
  Hint Unfold update_head.


  Lemma infinite_update beta b : infinite beta -> infinite (update_head beta b).
  Proof.
    intros H k.
    destruct (H (S k)) as [j [H1 H2]].
    exists j. split; auto.
    destruct j; auto.
  Qed.

  Lemma update_false_mem beta n: update_head beta false n = true -> n > 0 /\ beta n = true.
  Proof.
    intros H.
    destruct n; auto.
    exfalso. now cbn in H.
  Qed.

  Lemma update_true_mem beta n: (update_head beta true) n = true -> n > 0 -> beta n = true.
  Proof.
    intros H G.
    destruct n; auto.
  Qed.

  Lemma update_head_hd_correct beta b : (update_head beta b) 0 = b.
  Proof.
    reflexivity.
  Qed.

End FactorizationToBooleanSequence.


Equivalence of RF and RA

We define RA and show it equivalent to RF.

Section AdditiveRamsey.

  Implicit Type(beta: Seq bool).
  Definition additive (Gamma: FiniteSemigroup) (gamma: nat -> nat -> Gamma) := forall i j k, i < j < k -> gamma i k = add (gamma i j) (gamma j k).
  Definition homogenous (Gamma: FiniteSemigroup) (gamma : nat -> nat -> Gamma) beta := exists c, forall i j, i < j -> beta i = true -> beta j = true -> gamma i j = c.

  Definition RA := forall (Gamma: FiniteSemigroup) gamma, additive gamma -> exists beta, infinite beta /\ homogenous gamma beta.

  Lemma flatten_idempotent (Gamma: FiniteSemigroup) (x: NStr (NStr Gamma)) c : (forall n, n <= delta x -> (SUM (x n) = c)) -> idempotent c -> SUM (nstr_flatten x ) = c.
  Proof.
    intros H I. induction x.
    - simpl. apply (H 0). omega.
    - simpl. rewrite SUM_concat.
      pose proof (H 0) as H1. simpl in H1. rewrite H1 by omega.
      rewrite IHx.
      + apply I.
      + intros n L. apply (H (S n)). cbn. omega.
  Qed.

  Lemma ramsey_fac_iff_homogenous (Gamma: FiniteSemigroup) (sigma: Seq Gamma) : admits_ramseyan_factorization sigma <-> exists beta, infinite beta /\ homogenous (fun i j => SUM (substr' sigma i j)) beta.
  Proof.
    split.
    - intros [tau [[H1 H2] H3]] % admits_ramseyan_fac_iff_idem_ramseyan_fac.
      exists (update_head (factorisation_to_bseq tau) false). split.
      + apply infinite_update, factorisation_to_bseq_infinite.
      + exists (SUM (tau 1)). intros i j L [Gi Mi]%update_false_mem [Gj Mj]%update_false_mem.

        destruct (factorisation_to_bseq_correct L Mi Mj) as [n [m [Q1 Q2]]].
        rewrite H1, Q2.
        rewrite flatten_idempotent with (c:= SUM (tau 1)); auto.
        intros k. rewrite substr'_delta; auto. intros L'. rewrite substr'_nth by auto. apply H2. omega.
    - intros [beta [Inf [c Hom]]].
      exists (infinite_bseq_to_factorisation sigma (infinite_update true Inf)). split.
      + symmetry. now apply infinite_bseq_to_factorisation_correct.
      + intros n L. destruct (infinite_bseq_to_factorisation_seg sigma (infinite_update true Inf) n) as [j [k [H1 [H2 [H3 H4]]]]].
        * apply (update_head_hd_correct beta).
        * rewrite !H4.
          destruct (infinite_bseq_to_factorisation_seg sigma (infinite_update true Inf) 1) as [j' [k' [H1' [H2' [H3' H4']]]]].
          -- apply (update_head_hd_correct beta).
          -- rewrite H4'.
             rewrite !Hom; auto; apply update_true_mem; auto.
  Qed.

  Lemma additive_to_substr' (Gamma : FiniteSemigroup) gamma:
      additive gamma -> (forall i j, i < j -> gamma i j = SUM (substr' (wrap (fun n => gamma n (S n))) i j)).
  Proof.
    intros Add i j L.
    remember (j - S i) as k. assert (j = S k + i) by omega. subst j. clear Heqk.
    induction k.
    - unfold substr'. simpl. unfold closed_substr. rewrite Nat.sub_diag. simpl.
      now rewrite <-nth_first_hd, drop_nth', wrap_correct.
    - unfold substr'. simpl. rewrite closed_substr_step_last, SUM_concat by auto. simpl.
      rewrite wrap_correct.
      rewrite Add with (j := S (k + i)) by omega.
      f_equal. apply IHk. omega.
  Qed.

  Lemma RF_implies_RA : RF -> RA.
  Proof.
    intros rf Gamma gamma Add.
    specialize (rf Gamma (wrap (fun n => gamma n (S n)))).
    apply ramsey_fac_iff_homogenous in rf.
    destruct rf as [beta [Inf [c Hom]]].
    exists beta; split; auto.
    exists c. intros i j L iM jM.
    rewrite additive_to_substr' by assumption.
    now apply Hom.
  Qed.

  Lemma RA_implies_RF : RA -> RF.
  Proof.
    intros ra Gamma sigma.
    apply ramsey_fac_iff_homogenous. apply ra.
    intros i j k L. now rewrite (substr'_split sigma L), SUM_concat.
  Qed.
End AdditiveRamsey.

The following is not related to RA, but we place it here, as it concers a third representation of factorizations: strictly monotone functions. A strictly monotone function f: nat -> nat specifies the positions of a sequence, where the factors of a factorization starts. Here we require f 0 = 0.
Section FactorizationsAsStrictlyMonotoneFunctions.

  Definition fun_encodes_factorization (f: nat -> nat):= f 0 = 0 /\ s_monotone f.

  Definition encodes_fact_tl (f : nat -> nat) : nat-> nat := (fun n => f (S n) - f 1).

  Lemma tl_preserves_encodes_fact f : fun_encodes_factorization f -> fun_encodes_factorization (encodes_fact_tl f).
  Proof.
    intros [H1 H2]. split; unfold encodes_fact_tl; auto.
    intros n. destruct n.
    - specialize (H2 1). omega.
    - pose proof (H2 (S (S n))).
      enough (f 1 < f (S (S n))) by omega.
      apply s_monotone_order_preserving; auto.
  Qed.

  Lemma encodes_fact_tl_preserves_deltas f m : fun_encodes_factorization f -> f (S (S m)) - S (f (S m)) = encodes_fact_tl f (S m) - S (encodes_fact_tl f m).
  Proof.
    intros [H1 H2].
    unfold encodes_fact_tl .
    destruct m; auto.
    pose proof (H2 (S (S m))).
    enough (f 1 < f (S (S m))) by omega.
    apply s_monotone_order_preserving; auto.
  Qed.

  Lemma encodes_fact_tl_revert f n : fun_encodes_factorization f -> f (S n) = S (f 1 - S (f 0)) + encodes_fact_tl f n.
  Proof.
    intros [H1 H2]. unfold encodes_fact_tl.
    pose proof (H2 0). destruct n; auto.
    enough (f 1 < f (S (S n))) by omega.
    apply s_monotone_order_preserving; auto.
  Qed.


  Lemma factorize_monotone (X: Type) ( sigma: Seq X) (f: nat -> nat) :fun_encodes_factorization f->
                sigma == flatten (wrap (fun n => closed_substr sigma (f n) (pred (f (S n))))).
  Proof.
    intros H.
    enough (wrap (fun n => closed_substr sigma (f n) (pred (f (S n)))) == cut sigma (wrap (fun n => f(S n) - S (f n)))) as H'.
    - rewrite H'. now rewrite flatten_cut_inv.
    - intros n. revert f H sigma. induction n; intros f H sigma.
      + rewrite cut_correct, nth_first, <-nth_first_hd, !wrap_correct. unfold closed_substr.
        destruct H as [H1 H2]. rewrite H1. cbn. f_equal. omega.
      + rewrite cut_correct, nth_step.
        assert (tl (wrap (fun n0 : nat => f (S n0) - S (f n0)) ) == (wrap ( fun n => (encodes_fact_tl f) (S n) - S ((encodes_fact_tl f) n)))) as H2.
        { intros m. rewrite <-!nth_step_tl, !wrap_correct.
           now apply encodes_fact_tl_preserves_deltas. }
        rewrite H2, <-nth_first_hd. rewrite !wrap_correct.
        rewrite <-IHn.
        * rewrite !wrap_correct, closed_substr_shift. f_equal.
          -- now apply encodes_fact_tl_revert.
          -- rewrite (encodes_fact_tl_revert (S n) H).
             enough (0 < encodes_fact_tl f (S n)) by omega.
             pose proof (tl_preserves_encodes_fact H) as H3. destruct H3 as [_ H3].
             specialize (H3 n). omega.
        * now apply tl_preserves_encodes_fact.
  Qed.

End FactorizationsAsStrictlyMonotoneFunctions.