Set Implicit Arguments.

Require Import Coq.Init.Nat.
Require Import Coq.Arith.Even.
Require Import Coq.Arith.Div2.

Require Import BasicDefs.
Require Import Seqs.
Require Import FinType.
Require Import Ramsey.
Require Import NFAs.
Require Import Buechi.
Require Import Complement.
Require Import ASStructures.
Require Import AbstractMSO.
Require Import MSO.
Require Import RegularLanguages.

Open Scope string_scope.

Necessity of Additive Ramsey

We show that Additive Ramsey is necessary to derive classical behavior of MSO and closure under complement together with XM for the word problem.

Closure under Complement Implies Ramseyan Factorizations

We define an NFA which accepts sequences admitting an Ramseyan factorization and prove it to accept all sequences.

 Definition ComplClosed (X:finType) := forall aut: NFA X, exists aut', L_B aut' =$= (L_B aut)^$~.
 Definition XM_WordProblem (X:finType) := forall (aut: NFA X) w, L_B aut w \/ ~ (L_B aut w).

Section ClosureUnderComplementImpliesAdditiveRamsey.
 Context (X: FiniteSemigroup).
 Variable (complement : ComplClosed X ).
 Variable (xm_word_problem: XM_WordProblem X).

 Section RamseyNFA.

   Section RamseyNFAIdem.
     Variable (x: X).

     Notation ramsey_state := (X (+) finType_bool).
     Definition ramsey_transition (q:ramsey_state) (z:X) (s: ramsey_state) := match q,s with
       |inl y, inl y' => add y z = y'
       |inl y, inr true => add y z = x
       |inr false, inl y => z = y
       |inr false, inr true => z = x
       | _, _ => False
     end.
     Instance dec_ramset_transition q z s: dec (ramsey_transition q z s).
     Proof. destruct q as [q | [|]]; destruct s as [s|[|]]; cbn; auto. Qed.

     Definition ramsey_idem_aut' := mknfa ramsey_transition (fun q => q = inr false) (fun q => q = inr true).


     Fixpoint ramsey_idem_aut'_run v n := match n with
        | 0 => inr false
        | S n => if (decision (S n > |v|)) then inr true else
                 match (ramsey_idem_aut'_run v n) with
                 | inl y => inl (add y (v [n]))
                 | inr _ => inl (v[0])
                 end
     end.

     Lemma ramsey_idem_aut'_run_is_inl v: forall n , 0 <= n < |v| -> ramsey_idem_aut'_run v (S n) = inl (ADD (mkstring v n)).
     Proof.
       intros n L. induction n.
       - cbn. now trivial_decision.
       - remember (S n) as N. cbn. rewrite IHn by omega. destruct decision.
         + exfalso. omega.
         + f_equal. unfold ADD. subst N. rewrite ADD'_last; auto.
     Qed.

     Lemma ramsey_idem_aut'_scorrect : L_S ramsey_idem_aut' =$= (fun v => ADD v = x).
     Proof.
       intros v. split.
       - intros [r [V [I F]]].
         enough (forall n, n < |v| -> r (S n) = inl (ADD (mkstring v n))) as H.
         + destruct v as [w l]. destruct l.
           * cbn. specialize (V 0). cbn in V. rewrite I in V. rewrite F in V. cbn in V. apply V. omega.
           * unfold ADD. simpl lastindex in *. rewrite ADD'_last; auto.
             specialize (V (S l)). cbn in V. rewrite F in V.
             specialize (H l). rewrite H in V by omega. apply V. omega.
         + intros n L. induction n.
           * pose proof (V 0) as V'. cbn in V'. rewrite I in V'. cbn in V'. destruct (r 1) as [z | [|]] eqn:H.
             -- f_equal. now rewrite <-V' by omega.
             -- exfalso. specialize (V 1). rewrite H in V. cbn in V. apply V. omega.
             -- exfalso. apply V'. omega.
           * pose proof (V (S n)) as V'. cbn in V'. rewrite IHn in V' by omega. cbn in V'. destruct (r (S (S n))) as [z | [|]] eqn:H.
             -- f_equal. unfold ADD. simpl lastindex. rewrite ADD'_last by auto. now rewrite <-V' by omega.
             -- exfalso. specialize (V (S (S n))). rewrite H in V. cbn in V. apply V. omega.
             -- exfalso. apply V'. omega.
      - intros A. exists (ramsey_idem_aut'_run v). repeat split; auto.
        + intros n L. destruct n.
          * cbn. destruct decision; auto.
            destruct v. cbn in *. assert (lastindex = 0) by omega. subst lastindex. now cbn in A.
          * pose proof (ramsey_idem_aut'_run_is_inl (v:=v) (n:=n)) as P.
            remember (S n) as N. cbn. rewrite P by omega. destruct decision.
            -- cbn. subst N. rewrite <-ADD'_last; auto. unfold ADD in A. now rewrite_eq (|v| = S n) in A.
            -- cbn. reflexivity.
        + cbn. now trivial_decision.
     Qed.

     Definition ramsey_idem_aut := prepend_nfa univ_aut (nfa_omega_iter ramsey_idem_aut').

     Lemma ramsey_idem_aut_correct : L_B ramsey_idem_aut =$= (fun w => exists h, ADD(extract (h 0)(h 1) w) =x /\ is_ramseyan_factorization w h).
     Proof.
       unfold ramsey_idem_aut. split.
       - intros [v [w' [Ew [_ [W [A WE]] % nfa_omega_iter_correct]]]] % prepend_nfa_correct.
         exists (fun n => begin_in W n + S(|v|)). repeat split.
         + simpl. rewrite Ew. assert (S(|v|) = 0 + S(|v|)) as H by omega.
           setoid_rewrite H at 1. rewrite_eq (S((|W 0|) + 0 + S(|v|)) = S(|W 0|) + S(|v|)). rewrite extract_prepend.
           assert (0 = begin_in W 0) as H' by reflexivity.
           assert (S (|W 0|) = begin_in W 1) as H'' by comega.
           rewrite H''. setoid_rewrite H' at 1.
           rewrite WE.
           rewrite extract_concat_inf.
           apply ramsey_idem_aut'_scorrect, A.
         + intros n. pose proof (s_monotone_begin_in W n). omega.
         + intros n.
           rewrite Ew, WE, 2extract_prepend, 2extract_concat_inf.
           pose proof (A n) as An. apply ramsey_idem_aut'_scorrect in An.
           pose proof (A 0) as A0. apply ramsey_idem_aut'_scorrect in A0.
           now rewrite An, A0.
       - intros [h [Col [Mon RF]]].
         apply prepend_nfa_correct. apply split_position_lang_prepend. exists (pred (h 1)). split.
         + now apply univ_aut_scorrect.
         + apply nfa_omega_iter_correct. apply lang_o_iter_extract.
           exists (fun n => h (S n) - h 1). repeat split; oauto.
           * intros n. pose proof (Mon (S n)). enough (h 1 <= h (S n)) by omega.
             apply s_monotone_order_preserving; oauto.
           * intros n. apply ramsey_idem_aut'_scorrect.
             enough ((extract (h (S n) - h 1) (h (S (S n)) - h 1) (drop (S (pred (h 1))) w)) == (extract (h (S n)) (h (S (S n))) w)) as H.
             -- now rewrite H, <-Col, <- RF.
             -- pose proof (Mon (S n)). assert (h 1 <= h (S n)). { apply s_monotone_order_preserving; oauto. }
                split; try comega.
                intros m L. cbn. rewrite !drop_correct. f_equal. specialize (Mon 0). omega.
     Qed.
  End RamseyNFAIdem.
  Definition ramsey_nfa := big_union (map ramsey_idem_aut (elem X) ).

  Lemma ramsey_nfa_correct: L_B ramsey_nfa =$= admits_ramseyan_factorization.
  Proof.
    intros w. unfold ramsey_nfa. split.
    - intros [nfa [[x [E _]]%in_map_iff L]] % big_union_correct.
      subst nfa. apply ramsey_idem_aut_correct in L .
      destruct L as [h [_ RF]]. now exists h.
    - intros [h RF]. apply big_union_correct. exists (ramsey_idem_aut (ADD (extract (h 0)(h 1) w))). split.
      + apply in_map_iff. exists (ADD (extract (h 0)(h 1) w)). split; auto.
      + apply ramsey_idem_aut_correct. exists h. split; auto.
  Qed.
 End RamseyNFA.

 Lemma RamseyFacFromComplement : RamseyFac X.
 Proof.
   intros w. destruct (xm_word_problem ramsey_nfa w) as [D|D].
   - apply ramsey_nfa_correct; auto.
   - exfalso.
     destruct (complement ramsey_nfa) as [autC Compl].
     assert (L_B autC w). {
       apply Compl. intros L. apply D, L. }
     destruct (dec_language_empty_informative_periodic autC) as [[u [v L]]|D'].
     + pose proof (up_admits_ramseyan_fac u v) as H'.
       apply ramsey_nfa_correct in H'.
       apply Compl in H'; auto.
     + now apply D' in H.
  Qed.

End ClosureUnderComplementImpliesAdditiveRamsey.

Classical Behavior of S1S Implies Ramseyan Factorizations

We show this using proofs by contradiction of S1S encodings.
Section MSOClassicalImpliesRamseyFac.

  Instance OmegaNatSet: NatSetClass.
  Proof.
     apply NatSetFromSeq.
     apply OmegaSequenceStructure.
  Defined.

  Implicit Types (J: SInter ).

  Definition MSO_Classical := forall I J phi, I # J |== phi \/ ~ (I # J |== phi).

  Variable (MSO_XM : MSO_Classical).
  Instance logic_dec_satis I J phi: logic_dec (I # J |== phi).
  Proof. apply MSO_XM. Qed.

  Ltac mso_contra D := mso_contra_xm MSO_XM D.

  Definition seq_to_sets (X:finType) f: X -> NatSet:= ((fun (x:X) => (seq_map (fun y => if (decision (y = x)) then true else false) f):NatSet)).


  Fixpoint vars_for_list (X : finType) (L: list X)(begin : SVar) : (X -> SVar) := match L with
      | [] => (fun x => begin)
      | x'::L => (fun x => if (decision(x = x')) then begin else (vars_for_list L (S begin)) x)
  end.
  Definition vars_for_elems (X:finType) (begin:SVar) : (X -> SVar) := vars_for_list (elem X) begin.
  Arguments vars_for_elems X begin n : clear implicits.

  Lemma vars_for_list_ge (X:finType)(L:list X) (b b': SVar) (x: X): b< b' -> b < vars_for_list L b' x.
  Proof.
    revert b'. induction L; intros b'.
    - simpl. omega.
    - intros O. simpl. destruct decision.
      + omega.
      + apply IHL. omega.
  Qed.

  Lemma vars_for_list_bound (X:finType)(L:list X) (b:SVar) (x:X): b <= vars_for_list L b x <= b + length L.
  Proof.
    revert b. induction L; intros b.
    - simpl. omega.
    - simpl. decide (x = a).
      + omega.
      + specialize (IHL (S b)). omega.
  Qed.

  Lemma vars_for_list_injective (X:finType) (L:list X) (begin:SVar): dupfree L -> forall x y, x el L -> y el L -> vars_for_list L begin x = vars_for_list L begin y -> x = y.
  Proof.
    intros D x y Ex Ey. revert begin.
    induction D as [|z]; intros begin E.
    - now exfalso.
    - destruct Ex as [Hx|Hx]; destruct Ey as [Hy|Hy]; simpl in E;trivial_decision.
      + now subst z.
      + exfalso. decide (y = z).
        * now subst y.
        * assert( begin < S begin) as H' by omega. pose (vars_for_list_ge A y H'). omega.
      + exfalso. decide (x = z); trivial_decision.
        * now subst x.
        * assert (begin < S begin) as H' by omega. pose (vars_for_list_ge A x H'). omega.
      + apply IHD with (begin:=S begin); auto. decide (x = z); decide(y = z).
        * exfalso. now subst z.
        * exfalso. assert( begin < S begin) as H' by omega. pose (vars_for_list_ge A y H'). omega.
        * exfalso. assert (begin < S begin) as H' by omega. pose (vars_for_list_ge A x H'). omega.
        * assumption.
  Qed.

  Lemma vars_for_elems_injective (X:finType) (begin:SVar) : injective (vars_for_elems X begin).
  Proof.
    unfold vars_for_elems. intros x y E. apply vars_for_list_injective in E; auto using dupfree_elements.
  Qed.

  Lemma vars_for_elems_bound (X: finType) (b:SVar) (x:X) : b <= vars_for_elems X b x <= b + Cardinality X.
  Proof.
    unfold vars_for_elems. apply vars_for_list_bound.
  Qed.

  Lemma ipp_dm (X: finType): forall (w: Seq X), (exists x, infinite x w) \/ (forall x, exists n, forall i, n < i -> w i <> x).
  Proof.
    intros f.

    destruct (MSO_XM (fun n => 0) (finBigUpdate2 (vars_for_elems X 2) (seq_to_sets f) (fun n => singletonSet 0)) (OR { x | (fun x => True) x} all1 0, ex1 1, 0 <2 1 /\2 1 el2 (vars_for_elems X 2 x))).
    - left. apply finBigOrCorrect in H. destruct H as [x [Sat _]].
      exists x. intros n. rewrite all1_correct in Sat. specialize (Sat n).
      destruct Sat as [m [G Sat]]. exists m. cbn in *. trivial_decision. split; oauto.
      rewrite finBigUpdate2_changed in Sat by apply vars_for_elems_injective.
      unfold seq_to_sets, seq_map in Sat. cbn in Sat. destruct decision; auto. exfalso. congruence.
    - right. intros x. apply mso_DM_finBigOR' in H.
      rewrite finBigAndCorrect in H. specialize (H x I).
      apply mso_DM_forall_neg in H. destruct H as [m H].
      exists m. intros k.
      apply mso_DM_exist_neg in H; auto.
      rewrite all1_correct in H. specialize (H k).
      apply mso_DM_neg_and, or_correct in H. cbn in H. trivial_decision. destruct H as [H|H].
      + intros L. now exfalso.
      + rewrite finBigUpdate2_changed in H by apply vars_for_elems_injective.
        unfold seq_to_sets, seq_map in H. intros _.
        destruct decision; auto.
  Qed.


    Context (X:FiniteSemigroup).
    Variable (f: nat -> X).

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

    Notation update := finBigUpdate2.

    Section ADD_Formula.

      Variables (vX : X -> SVar) (vP: X -> SVar).

      Definition in_vP v_n (g: X -> X) := AND { y | True} v_n el2 (vX y) ==>2 v_n el2 (vP (g y)).

      Lemma in_vP_correct v_n g I J : I # J |== in_vP v_n g <-> forall x, (I v_n) elS (J (vX x)) -> (I v_n) elS (J (vP (g x))).
      Proof.
        split; unfold in_vP.
        - intros Sat. rewrite finBigAndCorrect in Sat. intros x M.
          specialize (Sat x ). rewrite impl_correct in Sat. apply Sat; auto.
        - intros Imp. apply finBigAndCorrect. intros x _. apply impl_correct.
          intros In. apply Imp, In.
      Qed.

      Definition ADD_formula' v_n v_m x := (fun v_k v_Sk =>
                                             (in_vP v_n (fun y => y)) /\2
                                             (all1 v_k, (IsSucc v_k v_m ==>2 v_k el2 (vP x))) /\2
                                              all1 v_k,(v_n <=2 v_k ==>2 v_k <2 v_m ==>2
                                                    AND {y|True} (v_k el2 (vP y)) ==>2
                                                         (all1 v_Sk, ((IsSucc v_k v_Sk) ==>2 (in_vP v_Sk (fun z => add y z)))))
                                             ) (S (v_n + v_m)) (S (S (v_n + v_m))).
      Lemma ADD_formula'_correct v_n v_m x I J : (I v_n < I v_m) ->
         I # J |== ADD_formula' v_n v_m x <-> (forall y, (I v_n) elS J (vX y) -> (I v_n) elS (J (vP y))) /\
                                              ((pred (I v_m)) elS (J (vP x))) /\
                                              forall k, (I v_n) <= k < (I v_m) -> (forall y z, k elS J (vP y) -> (S k) elS J (vX z) -> (S k) elS J (vP (add y z))).
      Proof.
        intros L. split; unfold ADD_formula'.
        - intros [Pn [Pm Pk]]. repeat split.
          + now rewrite in_vP_correct in Pn.
          + rewrite all1_correct in Pm. specialize (Pm (pred (I v_m))).
            rewrite impl_correct, isSuccCorrect, el_correct in Pm. trivial_decision.
            apply Pm. omega.
          + intros k [Leq Le] y z MP MX. rewrite all1_correct in Pk.
            specialize (Pk k). rewrite !impl_correct, leq_correct, le_correct, finBigAndCorrect in Pk.
            trivial_decision. specialize (Pk Leq Le y Logic.I).
            rewrite impl_correct, el_correct, all1_correct in Pk. trivial_decision. specialize (Pk MP (S k)).
            rewrite impl_correct, isSuccCorrect in Pk. trivial_decision. specialize (Pk eq_refl).
            rewrite in_vP_correct in Pk. trivial_decision. now apply Pk.
        - intros [Pn [Pm Pk]]. repeat split.
          + now apply in_vP_correct.
          + apply all1_correct. intros k. rewrite impl_correct, isSuccCorrect, el_correct; auto. trivial_decision.
            intros E. now rewrite <-E in Pm.
          + apply all1_correct. intros k. rewrite !impl_correct, leq_correct, le_correct, finBigAndCorrect.
            trivial_decision. intros Leq Le y _. rewrite impl_correct, el_correct, all1_correct. intros MP kS.
            rewrite impl_correct, isSuccCorrect. trivial_decision. intros HkS. subst kS.
            apply in_vP_correct. trivial_decision. intros z. now apply Pk.
      Qed.

      Definition ADD_formula v_n v_m x:= finBigEx2 vP (Unique vP /\2 (ADD_formula' v_n v_m x)).

      Lemma ADD_formula_correct v_n v_m x I J: injective vX -> injective vP -> (forall x y, vX x <> vP y) -> (I v_n) < (I v_m) ->
                       I # (update vX (seq_to_sets f) J) |== ADD_formula v_n v_m x <-> ADD (extract (I v_n) (I v_m) f) = x.
      Proof.
        intros InjX InjP DisImg L. split; unfold ADD_formula.
        - intros [P [U Sat]] % finBigEx2_correct; auto.
          apply ADD_formula'_correct in Sat; oauto.
          apply (@unique_correct OmegaSequenceStructure) in U; auto.
          unfold I2chain in U.
          enough (forall j, (I v_n) <= j < (I v_m) -> j elS P (ADD (extract (I v_n) (S j) f))) as H.
          + assert (I v_n <= pred (I v_m) < I v_m) as H' by omega.
            specialize (H (pred (I v_m)) H'). clear H'.
            destruct Sat as [_ [Sat _]].
            rewrite finBigUpdate2_changed in Sat; auto.
            specialize (U x (pred (I v_m))).
            cbn in U. rewrite finBigUpdate2_changed in U; auto. specialize (U Sat (ADD (extract (I v_n) (I v_m) f))).
            rewrite finBigUpdate2_changed in U; auto.
            rewrite_eq (S (pred (I v_m)) = I v_m) in H. specialize (U H).
            now rewrite U.
          + destruct Sat as [Begin [_ Step]]. induction L.
            * intros j Q. assert (j = (I v_n)) by omega. subst j.
              rewrite ADD_single_extract.
              specialize (Begin (f (I v_n))).
              rewrite finBigUpdate2_changed, finBigUpdate2_unchanged, finBigUpdate2_changed in Begin; auto.
              unfold seq_to_sets, seq_map in Begin. cbn in Begin. trivial_decision.
              now apply Begin.
            * intros j Leq. decide (j < m) as [D|D].
              -- apply IHL; oauto. intros k O y z.
                 apply Step. omega.
              -- assert (j = m) by omega. subst j.
                 assert (m = S (pred m)) by omega. remember (pred m) as m'. subst m.
                 assert (I v_n <= m' < S (S m')) as H' by omega.
                 pose proof Step as Step'.
                 specialize (Step m' H' (ADD (extract (I v_n) (S m') f)) (f (S m'))).
                 rewrite finBigUpdate2_changed, finBigUpdate2_unchanged, 2finBigUpdate2_changed in Step; auto.
                 rewrite ADD_extract_last; auto. apply Step.
                 ++ apply IHL; oauto.
                    intros k O y z. apply Step'. omega.
                 ++ unfold seq_to_sets, seq_map. cbn. now trivial_decision.
        - intros A. apply finBigEx2_correct; auto.
          exists (seq_to_sets (fun k => ADD (extract (I v_n) (S k) f))). split.
          + apply unique_correct.
            unfold I2chain. intros z m. rewrite finBigUpdate2_changed; auto. unfold seq_to_sets, seq_map.
            intros M y. rewrite finBigUpdate2_changed; auto. intros M'.
            unfold memSet in *. simpl in *. destruct decision as [D|D] in M.
            destruct decision as [D'|D'] in M'. now rewrite <-D, <-D'.
            discriminate M'. discriminate M.
          + apply ADD_formula'_correct; oauto. repeat split.
            * intros y. rewrite finBigUpdate2_unchanged, 2finBigUpdate2_changed; auto.
              unfold seq_to_sets, seq_map. intros M. cbn. rewrite decision_true. reflexivity.
              cbn in M. rewrite_eq (I v_n - I v_n = 0). cbn. rewrite drop_correct'. cbn.
              destruct decision in M; auto. discriminate M.
            * rewrite finBigUpdate2_changed; auto. unfold seq_to_sets, seq_map. cbn.
              rewrite decision_true; auto. cbn in A.
              now rewrite_eq (pred (I v_m) - I v_n = I v_m - S(I v_n)).
            * intros k Leq y z.
              rewrite finBigUpdate2_changed, finBigUpdate2_unchanged, 2finBigUpdate2_changed; auto.
              unfold seq_to_sets, seq_map. simpl. intros B F.
              destruct decision as [D|D] in B.
              -- unfold memSet. simpl. rewrite decision_true. reflexivity.
                 rewrite ADD_extract_last; oauto. rewrite D.
                 destruct decision as [D'|D'] in F.
                 ++ now rewrite D'.
                 ++ discriminate F.
              -- discriminate B.
      Qed.
    End ADD_Formula.

    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).

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

    Notation vX := (vars_for_elems X 0).
    Notation vP := (vars_for_elems X (S(Cardinality X))).

    Definition tilde_w_equiv_mso v_i v_j := (fun v_m =>
         ex1 v_m, ((v_i <2 v_m /\2 v_j <2 v_m) /\2 OR {x|True} (ADD_formula vX vP v_i v_m x /\2 ADD_formula vX vP v_j v_m x))
      ) (S(v_i + v_j)).

    Lemma vX_vP_disjoint x y : vX x <> vP y.
    Proof.
      pose proof (vars_for_elems_bound (X:=X) 0 x).
      pose proof (vars_for_elems_bound (X:=X) (S (Cardinality X)) y). omega.
    Qed.

    Lemma tilde_w_equiv_mso_correct i j I J: i ~~# j <-> I [0 := i][1:=j] # (update vX (seq_to_sets f) J) |== tilde_w_equiv_mso 0 1.
    Proof.
      split; unfold tilde_w_equiv_mso.
      - intros [m [[L1 L2] E]]. exists m. repeat split.
        + cbn. now trivial_decision.
        + cbn. now trivial_decision.
        + apply finBigOrCorrect. exists (F i m). repeat split; auto.
          * apply ADD_formula_correct; auto using vars_for_elems_injective,vX_vP_disjoint;
            cbn; now trivial_decision.
          * apply ADD_formula_correct; auto using vars_for_elems_injective, vX_vP_disjoint;
            cbn; now trivial_decision.
      - intros [m [[L1 L2] E]]. cbn in L1,L2. trivial_decision.
        exists m. repeat split; auto.
        apply finBigOrCorrect in E. destruct E as [x [[E1 % ADD_formula_correct E2 % ADD_formula_correct] _]];
        auto using vars_for_elems_injective, vX_vP_disjoint; trivial_decision; auto.
        now rewrite E1, E2.
    Qed.

    Lemma infinite_equiv_indices_dm : (exists i, forall j, exists k, j < k /\ i ~~# k) \/ (forall i, exists j, forall k, j >= k \/ ~ i~~# k).
    Proof.
      destruct (MSO_XM (fun n => 0) (update vX (seq_to_sets f) (fun n => singletonSet 0)) (ex1 0, all1 2, ex1 1, 2 <2 1 /\2 tilde_w_equiv_mso 0 1)) as [D|D].
      - left. destruct D as [i D]. exists i. intros j.
         rewrite all1_correct in D. specialize (D j). destruct D as [k [L E]].
         exists k. split.
         + cbn in L. now trivial_decision.
         + rewrite tilde_w_equiv_mso_correct with (I := (fun n => 0)[2:=j]) (J:= fun n => singletonSet 0). apply (mso_coincidence' E).
           * intros x F. repeat (destruct decision; auto). exfalso. congruence.
           * intros Z _. reflexivity.
      - right. intros i.
        rewrite mso_DM_exist_neg' in D; auto.
        rewrite all1_correct in D. specialize (D i).
        apply mso_DM_forall_neg in D. destruct D as [j D].
        exists (i + S j). intros k.
        apply mso_DM_exist_neg in D. rewrite all1_correct in D.
        specialize (D k).
        apply mso_DM_neg_and, or_correct in D. destruct D as [D|D].
        + cbn in D. trivial_decision. left. omega.
        + right. intros NE. rewrite tilde_w_equiv_mso_correct with (I:= (fun n => 0)[2:=j])(J:= fun n => singletonSet 0) in NE.
          apply D. apply (mso_coincidence' NE).
          * intros x F. repeat (destruct decision; auto). exfalso. congruence.
          * intros Z _. reflexivity.
    Qed.


Lemma mso_ramseyan_factorization : admits_ramseyan_factorization f.
Proof.
  apply ramseyan_factorization.
  - apply ipp_dm.
  - apply infinite_equiv_indices_dm.
Qed.



End MSOClassicalImpliesRamseyFac.

Summary: Equivalence of AR, RF, BC, BU, and SL

Theorem additive_ramsey_iff_ramsey_fac: (forall C, AdditiveRamsey C <-> RamseyFac C).
Proof.
  intros C. symmetry. apply RamseyFac_iff_AdditiveRamsey.
Qed.

Theorem mso_xm_implies_ramsey_fac : MSO_Classical -> forall C, RamseyFac C.
Proof.
  intros MSO_XM C f. now apply mso_ramseyan_factorization.
Qed.

Theorem additiveRamsey_implies_compl : (forall C, AdditiveRamsey C) -> (forall C, ComplClosed C /\ XM_WordProblem C).
Proof.
  intros AR C. split; intros aut.
  - exists (complement aut). apply (@complement_correct (OmegaStructure AR)).
  - apply (@xm_word_problem (OmegaStructure AR)).
Qed.

Theorem additiveRamsey_implies_mso_classical : (forall C, AdditiveRamsey C) -> MSO_Classical.
Proof.
  intros AR. intros I J phi. apply (@mso_classic (OmegaStructure AR)).
Qed.

Theorem compl_closed_xm_word_problem_implies_ramsey_fac: forall (C:FiniteSemigroup) , (ComplClosed C) -> (XM_WordProblem C) -> RamseyFac C.
Proof.
  intros C CC XM.
  now apply RamseyFacFromComplement.
Qed.

Definition UPDet X:= forall (aut1 aut2 : NFA X), (forall (x y : String X), L_B aut1 (x +++ y to_omega) <-> L_B aut2 (x +++ y to_omega)) -> (L_B aut1 =$= L_B aut2).

Lemma up_eq_compl: forall X , (ComplClosed X /\ XM_WordProblem X <-> UPDet X).
Proof.
  intros X. split.
  - intros [CC XM].
    enough (forall (aut1 aut2 : NFA X), (forall x y, L_B aut1 (x +++ y to_omega) <-> L_B aut2 (x +++ y to_omega)) -> (L_B aut1 <$= L_B aut2)) as H.
    + intros aut1 aut2 UPEq. split.
      * apply H, UPEq.
      * apply H. intros x y. symmetry. apply UPEq.
    + intros aut1 aut2 UPEq w.
      destruct (CC aut2) as [aut2C Compl].
      destruct (dec_language_empty_informative_periodic (intersect aut1 aut2C)) as [[u [v [L1 L2C] % intersect_correct]]|D].
      * exfalso.
        apply Compl in L2C. apply L2C, UPEq, L1.
      * intros L1. destruct (XM aut2 w) as [L2|NL2]; auto.
        exfalso. apply (D w), intersect_correct. split; auto.
        now apply Compl.
  - intros UPDet.
    unfold L_A, ASeq in *. simpl in *. unfold unfold in *.
    assert (forall (aut: NFA X) w, L_B (complement aut) w \/ L_B aut w) as H.
      { intros aut. enough (L_B (union (complement aut) aut) =$= L_B univ_aut) as H'.
        - intros w. rewrite union_correct in H'. apply H', univ_aut_correct, I.
        - apply UPDet. intros x y. split.
          + intros _. now apply univ_aut_correct.
          + intros _. apply union_correct.
            change ((L_B (complement aut) \$/ L_B aut) (unfold (mkUPSeq x y))).
            apply (complement_complete (AC:=UPStructure)). exact I. }
    assert (forall (aut: NFA X), L_B aut /$\ L_B (complement aut) <$= empty_language) as H2.
      { intros aut w [L C].
        destruct (dec_language_empty_informative_periodic (intersect aut (complement aut))) as [[u [v [L1 L2C] % intersect_correct]]|D].
        - rewrite (complement_correct (AC:=UPStructure) aut (mkUPSeq u v)) in L2C.
          now apply L2C.
        - apply (D w), intersect_correct. now split.
      }
   split.
   + intros aut. exists (complement aut). intros w. split.
     * intros LC L. now apply (H2 aut w).
     * intros NL. destruct (H aut w).
       -- assumption.
       -- now exfalso.
   + intros aut w. specialize (H aut w). destruct H.
     * right. intros L. now apply (H2 aut w).
     * now left.
Qed.

Addition: XM Word Problem suffices to derive the IPP

Section XMWordProblemImpliesInfinitePigeonholePrinciple.

  Variable (xm_word_problem: forall (A:finType) (aut: NFA A) w, L_B aut w \/ ~ L_B aut w).

  Definition finite (A: finType) (a:A) (w:Seq A) := exists n, forall m, m >= n -> w m <> a.


  Section AtLeastOneNFA.
    Variable (A: finType).
    Variable (a:A).

    Notation state := finType_bool.
    Notation no_a := true.
    Notation some_a := false.

    Definition transition_at_least_one s b s' := match s, s' with
      | no_a, no_a => True
      | no_a, some_a => b = a
      | some_a, some_a => True
      | some_a, no_a => False
     end.

    Instance dec_transition_at_least_one s b s' : dec (transition_at_least_one s b s').
    Proof. destruct s,s'; auto. Qed.
    Definition at_least_one_nfa := mknfa transition_at_least_one (fun s => s = no_a) (fun s => s = some_a).

    Lemma at_least_one_nfa_correct : L_B at_least_one_nfa =$= (fun w => exists n, w n = a).
    Proof.
      intros w. split.
      - intros [r [V [I F]]].
        destruct (F 1) as [m [P1 P2]].
        destruct (can_find_next_position (P:= fun x => x = some_a) (n:=0) (m:=m) (w:=r)) as [n [Q1 [Q2 Q3]]]; oauto.
        exists (pred n). specialize (V (pred n)). cbn in V.
        assert ( 1 <= n). { destruct n; oauto. cbn in I. congruence. }
        rewrite_eq (S (pred n) = n) in V.
        rewrite Q2 in V. destruct (r (pred n)) eqn:H2.
        + now cbn in V.
        + exfalso. apply (Q3 (pred n)); oauto.
      - intros [n P].
        exists ((mkstring (fun n => no_a) n) +++ (fun n => some_a)). repeat split.
        + intros m. decide (m <= n).
          * rewrite prepend_string_begin by comega. decide (m = n).
            -- subst m. rewrite prepend_string_rest by comega. now rewrite P.
            -- now rewrite prepend_string_begin by comega.
          * now repeat rewrite prepend_string_rest by comega.
        + unfold initial. now rewrite prepend_string_begin by comega.
        + intros m. decide (m <= n).
          * exists (S n). split; oauto. now rewrite prepend_string_rest by comega.
          * exists m. split; oauto. now rewrite prepend_string_rest by comega.
    Qed.
  End AtLeastOneNFA.

  Section AllNotNFA.
    Variable (A: finType).
    Variable (a:A).

    Notation state := finType_bool.
    Notation all_not_a := true.
    Notation some_a := false.

    Definition transition_all s b s' := match s, s' with
      | all_not_a, some_a => True
      | all_not_a, all_not_a => b <> a
      | some_a, some_a => True
      | some_a, all_not_a => False
     end.

    Instance dec_transition_all s b s' : dec (transition_all s b s').
    Proof. destruct s,s'; auto. Qed.
    Definition all_not_nfa := mknfa transition_all (fun s => s = all_not_a) (fun s => s = all_not_a).

    Lemma accepting_all (r: Run all_not_nfa) w : accepting r w -> r === (fun n => all_not_a).
    Proof.
      intros [V [I F]] n.
      decide (r n = all_not_a) as [D|D]. {assumption. }
      exfalso.
      assert (forall k, r (n + k) = some_a) as H. {
        intros k. induction k.
        - rewrite_eq (n + 0 = n). destruct (r n); congruence.
        - specialize (V (n + k)). rewrite IHk in V. cbn in V.
          rewrite_eq (n + S k = S (n + k)). now destruct (r (S (n + k))).
      }
      destruct (F n) as [m [P Q]]. cbn in Q.
      rewrite_eq (m = n + (m - n)) in Q. rewrite H in Q. congruence.
    Qed.

    Lemma all_not_nfa_correct : L_B all_not_nfa =$= (fun w => forall n, w n <> a).
    Proof.
      intros w. split.
      - intros [r Acc] n.
        destruct (r n) eqn:H.
        + destruct (r (S n)) eqn:H2.
          * destruct Acc as [V _]. specialize (V n). now rewrite H, H2 in V.
          * pose (accepting_all Acc (S n) ). congruence.
        + pose (accepting_all Acc n ). congruence.
      - intros N. exists (fun n => all_not_a). repeat split.
        + firstorder.
        + intros n. exists n. split; oauto. now cbn.
    Qed.
  End AllNotNFA.

  Lemma not_finite_intermediate (A:finType) (a:A) w : ~ finite a w -> forall n, ~forall m, m >= n -> w m <> a.
  Proof.
    intros N n.
    destruct (xm_word_problem (all_not_nfa a) (drop n w)) as [H|H].
    - exfalso. apply N. exists n. intros m L.
      pose (P:=all_not_nfa_correct a (drop n w)). rewrite P in H.
      specialize (H (m - n)). rewrite drop_correct in H.
      now rewrite_eq (n + (m - n) = m) in H.
    - intros Q. apply H. apply all_not_nfa_correct. intros m. rewrite drop_correct.
      apply Q. omega.
  Qed.

  Lemma intermediate_infinite (A:finType) (a:A) w : (forall n, ~forall m, m >= n -> w m <> a) -> infinite a w.
  Proof.
    intros N n.
    destruct (xm_word_problem (at_least_one_nfa a) (drop n w)) as [H|H].
    - apply at_least_one_nfa_correct in H. destruct H as [m P].
      exists (n +m) . rewrite drop_correct in P. split; oauto.
    - exfalso. apply (N n). intros m G. decide (w m = a).
      + exfalso. apply H. apply at_least_one_nfa_correct. exists (m - n).
        rewrite drop_correct. rewrite <-e. f_equal. omega.
      + assumption.
  Qed.

  Lemma not_finite_implies_infinite (A:finType) (a:A) w : ~ finite a w -> infinite a w.
  Proof.
    intros P. now apply intermediate_infinite, not_finite_intermediate.
  Qed.

  Variable (A:finType).

  Section FiniteAut.
    Variable (a:A).

    Definition fin_nfa := prepend_nfa univ_aut (all_not_nfa a).

    Lemma fin_nfa_correct : L_B fin_nfa =$= finite a.
    Proof.
      unfold fin_nfa. rewrite prepend_nfa_correct, all_not_nfa_correct, univ_aut_scorrect. intros w. split.
      - intros [v [w' [E [_ N]]]].
        exists (S (|v|) ). intros m L. rewrite E.
        rewrite prepend_string_rest by omega. apply N.
      - intros [n N]. apply split_position_lang_prepend. exists n. split; auto.
        intros k. rewrite drop_correct. apply N. omega.
    Qed.

  End FiniteAut.

  Definition all_fin_nfa := big_intersection (map fin_nfa (elem A)).
  Lemma all_fin_nfa_correct: L_B all_fin_nfa =$= fun w => forall a, finite a w.
  Proof.
    unfold all_fin_nfa.
    rewrite big_intersection_correct. intros w. split; intros P a.
    - apply fin_nfa_correct, P, in_map_iff. eauto.
    - intros [aut [Y Z]]%in_map_iff. subst a. now apply fin_nfa_correct.
  Qed.

  Lemma big_intersection_compl_correct (B: finType) (l: list (NFA B)): (L_B (big_intersection l))^$~ =$= (fun w => exists a, a el l /\ (L_B a)^$~ w ).
  Proof.
    intros w. split.
    - intros I. induction l; cbn in I.
      + exfalso. now apply I, univ_aut_correct.
      + destruct (xm_word_problem a w) as [D|D].
        * destruct IHl as [a' [P Q]].
          -- intros I'. now apply I, intersect_correct.
          -- exists a'. split; auto.
        * exists a. split; auto.
    - intros [a [P Q]] I. apply Q.
      now apply big_intersection_correct with (l:=l).
  Qed.

  Lemma all_finite_impossible (w: Seq A) : ~ (forall a, finite a w).
  Proof.
    intros F.
    enough (exists n, forall a, w n <> a) as [n H].
    - specialize (H (w n)). congruence.
    - enough (exists n, forall a, a el (elem A) -> forall m, m >= n -> w m <> a) as [n H].
      + exists n. intros a. apply H with (m := n); auto.
      + induction (elem A).
        * exists 0. now intros.
        * destruct (F a) as [n P].
          destruct IHl as [m Q].
          exists (max n m). intros b [E|E] k L.
          -- subst b. apply P. pose (Nat.le_max_l n m). omega.
          -- apply (Q b E). pose (Nat.le_max_r n m). omega.
  Qed.

  Lemma closure_complement_implies_finite_type_seq: InfinitePigeonholePrinciple A.
  Proof.
    intros w.
    destruct (xm_word_problem all_fin_nfa w) as [D|D].
    - exfalso. apply all_finite_impossible with (w:=w). now apply all_fin_nfa_correct.
    - apply big_intersection_compl_correct in D. destruct D as [a' [[a [X Y]]%in_map_iff Q]]. subst a'.
      exists a. apply not_finite_implies_infinite. intros F. now apply Q, fin_nfa_correct.
  Qed.
End XMWordProblemImpliesInfinitePigeonholePrinciple.