Set Implicit Arguments.

Require Import Coq.Init.Nat.
Require Import Coq.Relations.Relation_Definitions.

Require Import BasicDefs.
Require Import Seqs.
Require Import FinType.
Require Import Ramsey.
Require Import NFAs.
Require Import RegularLanguages.
Require Import Buechi.

Close Scope list_scope.
Open Scope string_scope.

Complementation of Buechi Automata

Büchi Equivalence Relation


Section BuechiEquivalenceRelation.

  Context {A:finType}.
  Context {aut:NFA A}.

  Definition transforms (w :String A) (s s': state aut) :=
      exists r, path r w s s'.

  Definition transforms_final (w:String A) (s s': state aut) :=
      exists r, path r w s s' /\ exists n, n <= S (|w|) /\ final_state (r n).

  Notation " s1 '===>' s2 'on' w" := (transforms w s1 s2) (at level 10).
  Notation " s1 '=!=>' s2 'on' w" := (transforms_final w s1 s2) (at level 10).

Facts about ===> and =!=> for Concattenation

  Lemma final_transform_implies_transform s s' w: s =!=> s' on w -> s ===> s' on w.
  Proof.
    intros [r [P _]]. now exists r.
  Qed.

  Lemma split_transforms u w s s': s ===> s' on (u ++ w) -> exists s'', s ===> s'' on u /\ s'' ===> s' on w.
  Proof.
    intros [r W].
    destruct (split_path W) as [s'' [P1 P2]].
    exists s''. split.
    - now exists r.
    - now exists ((drop (S (| u |)) r)).
  Qed.

  Lemma combine_transforms u v s s' s'' : s ===> s'' on u -> s'' ===> s' on v -> s ===> s' on (u++v).
  Proof.
    intros [r1 W1] [r2 W2].
    exists ((mkstring r1 (|u|)) +++ r2).
    now apply (concat_paths (aut:=aut) (s'':=s'')).
  Qed.

  Lemma split_final_transforms u w s s': s =!=> s' on (u ++ w) -> exists s'',
         (s =!=> s'' on u /\ s'' ===> s' on w) \/ (s ===> s'' on u /\ s'' =!=> s' on w).
  Proof.
    intros [r [V [n [L F]]]].
    destruct (split_path V) as [s'' [P1 P2]].
    exists s''.
    decide (n <= S(|u|)) as [D|D].
    - left. split.
      + exists r. split; firstorder.
      + now exists (drop (S (| u |)) r) .
    - right. split.
      + now exists r.
      + exists (drop (S (| u |)) r). split; auto.
        exists (n - (S(|u|))). split.
        * simpl in L. omega.
        * rewrite drop_correct''; oauto.
  Qed.

  Lemma combine_final_transforms_left u w s s' s'' : s =!=> s'' on u -> s'' ===> s' on w -> s =!=> s' on (u++w).
  Proof.
    intros [r1 [W1 [n1 [L1 F1]]]] [r2 W2].
    exists ((mkstring r1 (|u|)) +++ r2). split.
    - now apply (concat_paths (aut:=aut)) with (s'':=s'').
    - exists n1. split; oauto.
      decide (n1 = S (|u|)) as [D|D].
      + subst n1. rewrite prepend_string_rest by comega. cbn.
        rewrite_eq (|u| - (|u|) = 0).
        now rewrite (proj1 (proj2 W2)), <-(proj2(proj2 W1)).
      + now rewrite prepend_string_begin by comega.
  Qed.

  Lemma combine_final_transforms_right u w s s' s'' : s ===> s'' on u -> s'' =!=> s' on w -> s =!=> s' on (u++w).
  Proof.
    intros [r1 W1] [r2 [W2 [n2 [L2 F2]]]].
    exists (mkstring r1 (|u|) +++ r2). split.
    - now apply (concat_paths (aut:=aut)) with (s'':=s'').
    - exists (S(|mkstring r1 (|u|)|)+n2). split; oauto.
      rewrite prepend_string_rest' ; oauto.
  Qed.

Definition of the Equivalence Relation ~~
Extensionality of ~~

  Global Instance transforms_extensional: Proper (strings_equal ==> eq ==> eq ==> iff) transforms.
  Proof.
    intros u v E s_1 s_1' E_1 s_2 s_2' E_2. subst s_1' s_2'. split;
    intros [r P]; exists r; [now rewrite <-E|now rewrite E].
  Qed.

  Global Instance transforms_final_extensional: Proper (strings_equal ==> eq ==> eq ==> iff) transforms_final.
  Proof.
    intros u v E s_1 s_1' E_1 s_2 s_2' E_2. subst s_1' s_2'. split;
    intros [r [P1 P2]]; exists r; split.
    now rewrite <-E. now rewrite <-(proj1 E). now rewrite E. now rewrite (proj1 E).
  Qed.

Decidability of ~~

  Instance dec_transforms : forall s s' w, dec (s ===> s' on w).
  Proof.
    intros s s' w. unfold transforms.
    enough (dec (exists r : ConstLengthString (S (|w|)), path (to_seq r) w s s')) as H.
    - destruct H as [H|H].
      + left. destruct H as [r H]. now exists (to_seq r).
      + right. intros [r E]. apply H. exists (to_bounded r).
        now apply bounded_run_is_valid_path.
    - auto.
  Qed.

  Instance dec_transforms_final : forall s s' w, dec(s =!=> s' on w).
  Proof.
  intros s s' w. unfold transforms_final.
    enough (dec (exists r : (state aut) ^ (finType_Le_K (S (|w|))), path (to_seq r) w s s' /\
     (exists L: Le_K (S (| w |)), final_state (applyVect r L)))) as H.
    - destruct H as [H|H].
      + left. destruct H as [r [H1 [L H2]]]. exists (to_seq r). split; auto.
        exists (proj1_sig L). split.
        * apply le_L_is_le.
        * now rewrite to_seq_unchanged'.
      + right. intros [r [E1 [n [L E2]]]]. apply H. exists (to_bounded r). split.
        * now apply bounded_run_is_valid_path.
        * exists (create_Le_K L). now rewrite (to_bounded_unchanged).
    - auto.
  Qed.

Given ===> or =!=> we can compute the run on the NFA

  Lemma compute_run_transforms s s' w : s ===> s' on w -> Sigma r, path r w s s'.
  Proof.
    intros T.
    enough ({r: (state aut) ^ (finType_Le_K (S (|w|))) | path (to_seq r) w s s'}).
    - destruct X as [r P]. now exists (to_seq r).
    - apply finType_cc.
      + auto.
      + destruct T as [r P]. exists (to_bounded r).
        now apply bounded_run_is_valid_path.
  Qed.

  (* Need the products instead of conjunctions in this lemma because we will destruct it in functions later *)
  Lemma compute_run_final_transforms s s' w : s =!=> s' on w -> Sigma r, prod (path r w s s') (Sigma n, prod (n <= S (|w|)) (final_state (r n))).
  Proof.
    intros T.
    enough ({r: (state aut) ^ (finType_Le_K (S (|w|)))| (path (to_seq r) w s s') /\ ((exists (L : Le_K (S (| w |))), final_state (applyVect r L)))}).
    - destruct X as [r [P1 [L P2]%finType_cc]]; auto.
      exists (to_seq r). split;auto.
      exists (proj1_sig L). split.
      + apply le_L_is_le.
      + now rewrite to_seq_unchanged'.
    - apply finType_cc; auto.
      destruct T as [r [P1 [n [P2 P3]]]].
      exists (to_bounded r). split.
      + now apply bounded_run_is_valid_path.
      + exists (create_Le_K P2).
        now rewrite to_bounded_unchanged.
  Qed.

  Definition run_for_transforms s s' w (T: s ===> s' on w) := projT1 (compute_run_transforms T).
  Lemma run_for_transforms_correct s s' w (T:s ===> s' on w): path (run_for_transforms T) w s s'.
  Proof.
    unfold run_for_transforms. now destruct compute_run_transforms.
  Qed.

Finite Type for Equivalence Classes of ~~

  Definition EqClass := (? finType_bool) ^ (state aut (x) state aut).
  Notation transformsBehavior V s s' := (fun w => match (applyVect V (s,s')) with
               | None => ~ (s ===> s' on w)
               | Some false => (s ===> s' on w) /\ ~(s =!=> s' on w)
               | Some true => s =!=> s' on w
              end).

  Implicit Types (V W U : EqClass).


  Definition buechi_eq_class w : EqClass:= (vectorise (fun z => match z with
                (s,s') => if (decision (s ===> s' on w))
                            then if (decision (s =!=> s' on w))
                                then Some true
                                else Some false
                            else None end)).

  Definition eqClass V : StringLang A := fun w => buechi_eq_class w = V.


  Notation "{[ V ]}" := (eqClass V) (at level 0).

  Lemma buechi_eq_class_correct w: {[buechi_eq_class w]} w.
  Proof.
    unfold eqClass. reflexivity.
  Qed.

  Notation "w ~~ v" := ( buechi_eq_class w = buechi_eq_class v) (at level 60).
  Notation buechi_equiv := (fun v w => v~~w).

  Instance buechi_eq_class_proper : Proper (strings_equal ==> eq) buechi_eq_class.
  Proof.
    intros u v E. apply vector_eq. intros [s s']. unfold buechi_eq_class.
    rewrite 2apply_vectorise_inverse. repeat destruct decision; auto;
    exfalso; rewrite E in *; tauto.
  Qed.

  Lemma at_most_one_eq_class w V : {[V]} w <-> V = buechi_eq_class w.
  Proof.
    unfold eqClass. split; intros; congruence.
  Qed.

  Lemma equivalent_in_equivalence_class' V w w': {[V]} w -> {[V]} w' -> w ~~ w'.
  Proof.
    intros WI W'I'. apply at_most_one_eq_class in WI. apply at_most_one_eq_class in W'I'.
    now rewrite <-WI, <-W'I'.
  Qed.

  Instance equivalence_class_closed_proper: Proper (eq ==> buechi_equiv ==> iff) eqClass.
  Proof.
    intros i j <- u v T. split; intros T' % at_most_one_eq_class; rewrite T'; [rewrite T | rewrite <-T]; apply buechi_eq_class_correct.
  Qed.

  Instance equivalence_class_extensional_proper: Proper (eq ==> strings_equal ==> iff) eqClass.
  Proof.
    intros i j <- u v T. split; intros T' % at_most_one_eq_class; rewrite T'; [rewrite T | rewrite <-T]; apply buechi_eq_class_correct.
  Qed.

  Corollary eq_classes_extensional V: StringLang_Extensional {[V]}.
  Proof.
    intros w w' T E. now rewrite <-E.
  Qed.

  Lemma equivalent_in_equivalence_class {u} {v} : u ~~ v <-> forall s s',
      (s ===> s' on u <-> s ===> s' on v) /\
      (s =!=> s' on u <-> s =!=> s' on v).
  Proof.
    split.
    - intros T s s'.
       assert (applyVect (buechi_eq_class u) (s,s') = applyVect (buechi_eq_class v) (s,s')) as H by now rewrite T.
       unfold buechi_eq_class in H. rewrite !apply_vectorise_inverse in H. repeat split;
       intros T'; repeat destruct decision in H; (try now (exfalso; auto using final_transform_implies_transform)); auto.
    - intros T. apply vector_eq. intros [s s']. specialize (T s s').
       unfold buechi_eq_class. rewrite !apply_vectorise_inverse. destruct T as [[T1 T2][T3 T4]].
       repeat destruct decision; (try now (exfalso; auto using final_transform_implies_transform)); auto.
  Qed.

~~ is a congruence relation

  Lemma tilde_congruence u v w: u ~~ v -> (u ++ w) ~~ (v ++ w).
  Proof.
    intros UV. rewrite equivalent_in_equivalence_class in UV. apply equivalent_in_equivalence_class. intros s s'. split.
    - split; intros T; destruct (split_transforms T) as [s'' [P1 P2]];
       destruct (UV s s'') as [[? ?][? ?]]; eauto using combine_transforms.
    - split; intros T; destruct (split_final_transforms T) as [s'' [[F1 P2]|[P1 F2]]]; destruct (UV s s'') as [[? ?] [? ?]];
      eauto using combine_final_transforms_left, combine_final_transforms_right.
  Qed.

  Instance dec_buechi_eq_class V w: dec( {[V]} w).
  Proof.
    unfold eqClass. auto.
  Qed.

Regularity of Equivalence Classes

There are two ways to show this: using Myhill Nerode or Closure Properties of NFAs

  Section BuechiEquivalenceClassRecognizableMyhillNerode.

Myhill-Nerode is only proven for Strings including the empty String. We do not prove it here. Quickly define EStrings (String including the empty one) and the EString language of an NFA

    Definition EString := option (String A).

    Definition econcat (s1 s2: EString) := match s1,s2 with
       | None, None => None
       | None, Some _ => s2
       | Some _ , None => s1
       | Some s1, Some s2 => Some (s1 ++ s2) end.

    Definition seaccepting (aut: NFA A) r s := match s with
      | None => initial_state (r 0) /\ final_state (aut:=aut) (r 0)
      | Some w => saccepting r w
    end.

    Definition selanguage (aut:NFA A) := fun w => exists r, seaccepting (aut:=aut) r w.

Myhill-Nerode Theorem, without proof

    Definition right_congruent (X: Type) (f: EString -> X) := forall x y, f x = f y -> forall a, f (econcat x a) = f (econcat y a).
    Definition classifier (X: finType) (f: EString -> X) := right_congruent f.
    Definition refines (X: finType) (f:EString ->X) (L: Language EString) := forall x y, f x = f y -> (L x <-> L y).

    Definition MyhillNerode (X:finType) (f: EString -> X) (L: Language EString) :=
      (forall s, dec (L s)) -> classifier f -> refines f L -> { aut| selanguage aut =$= L}.

    Lemma equalSELangImpliesEqualSLang (a: NFA A) (L: StringLang A) (P:Prop): selanguage a =$= (fun (s:EString) => match s with
         | None => P
         | Some w => L w
       end ) -> L_S a =$= L.
    Proof.
      intros E w.
      now specialize (E (Some w)).
    Qed.

No we obtain the desired NFA to recognize a equivalence class when we use the equivalence classes as classifier.

    Lemma buechi_equiv_class_NFA_recognizable_MyhillNerode V: (forall X f L, MyhillNerode (X:=X) f L) ->
        Sigma aut, slanguage aut =$= {[V]}.
    Proof.
      intros M.
      pose (f:= fun (s:EString) => match s with
            | None => None
            | Some w => Some (buechi_eq_class w)
           end).
      pose (L:= fun(s:EString) => match s with
            | None => False
            | Some w => {[V]} w
           end).
      assert (forall s, dec (L s)) as decL. { intros s. unfold L. destruct s; auto. }
      assert (classifier f) as clasF. { unfold f. intros x y E a. destruct x,y,a ;simpl; try discriminate; auto.
         f_equal. apply tilde_congruence. congruence. }
      assert (refines f L) as ref. { unfold f, L. intros x y E. destruct x as [w|]; destruct y as [v|]; try discriminate.
         - split; intros W; apply at_most_one_eq_class; apply at_most_one_eq_class in W; congruence.
         - tauto. }
      destruct (M (? EqClass) f L decL clasF ref) as [a P].
      exists a.
      unfold f, L in *.
      now apply (equalSELangImpliesEqualSLang (P:=False)).
  Qed.

  End BuechiEquivalenceClassRecognizableMyhillNerode.

This Section is not as nice, but it is not as intersting. If I would use the automata of the Doczkal library to have a proof for Myhill Nerode and to apply the section before, but because I use the finite types of Jan's bachelor thesis it was right easy to show the equivalence of my NFAs to his and to obtain closure properties from them

  Section BuechiEqivalenceClassRecognizable.

    Section TransformsRecognizable.
      Variable (startS : state aut).
      Variable (endS: state aut).

      Definition tf_aut := mknfa (transition (aut:=aut)) (fun s => s = startS) (fun s => s = endS).

      Lemma tf_accepts_tranforms w: (startS ===> endS on w)-> L_S tf_aut w.
      Proof.
        intros [r [V [B E]]].
        exists r.
        repeat split; auto.
      Qed.

      Lemma tf_is_transforms w: L_S tf_aut w -> (startS ===> endS on w).
      Proof.
        intros [r [V [I F]]].
        exists r. repeat split; auto.
      Qed.

      Lemma tf_recognizes_transforms w : startS ===>endS on w <-> (L_S tf_aut w).
      Proof.
        split. apply tf_accepts_tranforms. apply tf_is_transforms.
      Qed.

    End TransformsRecognizable.

    Section TransformsFinalRecognizable.
      Variable (startS : state aut).
      Variable (endS: state aut).

      Definition tff_state := (state aut) (x) finType_bool.
      Definition tff_transition s a s' := match s,s' with
           | (s,b),(s', b') => transition (aut:=aut) s a s' /\ (b' = true -> (b = true \/ final_state s')) end.

          (* | (s, true),(s',true) => transition (aut:=aut) s a s'
           | (s, false), (s', true) => transition (aut:=aut) s a s' /\ final_state s'
           | (s, false), (s', false) => transition (aut:=aut) s a s'
           | _,_ => False
           end.*)

      Instance tff_transition_dec s a s': dec (tff_transition s a s'). Proof. unfold tff_transition. destruct s as [s [|]];destruct s' as[s' [|]]; auto. Qed.

      Definition tff_aut := mknfa tff_transition (fun q => q = (startS,false) \/ (q = (startS,true) /\ final_state startS)) (fun q => q = (endS, true)).

      Lemma tff_accepts_tranforms_final w: (startS =!=> endS on w)-> L_S tff_aut w.
      Proof.
        intros [r [[V [B E]] [k [Lk Fk]]]].
        exists (fun n => if (decision (n < k))
                         then (r n, false)
                         else (r n, true)).
        repeat split.
        - intros n L. destruct decision.
          + destruct decision; split; auto using V.
            intros _. right. now rewrite_eq (S n = k).
          + rewrite decision_false by omega. cbn. split. now apply V. tauto.
        - unfold sinitial. destruct decision; cbn; rewrite B.
          + tauto.
          + rewrite_eq (k = 0) in Fk. rewrite B in Fk. tauto.
        - cbn. trivial_decision. now rewrite E.
      Qed.

      Lemma tff_is_transforms_final w: L_S tff_aut w -> startS =!=> endS on w.
      Proof.
        intros [r [V [I F]]].
        exists (seq_map fst r).
        repeat split; unfold seq_map.
        - intros n L. specialize (V n).
          destruct (r n) as[sn ?]; destruct (r (S n)) as[ sSn ?]. now apply V.
        - destruct I as [I | [I _]]; destruct (r 0); cbn in *; congruence.
        - unfold sfinal in F.
          destruct (r (S(|w|))). cbn in *. congruence.
        - assert (0 <= S(|w|)) as H by omega.
          pose ( p := fun (s:tff_state) => snd s = true).
          assert (snd (r (S(|w|))) = true) as H2. { simpl in F. rewrite F. now simpl. }
          assert (forall s, dec (p s)) as decP. { intros s. unfold p. auto. }
          destruct (can_find_next_position H H2) as [n [L [P Q]]]; subst p.
          exists n. split.
          + omega.
          + destruct n.
            * destruct I as [I | [I1 I2]].
              -- exfalso. destruct (r 0). cbn in P. congruence.
              -- now rewrite I1.
            * specialize (V n).
              destruct (r n) as [rn [|]] eqn:N; destruct (r (S n)) as [rSn [|]].
              -- exfalso. apply (Q n); oauto. now rewrite N.
              -- exfalso. simpl in P. congruence.
              -- destruct V as [_ [V|V]]; oauto. now exfalso.
              -- exfalso. simpl in P. congruence.
       Qed.

      Lemma tff_recognizes_transforms_final w: (startS =!=> endS on w) <-> L_S tff_aut w.
      Proof.
        split. apply tff_accepts_tranforms_final. apply tff_is_transforms_final.
      Qed.
   End TransformsFinalRecognizable.

   Context { V : EqClass}.

   Definition s_s'_pair_aut (p :(state aut) (x) (state aut)):=
    let (s, s') := p in
    match (applyVect V (s, s')) with
       | None => scomplement (tf_aut s s')
       | Some false => sdiff (tf_aut s s') (tff_aut s s')
       | Some true => (tff_aut s s')
   end.

   Lemma s_s'_pair_aut_correct s s': L_S (s_s'_pair_aut (s, s')) =$= transformsBehavior V s s'.
   Proof.
     unfold s_s'_pair_aut. intros v. destruct (applyVect V (s,s')) as [[|]|].
     - now rewrite tff_recognizes_transforms_final.
     - rewrite (sdiff_correct (tf_aut s s') (tff_aut s s') v ).
       now rewrite tff_recognizes_transforms_final, tf_recognizes_transforms.
     - now rewrite (scomplement_correct (tf_aut s s') v), tf_recognizes_transforms.
   Qed.

   Definition buechi_equiv_class_aut := big_sintersection (map s_s'_pair_aut (elem ((state aut) (x) (state aut)))) .

  Lemma buechi_equiv_class_NFA_recognizable: {[V]} =$= L_S buechi_equiv_class_aut.
  Proof.
   unfold buechi_equiv_class_aut. rewrite big_intersection_scorrect.
   intros w. split.
   - intros T a [[s s'] [E T']] % in_map_iff. subst a. apply s_s'_pair_aut_correct.
     unfold eqClass,buechi_eq_class in T. rewrite <-T. rewrite apply_vectorise_inverse.
     repeat destruct decision; auto.
   - intros T. unfold eqClass, buechi_eq_class. apply vector_eq. intros [s s']. rewrite apply_vectorise_inverse.
     assert( s_s'_pair_aut (s, s') el map s_s'_pair_aut (elem (state aut (x) state aut))) as H. { apply in_map_iff. exists (s,s'); auto. }
     specialize (T (s_s'_pair_aut (s,s')) H).
     rewrite (s_s'_pair_aut_correct s s' w) in T.
     destruct (applyVect V (s, s')) as [[|]|].
     + repeat destruct decision; auto; exfalso; eauto using final_transform_implies_transform.
     + destruct T as [T1 T2]. repeat destruct decision; auto; exfalso; eauto using final_transform_implies_transform.
     + repeat destruct decision; auto; exfalso; eauto using final_transform_implies_transform.
  Qed.

  End BuechiEqivalenceClassRecognizable.


NFA recognizing V o W^00
  Definition VW_aut V W := prepend_nfa (buechi_equiv_class_aut (V:=V)) (nfa_omega_iter (buechi_equiv_class_aut (V:=W))).

  Lemma VW_aut_correct V W: L_B (VW_aut V W) =$= {[V]}o{[W]}^00.
  Proof.
    unfold VW_aut.
    now rewrite prepend_nfa_correct, nfa_omega_iter_correct, 2buechi_equiv_class_NFA_recognizable.
  Qed.

Compatibility


  Lemma leq_0 x : 0 <= x.
  Proof. omega. Defined.

  Section Compatibility.
And both strings are pointwise equivalent to some v +++ (w1 ++ w2 ++ ..)
    Variable (v v' : String A).
    Variable (w w' : Seq (String A)).

and the v v' resp wi w'i are from the same ~ equivalence class
    Variables (V W: EqClass).
    Variables (inV: {[V]} v )(inV': {[V]} v').
    Variables (inW: (forall n, {[W]} (w n) ))(inW': (forall n, {[W]} (w' n))).

and r gets partitioned into r0 R according to v w
    Variable (r0 : String (state aut)).
    Variable (R : Seq (String (state aut))).

    Variables (Acc: accepting (r0 +++ concat_inf R) (v +++ (concat_inf w))).

    Variable (eqLengthv: (|r0| = |v|)).
    Variable (valid_r0: (valid_path (seq r0) v)).
    Variable (agree_r0: (r0 [S(|r0|)] = (R 0) [0])).
    Variable (valid_R : (forall k, |R k| = |w k| /\
        valid_path (seq (R k)) (w k))).
    Variable (agree_R: (forall k, (R k)[ S(|R k|)] = (R (S k)) [0])).

Then we can show that there is an accepting run for ow'

    (* predicate that tells whether in R k is a final state, so wether on w k there is a final state *)
    Definition visits_final r := (holdsIn (final_state (aut:=aut)) r).
    Definition W_final := fun k => visits_final (R k).
    Definition pure_W_final := pure W_final.

    Lemma W_final_iff k: W_final k <-> pure_W_final k.
    Proof.
      unfold pure_W_final. apply pure_equiv.
    Qed.

    Instance dec_pure_W_final: forall k, dec (pure_W_final k).
    Proof.
      intros k. apply dec_trans with (P:= W_final k); auto using W_final_iff.
    Qed.

    Lemma v_transforms: (r0 [0]) ===> (R 0) [0] on v .
    Proof.
      exists (seq r0). rewrite <-agree_r0. split; auto.
    Qed.

    Lemma W_transforms k: (R k)[0] ===> (R (S k)) [0] on (w k) /\
            (W_final k -> (R k)[0] =!=> (R (S k)) [0] on (w k)).
    Proof.
      specialize (agree_R k). destruct (valid_R k) as [E P]. split.
      - exists (seq (R k)). split; auto. now rewrite <-E.
      - intros F. exists (seq (R k)). repeat split; auto. now rewrite <-E.
        destruct F as [m [L F]]. exists m. split; oauto.
    Qed.

    Lemma v'_transforms: (r0 [0]) ===> (R 0) [0] on v'.
    Proof.
      eapply (equivalent_in_equivalence_class). apply (equivalent_in_equivalence_class' inV' inV).
      apply v_transforms.
    Qed.

    Lemma W'_transforms k: (R k)[0] ===> (R (S k)) [0] on (w' k) /\
        (pure_W_final k -> (R k)[0] =!=> (R (S k)) [0] on (w' k)).
    Proof.
      split.
      - eapply equivalent_in_equivalence_class. apply (equivalent_in_equivalence_class'(inW' k) (inW k)). apply W_transforms.
      - intros F. rewrite <-W_final_iff in F.
        eapply equivalent_in_equivalence_class. apply (equivalent_in_equivalence_class'(inW' k) (inW k)). now apply W_transforms.
    Qed.

Build the accepting run for ow' Runs for the strings in W'. Need to check whether W is final to ensure that the run for W' is final, too
    Definition R' : Seq (String (state aut)):= fun k => match (dec_pure_W_final k) with
           | left B => match (W'_transforms k ) with
              | conj _ Z => mkstring (projT1 (compute_run_final_transforms (Z B))) (|w' k|) end
           | _ => match (W'_transforms k) with
              | conj Z _ => mkstring (projT1 (compute_run_transforms Z)) (|w' k|) end end.
Run on ow' is obtained from concatting the run on v' to R'
    Definition r' : (Run aut):= (mkstring (projT1 (compute_run_transforms v'_transforms)) (|v'|)) +++ (concat_inf R').

    Ltac destruct_in_R' := destruct dec_pure_W_final; destruct W'_transforms; try (destruct compute_run_final_transforms); try (destruct compute_run_transforms).

    Lemma R'k0_eq_Rk0: forall k, (R' k) [0] = (R k) [0].
    Proof.
      intros k. unfold R'.
      destruct_in_R'; simpl; unfold path in *; tauto.
    Qed.

    Lemma valid_r' : valid_run r' (v' +++ (concat_inf w')).
    Proof.
      unfold r'. apply valid_prepend_path.
        - destruct compute_run_transforms as [x P]. simpl. apply P.
        - destruct compute_run_transforms as [x P].
          unfold concat_inf. simpl. rewrite R'k0_eq_Rk0. symmetry. apply P.
        - unfold R'. apply concat_inf_is_valid'. intros n. repeat split.
          + now destruct_in_R'.
          + destruct_in_R'; unfold path in *; simpl; tauto.
          + assert (forall x y, x (S (| w' n |)) = (R (S n)) [0] -> y 0 = (R (S n)) [0] -> x (S (| w' n |)) = y 0) as T. {
               intros x y E1 E2. now rewrite E1, E2. }
            repeat destruct_in_R'; simpl; unfold path in *; cbn; apply T; tauto.
    Qed.

    Lemma initial_r' : initial r'.
    Proof.
      unfold initial, r'. simpl.
      destruct compute_run_transforms as [x [? [B E]]]. simpl.
      rewrite prepend_string_begin by comega. cbn. rewrite B.
      destruct Acc as [_ [I _]]. cbn in I. unfold initial in I.
      now rewrite prepend_string_begin in I by omega.
    Qed.

In order to prove that r' is final, we prove that infinitely many strings in R' visit a final state. This may switch the next string in R', if the final state in run for (W' k) is the last state, because this is cut off because it is equal to the first in the run of (W' (S k)).
    Lemma string_final_R' k: visits_final (R k) -> visits_final (R' k) \/ visits_final (R' (S k)).
    Proof.
      intros WF. unfold R'. destruct dec_pure_W_final.
      - destruct W'_transforms.
        destruct compute_run_final_transforms as [? [P [n F]]]. simpl.
        decide (n = S (|w' k|)) as [D|D].
        + right. exists 0.
          assert (forall y , y 0 = (R (S k)) [0] -> final_state (y 0 )) as T. {
            intros y E. rewrite E. destruct P as [_ [_ H]]. rewrite <-H, <- D. tauto. }
          destruct_in_R'; simpl; split; try omega; unfold path in *; apply T; tauto.
        + left. exists n. destruct F. split; oauto.
      - exfalso. apply n. now apply W_final_iff.
    Qed.

    Lemma infinite_final_strings_R: infiniteP visits_final R.
    Proof.
      apply concat_inf_infiniteP_inverse.
      rewrite <-(revert_prepend_string r0 (concat_inf R)).
      apply final_drop. apply Acc.
    Qed.

There are infinite final strings in r', so there are infinite final states in r', with infinite combinatorics there is a final state occuring infinitely often
    Lemma final_r' : final r'.
    Proof.
      unfold r'.
      apply final_prepend, concat_inf_infiniteP.
      intros n.
      destruct (infinite_final_strings_R n) as [m [L P]]; destruct (string_final_R' P).
      - now exists m.
      - exists (S m). split; oauto.
    Qed.

So we obtain that r' is accepting
    Lemma accepting_run_for_W': exists r', accepting (aut:=aut) r' (v' +++ (concat_inf w')).
    Proof.
      exists r'. repeat split; auto using valid_r', initial_r', final_r'.
    Qed.

  End Compatibility.

  Theorem compatibility V W w: ({[V]}o{[W]}^00 /$\ L_B aut) w -> ({[V]}o{[W]}^00) <$= L_B aut.
  Proof.
    intros [[v [w' [E [LV [w'' [LW Ew]]]]]][r Acc]].
    rewrite E in Acc. rewrite Ew in Acc. clear E Ew w w'.
    destruct (partition_run_on_prepend_string (proj1 Acc)) as [r0 [R' [P1 [P2 [P3 [P4 P5] ]]]]].
    rewrite <-P1 in Acc. clear P1.
    destruct (partition_run_on_concat_inf P5) as [R [P6 [P7 P8]]].
    rewrite <-P6 in Acc. rewrite <-P6 in P3.

    intros w''' [v' [w' [E' [LV' [W' [LW' Ew']]]]]]. rewrite E', Ew'. clear E' w''' Ew' w'.
    apply accepting_run_for_W' with (v:=v) (w:=w'')(r0 := r0) (R:=R)(V:=V)(W:=W); auto.
  Qed.

  Corollary compatibilityComplement V W w: ({[V]}o{[W]}^00 /$\ (L_B aut)^$~) w -> ({[V]}o{[W]}^00) <$= (L_B aut)^$~.
  Proof.
    intros [IJw Cw] v IJv Bv. apply Cw. now apply (compatibility (V:=V) (W:=W) (w:=v)).
  Qed.

  Corollary compatibility2 V W: {[V]}o{[W]}^00 <$= L_B aut \/ {[V]}o{[W]}^00 <$= (L_B aut)^$~.
  Proof.
    destruct (dec_language_empty_informative (intersect (VW_aut V W) aut) ) as [[w [L1 % VW_aut_correct L2] % intersect_correct]|D].
    - left. now apply (compatibility (w:=w) (V:=V)(W:=W)).
    - right. intros w VW B. apply (D w), intersect_correct. split; auto.
      now apply VW_aut_correct.
  Qed.

Totality


  Section Totality.
    Context (w : Seq A).

Addition of Equivalence Classes

    Definition addEqClass V W: EqClass.
    Proof.
       unfold EqClass.
       apply vectorise. intros [p q].
       decide (exists s, (applyVect V (p,s) = Some true /\ applyVect W (s, q) <> None)\/
                         (applyVect V (p,s) <> None /\ applyVect W (s, q) = Some true)).
       - exact (Some true).
       - decide (exists s, (applyVect V (p,s) = Some false /\ applyVect W(s,q) = Some false)).
         + exact (Some false).
         + exact None.
    Defined.

Proofs with addEqClass get elaborate (and I were happy when the proofs were closed and did not try to hard to simply them

    Ltac destructAll := repeat destruct decision; auto; try tauto; try (now exfalso; try tauto;
          eauto using combine_final_transforms_left, combine_final_transforms_right, combine_transforms, final_transform_implies_transform, split_transforms, split_final_transforms).

    Lemma addEqClass_is_additive v u: addEqClass (buechi_eq_class v) (buechi_eq_class u) = buechi_eq_class (v ++ u).
    Proof.
       assert (None <> Some true) by congruence.
           assert (None <> Some false) by congruence.
           assert (Some false <> Some true) by congruence.
        unfold addEqClass, buechi_eq_class. apply vector_eq. intros [p q]. rewrite !apply_vectorise_inverse.
        destruct decision as [[s P] |D].
        + rewrite !apply_vectorise_inverse in P. destructAll.
        + destruct decision as [[s P] |D'].
          * rewrite !apply_vectorise_inverse in P. destructAll; destruct P as [P1 P2]; try congruence.
            exfalso. apply D. pose proof (split_final_transforms t2) as K. destruct K as [s' [[T1 T2]| [T1 T2]]]; exists s';
              rewrite !apply_vectorise_inverse; destructAll.
          * destruct decision.
            -- exfalso. apply split_transforms in t. apply D'. destruct t as [s' [t1 t2]].
                exists s'. rewrite !apply_vectorise_inverse. destructAll;
                exfalso; apply D; exists s'; rewrite !apply_vectorise_inverse; destructAll.
            -- auto.
    Qed.

    Lemma addEqClass_is_associative : associative addEqClass.
    Proof.
      (* Better do not look at this *)
      intros U V W.
      assert (None <> Some true) by congruence. assert (Some true <> None) by congruence.
      assert (None <> Some false) by congruence.
      assert (Some false <> Some true) by congruence.
      unfold addEqClass. apply vector_eq. intros [p q]. rewrite !apply_vectorise_inverse. destruct decision as [[s [P|P] ] |N].
      - rewrite !apply_vectorise_inverse in *. destruct decision as [[s2 [P2|P2]] | N2].
        + rewrite decision_true. reflexivity.
          exists s2. rewrite apply_vectorise_inverse.
          rewrite decision_true. tauto. exists s. left. split. tauto. destruct P2. congruence.
        + rewrite decision_true. reflexivity.
          exists s2. rewrite apply_vectorise_inverse.
          rewrite decision_true. tauto. exists s. tauto.
        + rewrite decision_true. reflexivity.
          destruct decision as [[s2 P2]|N3] in P.
          * exists s2. rewrite apply_vectorise_inverse.
            rewrite decision_true. left. split; auto. destruct P2. congruence.
            exists s. left. destruct P2, P. split; congruence.
          * exfalso. now apply P.
      - rewrite apply_vectorise_inverse in P. destruct decision as [[s2 [P2|P2]]|N2] in P.
        + rewrite decision_true. reflexivity.
          exists s2. rewrite apply_vectorise_inverse.
          rewrite decision_true. tauto. exists s. tauto.
        + rewrite decision_true. reflexivity.
          exists s2. rewrite apply_vectorise_inverse.
          destruct decision as [[s3[P3|P3]]|N3]; try tauto.
          right. rewrite decision_true. split; try tauto. congruence.
          exists s. split.
          * destruct (applyVect U (p , s)) as [[|]|] eqn:K; auto; exfalso.
            -- apply N3. exists s. tauto.
            -- now apply P.
          * destruct (applyVect V (s, s2))as [[|]|] eqn:K; auto; exfalso.
            -- apply N3. exists s. tauto.
            -- now apply P2.
        + exfalso. destruct decision in P; destruct P; congruence.
      - destruct decision as [[s P] | N2].
        + rewrite apply_vectorise_inverse in P. destruct decision as [[s2 P2] |N3] in P.
          * exfalso. destruct P. congruence.
          * destruct decision as [[s2 P2]|N4] in P.
            -- rewrite decision_false.
               ++ rewrite decision_true. reflexivity.
                  exists s2. split; try tauto. rewrite apply_vectorise_inverse.
                  rewrite decision_false. rewrite decision_true. tauto.
                  exists s. tauto.
                  intros [s3 [P3|P3]]; apply N; exists s3.
                  ** left. split; try tauto. rewrite apply_vectorise_inverse.
                     destruct decision as [[s4 P4] | N4].
                     --- congruence.
                     --- rewrite decision_true; auto.
                         exists s2. split; try tauto.
                         destruct (applyVect V (s3,s2)) as [[|]|] eqn:K; auto.
                         +++ exfalso. apply N4. exists s2. left. split; try tauto. destruct P2. congruence.
                         +++ destruct P3. congruence.
                  ** right. split; try tauto. rewrite apply_vectorise_inverse.
                     rewrite decision_true; auto.
                     exists s2. left. destruct P2,P3. split; congruence.
               ++ intros [s3 [P3|P3]]; apply N; rewrite apply_vectorise_inverse in P3; destruct decision as [[s4 [P4|P4]]|N4] in P3.
                  ** exists s4. left. split; try tauto.
                     rewrite apply_vectorise_inverse.
                     destruct decision as [[s5 P5]|N5]; auto.
                     rewrite decision_true; auto. exists s3.
                     destruct (applyVect V (s4, s3)) as [[|]|] eqn:K1; destruct (applyVect W (s3,q)) as [[|]|] eqn:K3; auto; exfalso;
                     try ( apply N5; exists s3; left; split; auto; now rewrite K3);
                     try (apply N5; exists s3; right; split; auto; now rewrite K1).
                     destruct P3; congruence. destruct P4; congruence. destruct P4; congruence.
                  ** exists s4. right. split; try tauto.
                     rewrite apply_vectorise_inverse. rewrite decision_true; auto.
                     exists s3. now left.
                  ** exfalso. destruct decision in P3; destruct P3; congruence.
                  ** exists s4. left. split; try tauto.
                     rewrite apply_vectorise_inverse.
                     destruct decision as [[s5 P5]|N5]; auto.
                     rewrite decision_true; auto. exists s3.
                     destruct (applyVect V (s4, s3)) as [[|]|] eqn:K1; destruct (applyVect W (s3,q)) as [[|]|] eqn:K3; auto; exfalso;
                     try ( apply N5; exists s3; left; split; auto; now rewrite K3);
                     try (apply N5; exists s3; right; split; auto; now rewrite K1).
                     destruct P3; congruence. destruct P4; congruence. destruct P4; congruence.
                  ** exists s4. right. split; try tauto.
                      rewrite apply_vectorise_inverse. rewrite decision_true; auto.
                     exists s3. left; split; try tauto. destruct P3. congruence.
                  ** destruct decision as [[s5 [P51 P52]] | N5] in P3.
                     --- exists s5. right. split; try congruence.
                         rewrite apply_vectorise_inverse. rewrite decision_true; auto.
                         exists s3. right. split; try congruence. apply P3.
                     --- exfalso. now apply P3.
            -- exfalso. destruct P. congruence.
        + rewrite decision_false.
          -- rewrite decision_false; auto.
             intros [s2 P2]. rewrite apply_vectorise_inverse in P2.
             destruct decision in P2. exfalso. destruct P2. congruence.
             destruct decision in P2. {
              apply N2. destruct e as [s P3].
               exists s. split; try tauto. rewrite apply_vectorise_inverse.
               destruct decision as [[s4 P4]|N4].
               ** exfalso. apply N.
                  exists s. right. split. destruct P3. congruence.
                  rewrite apply_vectorise_inverse. rewrite decision_true; auto.
                  exists s4. tauto.
               ** rewrite decision_true; auto.
                  exists s2. tauto.
             }
             exfalso. destruct P2. congruence.
          -- intros [s P]. rewrite apply_vectorise_inverse in P. destruct P as [P|P].
             ++ destruct decision as [[s2 [P2|P2]]|N3]; auto.
                ** apply N. exists s2. left. split; try tauto.
                   rewrite apply_vectorise_inverse. destruct decision as [P5|N5]; try congruence.
                   destruct decision as [[s3 P3] | N4]; try congruence.
                   exfalso. destruct (applyVect V (s2, s)) as [[|]|] eqn:EV.
                   --- apply N5. exists s. tauto.
                   --- destruct (applyVect W (s,q)) as [[|]|] eqn:EW.
                       +++ apply N5. exists s. right. split; try congruence. auto.
                       +++ apply N4. exists s. tauto.
                       +++ exfalso. destruct P. congruence.
                   --- exfalso. destruct P2. congruence.
                ** apply N. exists s2. right. split; try tauto.
                   rewrite apply_vectorise_inverse. destruct decision as [P5|N5]; try congruence.
                   exfalso. apply N5. exists s. tauto.
                ** destruct decision in P; destruct P; congruence.
             ++ destruct decision as [[s2 [P2 |P2] ]|N3].
                ** apply N. exists s2. left. split; try tauto.
                   rewrite apply_vectorise_inverse.
                   rewrite decision_true; try congruence.
                   exists s. tauto.
                ** apply N. exists s2. right. split; try tauto.
                   rewrite apply_vectorise_inverse.
                   rewrite decision_true; try congruence.
                   exists s. left. destruct P2 as [_ P2]. rewrite P2. destruct P as [_ P]. rewrite P. split; congruence.
                ** destruct decision as [[s2 [P2 P3]]|N4] in P.
                   --- apply N. exists s2. right. split; try congruence.
                       rewrite apply_vectorise_inverse. rewrite decision_true; auto.
                       exists s. right. destruct P. split; congruence.
                   --- destruct P. congruence.
     Qed.

Totality using Additive Ramsey for the finite semigroup of the equivalence classes
    Lemma ramseyTotality: AdditiveRamsey (mkSG addEqClass_is_associative) -> (exists V W, ({[V]}o{[W]}^00) w).
    Proof.
      intros R.
      destruct (R (fun n m => buechi_eq_class (extract n m w))) as [g [Inc P]].
      - intros i j k L.
        rewrite <-concat_extract with (i_1:=i)(i_2:=j)(i_3:=k); oauto.
        apply addEqClass_is_additive.
      - exists (buechi_eq_class (mkstring w (pred (g 1)) )),(buechi_eq_class (extract (g 0)(g 1) w)).
        apply split_position_lang_prepend. exists (pred (g 1)). split.
        + apply buechi_eq_class_correct.
        + apply lang_o_iter_extract. exists (seq_map (fun n => n - (g 1)) (drop 1 g)). repeat split; unfold seq_map.
          * simpl. intros n. pose (Inc (S n)). destruct n.
            -- omega.
            -- enough (g 1 < g (S (S n)) /\ g 1 < g (S (S (S n)))) by omega.
               split; apply s_monotone_strict_order_preserving; oauto.
          * simpl. omega.
          * intros n.
            pose (Inc 0). rewrite_eq (S (pred (g 1)) = g 1).
            rewrite extract_from_drop'.
            -- repeat rewrite drop_correct.
               rewrite (P (1 + n) (1 + S n)) by omega.
               apply buechi_eq_class_correct.
            -- repeat rewrite drop_correct.
               apply s_monotone_order_preserving; oauto.
    Qed.
  End Totality.

End BuechiEquivalenceRelation.

Definition of Complement NFA

Section Complement.

  Variable (A: finType).
  Variable (aut: NFA A).

NFAs recognizing all V o W^00
    Notation EqClassPair := ((EqClass (aut:=aut)) (x) (EqClass (aut:=aut))).

V o W^00 is part of the complement if its intersection with the Buechi language is empty
    Definition VW_part_of_complement (vw : EqClassPair) := L_B (intersect (VW_aut (fst vw) (snd vw)) aut) =$= {}.

    Instance dec_VW_part_of_complement vw: dec (VW_part_of_complement vw).
    Proof.
     unfold VW_part_of_complement.
     apply dec_language_empty.
    Qed.

    Definition complement_auts := map (fun vw => VW_aut (fst vw) (snd vw)) (filter (DecPred VW_part_of_complement ) (elem EqClassPair)).

The complement NFA is the union of all these automata
    Definition complement := big_union complement_auts.
End Complement.