Set Implicit Arguments.

Require Import Utils.
Require Import Strings.
Require Import Sequences.
Require Import NFAs.
Require Import Buechi.
Require Import Complement.
Require Import MinimalS1S.
Require Import FullS1S.
Require Import RegularLanguages.
Require Import FiniteSemigroups.
Require Import RamseyanFactorizations.
Require Import AdditiveRamsey.

Ramseyan Pigeonhole Principle

We call Ramseyan pigeonhole principle (RP) the proposition that states that the following merging equivalence has one infinite equivalence class for every sequence over a finite semigroup. We show it equivalent to RF and use it to show that RF was necessary. RP is easier to use for this as it does not require the existence of a function but only the existence of infinitely many positions.

Section RamseyanPigeonholePrinciple.

The Merging Relation

We define the merging relation for two positions on a given sequence over a finite semigroup. Formally, we do not need to prove that it is an equivalence.

Section Merging.

Context (Gamma:FiniteSemigroup).

Variable (sigma: Seq Gamma).

Note that the merging at a position is defined slightly different as we use a substring operations for which the end is inclusively. Of course, this could be easily apated to the not including the end position. But including the end position was easier to formalize in our framework. Note that the merge relation is not affected by this, as it quantifies existentially on the position.

    Definition merge_at i j k := ((k >= i /\ k >= j ) /\ SUM (closed_substr sigma i k) = SUM (closed_substr sigma j k)).
    Definition merge i j := exists k, merge_at i j k.

    Lemma merge_extend i j k n : merge_at i j k -> k <= n -> merge_at i j n.
    Proof.
      intros [H1 H2] H3. split; auto.
      remember (n - k) as m. assert (n = m + k) by omega. subst n. clear Heqm H3. induction m; auto.
      simpl plus. rewrite !closed_substr_step_last; auto.
      now rewrite !SUM_concat, IHm.
    Qed.

We show that merging can only have finitely many equivalence classes.

    Fixpoint max_of_nat_string (v : NStr nat) := match v with
      | sing n => n
      | ncons n v => max n (max_of_nat_string v)
    end.

    Lemma max_of_nat_string_correct v: forall n , n <=delta v -> v n <= max_of_nat_string v.
    Proof.
      induction v; intros n L.
      - now simpl.
      - simpl. destruct n.
        + now apply max_le_left.
        + apply max_le_right. apply IHv. simpl in L. omega.
    Qed.

    Corollary max_of_nat_string_correct' v : forall n, n <= delta v -> S (max_of_nat_string v) >= v n.
    Proof.
      intros n L. pose proof (max_of_nat_string_correct L). omega.
    Qed.

    Lemma merging_finite_equiv_classes: (exists n, forall (L : NStr nat), delta L >= n -> exists i j, i < j <= delta L /\ merge (L i) (L j)).
    Proof.
      exists (S(Cardinality Gamma)). intros L O.
      destruct (duplicates (x:=nstr_map (fun n => SUM (closed_substr sigma n ( S( max_of_nat_string L)))) L)) as [i [j [H1 H2]]].
      - rewrite <-delta_length, nstr_map_delta. omega.
      - exists i, j. rewrite <-delta_length,nstr_map_delta in H1. split.
        + omega.
        + exists ( S( max_of_nat_string L)). split.
          * split; apply max_of_nat_string_correct'; omega.
          * rewrite 2str_nth_nstr in H2 by (rewrite nstr_map_delta; omega).
            now rewrite 2nstr_map_nth in H2 by auto.
    Qed.

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

We define RP_sigma and RPc_sigma, where RPc_sigma is trivially equivalent to RP_sigma assuming XM. We show that RPc_sigma holds constructively. To show that a proposition P implies RP we just can use P to show RPc equivalent to RP (which is just RP_sigma and RPc_sigma for all sigma).

Definition RP_sigma := exists i, forall k, exists j, k <= j /\ merge i j.
Definition RPc_sigma:= ~(forall i, exists k, forall j, j < k \/ ~ merge i j ).

RPc holds

    Lemma RPc_holds : RPc_sigma.
    Proof.
       intros D.
       enough (forall i, exists j, i < j /\ forall k, j <= k -> ~ merge i k) as H.
        + enough (forall n, exists (l: NStr nat) m,
                     delta l >= n /\
                     (forall i j, i < j <= delta l -> ~ merge (l i) (l j)) /\
                     (forall j k, j <= delta l -> m <= k -> ~ merge (l j) k ) ) as H'.
          * destruct merging_finite_equiv_classes as [m FinIn].
            destruct (H' ( S m)) as [l [m' [G [NEq _]]]].
            specialize (FinIn l). destruct FinIn as [i [j [O E]]].
             -- omega.
             -- apply (NEq i j); oauto.
          * intros n. induction n.
            -- exists (sing 0).
                destruct (H 0) as [j [H1 H2]]. exists (S j). repeat split; simpl ; auto.
            -- destruct IHn as [l [m [L [P N]]]].
               specialize (H m). destruct H as [j [H1 H2]].
               exists ( ncons m l ), (S j). repeat split.
               ++ simpl; auto.
               ++ intros i k R. destruct i, k; simpl in *; auto.
                  apply neg_merging_sym, N; omega.
               ++ intros i k L1 L2. destruct i; simpl in *; auto.
        + intros i. destruct (D i) as [j P]. exists (i +S ( S j)). split; oauto.
          intros k L. specialize (P k). destruct P as [P|P]; auto.
    Qed.

End Merging.

Definition RP := forall (Gamma: FiniteSemigroup) (gamma: Seq Gamma), RP_sigma gamma.
Definition RPc := forall (Gamma: FiniteSemigroup) (gamma: Seq Gamma), RPc_sigma gamma.

Arguments merge {Gamma} sigma i j.

Lemma merging_shift (Gamma: FiniteSemigroup) sigma i j: i <= j -> merge sigma i j <-> merge (drop sigma i) 0 (j -i).
Proof.
  intros L. split; intros [k [[H1 H2] H3]].
  - exists (k - i). repeat split; auto. rewrite !closed_substr_shift.
    rewrite !Nat.add_0_r, !le_plus_minus_r; auto.
  - exists (i + k). repeat split; auto. rewrite !closed_substr_shift in H3.
    rewrite !Nat.add_0_r, !le_plus_minus_r in H3; auto.
Qed.

Global Instance merging_proper (Gamma:FiniteSemigroup) : Proper (@seq_equiv _ Gamma ==> eq ==> eq ==> iff) (merge (Gamma:=Gamma)).
Proof.
  intros sigma tau E i i' <- j j'<-. split; intros [k [H1 H2]]; exists k; split; auto; [rewrite <-E | rewrite E]; assumption.
Qed.

RP implies IP

The following proof is similar to the proof RF -> IP and needed for showing RP <-> RF.

Lemma RP_implies_IP: RP -> IP.
Proof.
  intros INF Gamma sigma.
  specialize (INF (mkSG (@left_assoc Gamma)) sigma).
  destruct INF as [i INF].
  exists (sigma i). intros n.
  destruct (INF n) as [k [P1 [l [P2 P3]]]].
  exists k. split; auto.
  now rewrite !left_assoc_sum, !closed_substr_nth in P3 by omega.
Qed.

End RamseyanPigeonholePrinciple.

Equivalence of RP and RF

We now show that RP and RF are equivalent. To direction RF -> RP is easy as RF gives us a function and we only need infinitely many indices. The other direction RP -> RF is more complicated as we need to build the function from the indices. This relies on constructive choice.

Section RPIffRF.

  Lemma RF_implies_RP: RF -> RP.
  Proof.
    intros RF Gamma sigma.
    specialize (RF Gamma sigma).
    apply ramsey_fac_iff_homogenous in RF.
    destruct RF as [beta [Inf Hom]].
    destruct (Inf 0) as [i [H1 H2]].
    exists i. intros k.
    destruct (Inf (S i + k)) as [j [H3 H4]].
    exists j. split; auto.
    destruct (Inf (S j)) as [l [H5 H6]].
    exists (pred l). repeat split; auto.
    destruct Hom as [a H7]. unfold substr' in H7.
    rewrite !H7; auto.
  Qed.

To show RP -> RF we use recursively constructive choice to compute the indices guaranteed to exist by RP.

  Section RPImpliesRF.
    Context (Gamma: FiniteSemigroup).
    Context (sigma: Seq Gamma).
    Context (i : nat).
    Variable (H: (forall k, exists j, k <= j /\ merge sigma i j)).

    Lemma H': forall n, exists k, exists j, j <= k /\ i <= k /\ n <= j /\ SUM (closed_substr sigma i k) = SUM (closed_substr sigma j k).
    Proof.
      intros n. specialize (H n). destruct H as [j [H2 [k [H3 H4]]]].
      exists k, j. split; auto.
    Qed.

    Definition cc_j_k n : { k : nat & {j | j <= k /\ i <= k /\ n < j /\ SUM (closed_substr sigma i k) = SUM (closed_substr sigma j k)}}.
    Proof.
      destruct (cc_nat _ (H' (S n))) as [k P].
      exists k. destruct (cc_nat _ P) as [j P'].
      now exists j.
    Qed.

We now define two functions g and f. g gives the positions where all preceeding positions merge with i at and f gives positions merging with i.

    Fixpoint g n := match n with
       | 0 => S i
       | S n => projT1 (cc_j_k (g n))
    end.

    Definition f n := match n with
       | 0 => i
       | S n => proj1_sig (projT2 (cc_j_k (g n)))
     end.

    Lemma order_g_f n : g n < f (S n) <= g (S n).
    Proof.
      destruct n.
      - simpl. destruct (cc_j_k (S i)) as [j [k H2]]. cbn. omega.
      - cbn. destruct (cc_j_k (g n)) as [j [k H2]]. cbn.
        destruct (cc_j_k j) as [j' [k' H3]]. cbn. omega.
    Qed.

    Lemma f_g_merging n : SUM (closed_substr sigma i (g n)) = SUM (closed_substr sigma (f n) (g n)).
    Proof.
      destruct n.
      - reflexivity.
       - simpl. now destruct (cc_j_k (g n)) as [j [k H2]].
     Qed.

    Lemma g_smonotone : s_monotone g.
    Proof.
      intros [|n].
      - cbn; destruct cc_j_k as [j [k H1]]; cbn; auto.
      - remember (S n) as m. cbn. destruct cc_j_k as [j [k H1]]; cbn; auto.
    Qed.

    Lemma f_smonotone : s_monotone f.
    Proof.
      intros [|n].
      - cbn. destruct cc_j_k as [j [k Q]]. cbn. omega.
      - pose proof (order_g_f ( n)).
        remember (S n) as m. cbn in *. destruct cc_j_k as [j [k Q]]. cbn in *. omega.
    Qed.

    Lemma f_g_merge n : merge_at sigma i (f n) (g n).
    Proof.
      split.
      - destruct n.
        + simpl. omega.
        + pose proof (order_g_f n). split; try omega.
          enough (g 0 < g ( S n)).
          * cbn in *. omega.
          * apply s_monotone_order_preserving; auto.
            apply g_smonotone.
      - apply f_g_merging.
    Qed.

    Lemma f_merging n m : n < m -> merge_at sigma i (f n) (pred (f m)).
    Proof.
      intros L. eapply merge_extend. apply f_g_merge.
      pose proof (order_g_f n).
      enough (f (S n) <= f m) by omega.
      decide (S n = m) as [<- | D]; auto.
      enough (f (S n) < f m) by omega.
      apply s_monotone_order_preserving; auto.
      apply f_smonotone.
    Qed.

Together we have a function producing positions that all merges with i.

    Lemma rp_implies_inf_merging_pos: exists f , (forall n, n <= f n ) /\ (forall n m , f n < f m -> merge_at sigma i (f n) (pred (f m))).
    Proof.
      exists f. split.
      - intros n. apply s_monotone_bound, f_smonotone.
      - intros n m L. apply f_merging. apply s_monotone_order_preserving in L; auto using f_smonotone.
    Qed.

This lemma is not needed for showing RP -> RF but will be needed to show AX -> RP.

    Lemma inf_merging_to_function: exists f, f 0 = 0 /\ forall n, exists k, f n <= k < f (S n) /\ SUM (closed_substr sigma i (pred (f (S n)))) = SUM (closed_substr sigma k (pred (f (S n)))).
    Proof.
      exists (fun n => match n with
                       | 0 => 0
                       | S n => S(g (S n)) end).
      split; auto. intros n.
      exists (f (S n)). destruct n.
      - split.
       + pose proof (order_g_f 0). omega.
       + apply f_g_merging.
      - split.
        + pose proof ( order_g_f (S n)). omega.
        + apply f_g_merging.
    Qed.

  End RPImpliesRF.

From f we can finally build factorizations.

  Lemma RP_implies_RF: RP -> RF.
    Proof.
      intros rp Gamma sigma.
      apply ramsey_fac_iff_homogenous.
      destruct (rp Gamma sigma) as [i H].
      destruct (rp_implies_inf_merging_pos H) as [f [H1 H2]].
      destruct (RP_implies_IP rp (wrap (fun n => SUM (closed_substr sigma i (pred (f (S n))))))) as [a Q].
      unfold merge_at in H.
      exists (wrap (fun n => if (decision (exists k, k <= n /\ (f k )= n /\ SUM (closed_substr sigma i (pred (f k))) = a)) then true else false)).
      split.
      - intros n. destruct (Q n) as [m [Q1 Q2]].
        rewrite wrap_correct in Q2. specialize (H1 (S m)).
        exists ( (f (S m))). split; auto.
        rewrite wrap_correct, decision_true; auto.
        exists (S m). repeat split; auto.
      - exists a. intros n m L. rewrite !wrap_correct.
        destruct decision as [[k1 [H3 [H4 H5]]]|D]; intros E; try (now exfalso).
        destruct decision as [[k2 [H6 [H7 H8]]]|D]; intros E'; try (now exfalso).
        subst n m.
        specialize (H2 k1 k2) as [m Q1]; auto.
        unfold substr'. now rewrite <-Q1, H8.
    Qed.

End RPIffRF.