Set Implicit Arguments.
Require Import Coq.Init.Nat.
Require Import BasicDefs.
Require Import FinType.
Require Import Seqs.
Require Import NFAs.
Require Import RegularLanguages.

Open Scope string_scope.

Büchi Automata

Büchi Acceptance

Section BuechiAutomaton.

  Context {X:finType}.
  Variable (aut: NFA X).
  Implicit Types (r: Run aut) (w: Seq X).

  Definition initial r := initial_state (r 0).
  Definition final r := infiniteP (final_state (aut:=aut)) r.
  Definition accepting r w := (valid_run r w) /\ (initial r) /\ (final r).
  Definition buechi_language : SeqLang X := fun w => exists r, accepting r w.

  Lemma accepting_extensional r r' w w' : r === r' -> w === w' -> accepting r w -> accepting r' w'.
  Proof.
    intros Er Ew [V [In Fin]]. repeat split.
    - now rewrite <-Er, <- Ew.
    - red. now rewrite <-Er.
    - now rewrite <-Er.
  Qed.

  Global Instance accepting_proper: Proper (@seq_equal (state aut) ==> @seq_equal X ==> iff) accepting.
  Proof.
    intros r r' Er w w' Ew. split; apply accepting_extensional; auto.
  Qed.

  Global Instance buechi_language_proper : Proper (@seq_equal X ==> iff) buechi_language.
  Proof.
    intros w w' E; split; intros [r A]; exists r. now rewrite <-E. now rewrite E.
  Qed.

  Lemma final_drop r n : final r -> final (drop n r).
  Proof. now apply drop_preserves_infiniteP. Qed.

  Lemma final_prepend (r' : String (state aut)) r : final r -> final (r' +++ r).
  Proof. now apply finite_prefix_preserves_infiniteP. Qed.

  Lemma omega_iteration_final (r: String (state aut)) k: k <= |r| -> final_state (r [k]) -> final (r to_omega).
  Proof. intros L F. apply omega_iteration_infiniteP. firstorder. Qed.

  Lemma final_iff_step r: (exists n, final_state (r n)) -> (forall n, final_state (r n) -> exists m, n < m /\ final_state (r m)) -> final r.
  Proof.
    intros B S n. induction n.
    - destruct B as [n F]. exists n; split; oauto.
    - destruct IHn as [m [G F]].
      destruct (S m F) as [m' [G' F']].
      exists m'. split; oauto.
  Qed.

End BuechiAutomaton.

Notation "'L_B'" := buechi_language.

Empty and Universal Büchi Automataon
Section EmptyBuechiAutomaton.

  Context {X:finType}.

  Definition empty_aut := mknfa (fun (s : finType_False)(x:X) (s':finType_False) => False) (fun _ => False) (fun _ => False).

  Lemma empty_aut_correct: L_B empty_aut =$= {}.
  Proof.
   apply language_empty_iff. intros w [r [? [I ?]]].
   unfold initial in I. now cbn in I.
  Qed.

  Lemma seq_in_empty_aut_contradicts w: L_B empty_aut w -> False.
  Proof. apply (empty_aut_correct w). Qed.

End EmptyBuechiAutomaton.

Section UniversalBuechiAutomaton.

  Context {X:finType}.

  Lemma univ_aut_correct: L_B (univ_aut (X:=X)) =$= universal_language.
  Proof.
    intros w. split; firstorder.
    exists (fun n => tt); repeat split.
    intros n. exists n; oauto.
  Qed.

End UniversalBuechiAutomaton.

Decidability of Language Emptiness


Section DecBuechiAutomatonEmpty.

  Context {X: finType}.
  Variable (aut: NFA X).

  Implicit Types (w: Seq X) (s: state aut).

  Definition final_loop_exists := exists (s_i s_f: state aut), initial_state s_i /\ final_state s_f /\ reachable s_i s_f /\ reachable s_f s_f.

  Lemma seq_implies_final_loop : (exists w, L_B aut w) -> final_loop_exists.
  Proof.
    intros [w [r [V [I F]]]]. exists (r 0).
    pose (r_f := infinite_filter F).
    destruct (can_find_duplicate' 1 (S(S (Cardinality (state aut)))) (seq_map r r_f)) as [[i [j [L [_ E]]]]|D].
    - exists (r (r_f i)). repeat split; auto.
      + subst r_f. apply infinite_filter_correct.
      + exists r, (mkstring w (pred (r_f i))). repeat split.
        * now apply valid_run_is_path_from_begin.
        * cbn. f_equal. enough (r_f i > 0) by omega.
           subst r_f. enough (1 <= i); try omega.
           apply s_monotone_ge_zero'; auto. apply infinite_filter_s_monotone.
      + exists (drop (r_f i) r), (extract (r_f i) (r_f j) w). repeat split.
        * now apply valid_run_is_path_everywhere.
        * rewrite drop_correct. f_equal. omega.
        * unfold seq_map in E. rewrite E.
           rewrite drop_correct. cbn. f_equal.
           enough (r_f j > (r_f i)) by omega.
           apply s_monotone_strict_order_preserving; oauto.
           apply infinite_filter_s_monotone.
    - exfalso. omega.
  Qed.

  Lemma final_loop_implies_up_seq : final_loop_exists -> (exists u v, L_B aut (u +++ v to_omega)).
  Proof.
    intros [s_i [s_f [I [F [[r_i [u [Vi [Bi Ei]]]] [r_f [v Pf]]]]]]].
    exists u, v, ((mkstring r_i (|u|)) +++ (mkstring r_f (|v|)) to_omega). repeat split.
    - apply valid_prepend_path; auto.
      + cbn. destruct Pf as [_ [Bf _]]. now rewrite Bf, <-Ei.
      + now apply cycle_omega_is_valid_run with (s:=s_f).
    - unfold initial. rewrite prepend_string_begin by omega.
      cbn. now rewrite Bi.
    - apply final_prepend. apply omega_iteration_final with (k := 0). omega.
      cbn. destruct Pf as [_ [Bf _]]. now rewrite Bf.
  Qed.

  Theorem dec_language_empty_informative_periodic : {exists u v, L_B aut (u +++ v to_omega)} + {L_B aut =$= {}}.
  Proof.
    decide (final_loop_exists) as [D|D].
    - left. now apply final_loop_implies_up_seq.
    - right. intros w. split.
      + intros M. apply D, seq_implies_final_loop. now exists w.
      + intros M. exfalso. apply M.
  Qed.

  Corollary dec_language_empty_informative : {exists w, L_B aut w} + {L_B aut =$= {}}.
  Proof.
    destruct (dec_language_empty_informative_periodic) as [D|D].
    - left. destruct D as [v [w L]]. now exists (v +++ w to_omega).
    - now right.
  Qed.

  Corollary dec_language_empty: dec(L_B aut =$= {}).
  Proof.
    destruct dec_language_empty_informative as [D|D].
    - right. intros E. destruct D as [w Lw]. now apply (E w).
    - now left.
  Qed.

End DecBuechiAutomatonEmpty.

Closure under Image and Preimage

Section ImageNFA.

  Context {X Y : finType}.
  Variable (f : X -> Y).


  Variable (aut: NFA X).

  Definition image_transition (s: state aut) (y: Y) (s': state aut) := exists x, f x = y /\ transition (aut:=aut) s x s'.

  Definition image_aut := mknfa image_transition (initial_state (aut:=aut)) (final_state (aut:=aut)).

  Lemma aut_accepts_image: L_B image_aut <$= Image f (L_B aut) .
  Proof.
    intros w' [r [V [I F]]].
    assert (forall n, { x | f x = w' n /\ transition (aut:=aut) (r n) x (r (S n))}) as W. {
       intros n . apply finType_cc; auto. now specialize (V n). }
    exists (fun n => proj1_sig (W n)). split.
    - intros n. unfold seq_map. now destruct (W n) as [x [P Q]].
    - exists r. repeat split; auto.
      intros n. now destruct (W n).
  Qed.

  Lemma image_accepts_aut: Image f (L_B aut) <$= L_B image_aut.
  Proof.
    intros w [w' [E [r [V [I F]]]]].
    exists r. repeat split; auto. rewrite <-E.
    intros n. cbn. now exists (w' n).
  Qed.

  Lemma image_aut_correct : L_B image_aut =$= Image f (L_B aut).
  Proof.
    intros w. split; auto using aut_accepts_image, image_accepts_aut.
  Qed.

End ImageNFA.

Section PreImageNFA.

  Context {X Y:finType}.
  Variable (f: X -> Y).
  Variable (aut: NFA Y).
  Implicit Types (p q : state aut).

  Definition preimage_aut := mknfa (fun p a q => transition p (f a) q) (initial_state (aut:=aut)) (final_state (aut:=aut)).

  Lemma preimage_aut_correct : L_B preimage_aut =$= PreImage f (L_B aut).
  Proof.
    intros w. split; intros [r [V [In Fin]]]; exists r; repeat split; auto.
  Qed.
End PreImageNFA.

Closure under Union

Section UnionClosure.

  Context {X : finType}.

  Section Def.

  Variables (aut_1 aut_2 : NFA X).

  Definition union_state : finType := (state aut_1) (+) (state aut_2).
  Definition union_transition (s1:union_state) (x:X) (s2:union_state) := match s1,s2 with
            | (inl s1), (inl s2) => transition s1 x s2
            | (inr s1), (inr s2) => transition s1 x s2
            | _ , _ => False
           end.
  Definition union_initial (s:union_state) := match s with
            | inl s => initial_state s
            | inr s => initial_state s
           end.
  Definition union_final (s : union_state) :=match s with
            | inl s => final_state s
            | inr s => final_state s
           end.
  Instance dec_union_transition: forall s1 x s2, dec(union_transition s1 x s2).
  Proof.
   intros s1 x s2. destruct s1,s2; simpl; auto.
  Qed.

  Instance dec_union_initial: forall s, dec(union_initial s).
  Proof.
    intros s. destruct s; auto.
  Qed.

  Instance dec_union_final: forall s, dec(union_final s).
  Proof.
    intros s. destruct s; simpl; auto.
  Qed.

  Definition union:= mknfa union_transition union_initial union_final.

  Implicit Types (w: Seq X) (r: Run union).

Because states from aut1 can only go the states of aut1
  Lemma states_do_not_mix r w : valid_run r w -> (exists s, (r 0) = inl s) ->
          (forall n, exists s, r n = inl s).
  Proof.
    intros V [s L] .
    induction n.
    - firstorder.
    - specialize (V n). destruct (r ( S n)) as [s2 |s2].
      + now exists s2.
      + exfalso. destruct IHn as [s1 E]. now rewrite E in V.
  Qed.

Given an accepting run of the union aut, the first state of the run decides whether the sequence is accepted by aut1 or aut2
  Lemma autU_accepted_by_aut1 r w:
       accepting r w -> (exists s, (r 0) = inl s) -> (L_B aut_1 w).
  Proof.
    intros [V [I Fin]] B.
    assert (forall n, exists s, r n = inl s) as M by now apply (states_do_not_mix V).
    destruct B as [s B].
    exists (seq_map (fun s' => match s' with
            | inl s' => s'
            | inr _ => s
            end) r ). repeat split; unfold seq_map.
    - intros n. specialize (V n).
      destruct (M n) as [s1 E1]. destruct (M (S n)) as [s2 E2]. now rewrite E1, E2 in *.
    - red. red in I. destruct (M 0) as [s0 E0]. now rewrite E0 in *.
    - intros n. destruct (Fin n) as [m [P Q]].
      exists m. split; auto.
      destruct (M m) as [sm Em]. now rewrite Em in *.
  Qed.

  Lemma aut1_incl_autU: L_B aut_1 <$= L_B union.
  Proof.
    intros w [r [V [I Fin]]].
    exists (fun n => inl (r n)). repeat split; auto.
  Qed.

  End Def.

  Definition swap_sum (X Y: Type) (v: X + Y) := match v with | inl l => inr l | inr r => inl r end.
  Arguments swap_sum {X} {Y} _.

  Lemma union_symmetric_acc (aut_1 aut_2: NFA X) r w: accepting (aut:=union aut_1 aut_2) r w -> accepting (aut:= union aut_2 aut_1) (seq_map swap_sum r) w.
  Proof.
    intros [V [I F]]. repeat split; unfold seq_map.
    - intros n. specialize (V n). now destruct (r n); destruct (r (S n)).
    - unfold initial in *. now destruct (r 0).
    - intros n. destruct (F n) as [m [P Q]]. exists m. split; auto. now destruct (r m).
  Qed.

  Lemma union_symmetric (aut_1 aut_2 : NFA X) : L_B (union aut_1 aut_2) =$= L_B (union aut_2 aut_1).
  Proof.
    intros w. split; intros [r Acc]; exists (seq_map swap_sum r); now apply union_symmetric_acc.
  Qed.

  Lemma union_correct (aut_1 aut_2 : NFA X) : L_B (union aut_1 aut_2) =$= L_B aut_1 \$/ L_B aut_2.
  Proof.
    intros w. split.
    - intros L. destruct L as [r Acc] . destruct (r 0) eqn:H.
      + left. apply autU_accepted_by_aut1 with (r:=r); firstorder.
      + right. apply union_symmetric_acc in Acc.
        eapply autU_accepted_by_aut1. apply Acc. exists e. unfold seq_map. now rewrite H.
    - intros [L1 | L2].
      + now apply aut1_incl_autU.
      + apply union_symmetric. now apply aut1_incl_autU.
  Qed.

End UnionClosure.

Closure under Intersection

Section IntersectionClosure.

  Context (X:finType).

  Variables (aut_1 aut_2 : NFA X).

  Definition intersection_state := state aut_1 (x) state aut_2 (x) finType_bool.

  Implicit Types (x:X)(s: intersection_state)(w:Seq X).

  Definition intersection_initial s := match s with
     | (s_1, s_2, _) => initial_state s_1 /\ initial_state s_2
  end.

  Definition intersection_final s := match s with
    | (_, s_2 , true) => final_state s_2
    | _ => False
  end.

  Definition intersection_transition s x s' := match s,s' with
     | (s_1, s_2, true), (s_1',s_2',b) =>
             (transition s_1 x s_1') /\ (transition s_2 x s_2') /\
             (b = false <-> final_state s_2)
     | (s_1, s_2, false), (s_1',s_2',b) =>
             (transition s_1 x s_1') /\ (transition s_2 x s_2') /\
             (b = true <-> final_state s_1)
  end.

  Instance dec_intersection_initial s : dec(intersection_initial s).
  Proof. destruct s as [[? ?] ?]; auto. Qed.
  Instance dec_intersection_final s : dec (intersection_final s).
  Proof. destruct s as [[? ?] [|]]; auto. Qed.
  Instance dec_intersection_transition s x s': dec(intersection_transition s x s').
  Proof. destruct s as [[? ?] [|]]; destruct s' as [[? ?] [|]]; auto. Qed.

  Definition intersect := mknfa intersection_transition intersection_initial intersection_final.

  Lemma between_final_state_intersect_is_final_state_aut_1 (r: Run intersect) w n m: valid_run r w -> final_state (r n) -> final_state (r m) -> n < m -> exists k, n <= k <= m /\ final_state (fst (fst (r k))).
  Proof.
    intros V Fn Fm L. decide (exists k , k <= m /\ n <= k /\ final_state (fst (fst (r k)))) as [[k [L1 [L2 F]]] | D].
    - exists k. tauto.
    - exfalso. enough (forall i, n < i <= m -> (snd (r ( i))) = false) as H.
      + enough (snd (r m) = true) as H'.
        * now rewrite (H ( m)) in H' by omega.
        * destruct (r m) as [[? ?][|]]; cbn in *; auto.
      + intros i [L' L'']. clear L. induction L' as [| i].
        * specialize (V n). destruct (r n) as [[? ?] [|]] eqn:E; destruct (r (S n)) as [[? ?] [|]] eqn:E'; cbn in *; try tauto.
        * specialize (V i). destruct (r i) as [[? ?] [|]] eqn:E; destruct (r (S i)) as [[? ?] [|]] eqn:E'; cbn in *; try tauto.
          -- apply IHL'. omega.
          -- exfalso. apply D. exists i. rewrite E. cbn in *. repeat split; oauto. now apply V.
  Qed.

  Lemma intersect_incl_aut1: L_B intersect <$= L_B aut_1.
  Proof.
    intros w [r [V [I F]]]. exists (seq_map (fun v => fst (fst v)) r). unfold seq_map. repeat split.
    - intros n. specialize (V n). destruct (r n) as [[? ?] [|]]; destruct (r (S n)) as [[? ?][|]]; cbn in *; tauto.
    - unfold initial in *. destruct (r 0) as [[? ?] [|]]; cbn in *; tauto.
    - intros n.
      pose (Fn := F n). destruct Fn as [m1 [L1 F1]].
      pose (Fm := F (S m1)). destruct Fm as [m2 [L2 F2]].
      destruct (between_final_state_intersect_is_final_state_aut_1 V (n := m1) (m := m2)) as [k [L Fk]]; oauto.
      exists k. split; oauto.
  Qed.

  Lemma intersect_incl_aut2: L_B intersect <$= L_B aut_2.
  Proof.
    intros w [r [V [I F]]]. exists (seq_map (fun v => snd (fst v)) r). unfold seq_map. repeat split.
    - intros n. specialize (V n). destruct (r n) as [[? ?] [|]]; destruct (r (S n)) as [[? ?][|]]; cbn in *; tauto.
    - unfold initial in *. destruct (r 0) as [[? ?] [|]]; cbn in *; tauto.
    - intros n. destruct (F n) as [m [L F']].
      exists m. split; auto. destruct (r m) as [[q1 q2] [|]]; cbn in *; auto. now exfalso.
  Qed.


  Fixpoint irun (r_1:Run aut_1) (r_2: Run aut_2) n: (state intersect) := match n with
     | 0 => ((r_1 0),(r_2 0), false)
     | S n => match (irun r_1 r_2 n) with
           | (_,_,true) => (r_1 (S n), r_2 (S n), if (decision (final_state (r_2 n))) then false else true)
           | (_,_,false) => (r_1 (S n), r_2 (S n), if (decision (final_state (r_1 n))) then true else false)
             end end.

  Section IRun.

    Variables (w: Seq X)(r_1 : Run aut_1) (r_2: Run aut_2).

    Lemma irun_valid: valid_run r_1 w -> valid_run r_2 w -> valid_run (irun r_1 r_2) w .
    Proof.
      intros V1 V2 n. induction n.
      - specialize (V1 0). specialize (V2 0). cbn in *. repeat split; auto; destruct decision; congruence.
      - specialize (V1 (S n)). specialize (V2 (S n)). cbn in *. destruct (irun r_1 r_2 n)as [[? ?][|]]; cbn in *;
        destruct decision; destruct decision; auto; repeat split; congruence.
    Qed.

    Lemma irun_initial: initial r_1 -> initial r_2 -> initial (irun r_1 r_2).
    Proof.
      intros I1 I2. unfold initial in *. cbn. tauto.
    Qed.


    Variables (F1: final r_1) (F2: final r_2).

    Lemma irun_step_to_true n : snd(irun r_1 r_2 n) = false -> exists m, m > n /\ snd (irun r_1 r_2 m) = true.
    Proof.
      intros F. exists (S (next_position_exists (F1 n))). split.
      - pose (next_position_exists_increasing (F1 n)). omega.
      - enough (forall k, n <= k <= (next_position_exists (F1 n)) -> snd (irun r_1 r_2 k) = false) as H.
        + destruct (irun r_1 r_2 (next_position_exists (F1 n))) as [[? ?][|]] eqn:E.
          * exfalso. specialize (H (next_position_exists (F1 n))).
            rewrite E in H. cbn in H. enough (true = false) by congruence. apply H.
            pose (next_position_exists_increasing (F1 n)). omega.
          * cbn. rewrite E. destruct decision as [D|D]; cbn; auto.
            exfalso. apply D. apply next_position_exists_correct.
        + intros k. intros [L1 L2]. induction L1; auto.
          cbn in *. destruct (irun r_1 r_2 m) as [[? ?][|]] eqn :H.
          * exfalso. cbn in IHL1. enough (true =false ) by congruence. apply IHL1. omega.
          * destruct decision as [D|D]; auto.
            exfalso. apply (next_position_exists_all (L:= F1 n) (k:=m)); oauto.
    Qed.

    Lemma irun_same_states n : fst (irun r_1 r_2 n) = (r_1 n, r_2 n).
    Proof.
      induction n; auto. cbn.
      destruct (irun r_1 r_2 n) as [[? ?] [|]]; auto.
    Qed.

    Lemma irun_step_final n : snd(irun r_1 r_2 n) = true -> exists m, m >= n /\ final_state (irun r_1 r_2 m).
    Proof.
      intros F. exists (next_position_exists (F2 n)). split.
      - pose (next_position_exists_increasing (F2 n)). omega.
      - enough (forall k, n <= k <= (next_position_exists (F2 n)) -> snd (irun r_1 r_2 k) = true) as H.
        + destruct (irun r_1 r_2 (next_position_exists (F2 n))) as [[? s2][|]] eqn:E.
          * cbn. enough (s2 = r_2 (next_position_exists (F2 n))) as -> by apply next_position_exists_correct.
            pose (H' := irun_same_states (next_position_exists (F2 n))). rewrite E in H'. cbn in H'. congruence.
          * exfalso. specialize (H (next_position_exists (F2 n))). rewrite E in H. cbn in H.
            enough (false = true) by congruence. apply H. pose (next_position_exists_increasing (F2 n)). omega.
        + intros k [L1 L2]. induction L1; auto.
          cbn in *. destruct (irun r_1 r_2 m) as [[? ?][|]] eqn :H.
          * destruct decision as [D|D]; auto.
             exfalso. apply (next_position_exists_all (L:= F2 n) (k:=m)); oauto.
          * exfalso. cbn in IHL1. enough (false = true) by congruence. apply IHL1. omega.
    Qed.

    Lemma irun_final: final (irun r_1 r_2).
    Proof.
      intros n. destruct (snd (irun r_1 r_2 n)) eqn:H.
      - now apply irun_step_final.
      - apply irun_step_to_true in H. destruct H as [n' [G T]].
        apply irun_step_final in T. destruct T as [m [G' F]].
        exists m. split; oauto.
    Qed.
  End IRun.

  Lemma intersection_incl_intersect : L_B aut_1 /$\ L_B aut_2 <$= L_B intersect.
  Proof.
    intros w [[r_1 [V1 [I1 F1]]] [r_2 [V2 [I2 F2]]]].
    exists (irun r_1 r_2). split; [|split].
    - now apply irun_valid.
    - now apply irun_initial.
    - now apply irun_final.
  Qed.

  Lemma intersect_correct: L_B intersect =$= L_B aut_1 /$\ L_B aut_2.
  Proof.
    intros w. split.
    - intros A. split; [now apply intersect_incl_aut1 | now apply intersect_incl_aut2].
    - apply intersection_incl_intersect.
  Qed.
End IntersectionClosure.

Union and Intersection of Finitely Many NFAs

Definition big_union (A:finType) (l:list (NFA A)) := fold_right union empty_aut l.

Lemma big_union_correct (A:finType) (l:list (NFA A)):
             L_B (big_union l) =$= fun w => exists a, (a el l) /\ L_B a w.
Proof.
split.
- intros U. induction l; cbn in U.
  + exfalso. now apply empty_aut_correct in U.
  + apply union_correct in U. destruct U as [U|U].
    * now exists a.
    * destruct (IHl U) as [a' [H1 H2]].
      exists a'; split; auto.
- intros [b [I L]]. induction l.
  + contradiction I.
  + cbn. apply union_correct.
    destruct I as [I |I].
    * left. now rewrite I.
    * right. now apply IHl.
Qed.

Definition big_intersection (A:finType) (l:list (NFA A)) := fold_right (intersect (X:=A)) univ_aut l.
Lemma big_intersection_correct (A:finType) (l:list (NFA A)):
            L_B (big_intersection l) =$= fun w => forall a, (a el l) -> L_B a w.
Proof.
  intros w. split.
  - intros I a L. induction l.
    + now exfalso.
    + cbn in I. apply intersect_correct in I. destruct I as [I1 I2].
      destruct L.
      * now subst a.
      * now apply IHl.
  - intros I. induction l.
    + cbn. now apply univ_aut_correct.
    + cbn. apply intersect_correct. split.
      * now apply I.
      * apply IHl. auto.
Qed.

ω-Iteration of a Regular Language

Section NFAOmegaIteration.
  Context {X:finType}.

  Section OmegaIterNormalized.

  Variable (aut: NFA X).

  Variables (initialW finalW : state aut).

  Variable (normW: sautomaton_normalized initialW finalW).

  Definition oiter_transition s a s' := (s' <> initialW /\ transition s a s') \/ (s' = initialW /\ transition s a finalW).

  Definition nfa_omega_iter' := mknfa oiter_transition (fun s => s = initialW) (fun s => s = initialW).

  Lemma nfa_omega_iter'_accepts_aut: (L_S aut)^00 <$= L_B nfa_omega_iter'.
  Proof.
    intros w W.
    destruct W as [ws [W C]].
    pose (R:= fun (n:nat) => mkstring ( fun k =>(proj1_sig (nfa_string_lang_cc (W n))) k) (|ws n|) : String (state nfa_omega_iter')).
    exists (concat_inf R).
    repeat split.
    - rewrite C. apply concat_inf_is_valid. repeat split.
      + intros k L. left. unfold R. destruct (nfa_string_lang_cc (W n)) as [r [Vn [In Fn]]]. cbn. split.
        * specialize (Vn k L). decide (r (S k) = initialW) as [D|D]; auto.
          exfalso. rewrite D in Vn. now apply normW in Vn.
        * now apply Vn.
      + right. unfold R. destruct (nfa_string_lang_cc (W n)) as [r [V [I F]]]; destruct (nfa_string_lang_cc (W (S n))) as [r' [V' [I' F']]]. cbn. split.
        * now apply normW in I'.
        * apply normW in F. rewrite <-F. now apply V.
    - cbn. destruct (nfa_string_lang_cc (W 0)) as [r [V [I F]]]. cbn.
      apply normW in I. now rewrite I.
    - intros n. exists (begin_in R n). split.
      + apply s_monotone_ge, s_monotone_begin_in.
      + unfold concat_inf. rewrite concat_inf_index_begin. cbn.
        destruct (nfa_string_lang_cc (W n)) as [r [V [I F]]]. cbn.
        now apply normW in I.
  Qed.

  Lemma initialW_partitions_in_W r w n m: accepting (aut:=nfa_omega_iter') r w
               -> n < m -> r n = initialW -> r m = initialW
               -> (forall k, n < k < m -> r k <> initialW )
                    -> (L_S aut) (extract n m w).
  Proof.
    intros [V [I F]] L nW mW kNW.
    exists ((extract n m r) +++ (fun _ => finalW)).
    repeat split.
    - intros k B. simpl.
      decide (k < m - S n).
      + rewrite 2prepend_string_begin by comega. cbn.
        repeat rewrite drop_correct. rewrite_eq (n + S k = S(n+k)).
        specialize (V (n + k)). simpl in V. unfold oiter_transition in V.
        enough (r (S (n + k)) <> initialW) by tauto. apply kNW. omega.
      + cbn in B.
        rewrite prepend_string_begin by comega.
        rewrite prepend_string_rest by comega. cbn.
        rewrite 2drop_correct.
        specialize (V (n + k)). simpl in V. unfold oiter_transition in V.
        enough (r (S (n + k)) = initialW) by tauto.
        rewrite <-mW. f_equal. omega.
    - unfold sinitial. rewrite prepend_string_begin by comega. cbn.
      rewrite drop_correct. rewrite_eq ( (n + 0) = n).
      rewrite nW. apply normW.
    - unfold sfinal. simpl.
      rewrite prepend_string_rest by comega.
      apply normW.
  Qed.

  Arguments infinite_filter [X] _ _ _ _ _.

  Lemma aut_accepts_nfa_omega_iter': L_B nfa_omega_iter' <$= (L_S aut)^00.
  Proof.
    intros w [r A].
    pose (A' := A). destruct A' as [V [I Fin]].
    apply lang_o_iter_extract.
    exists (infinite_filter r (fun s => s = initialW) (fun s=> decision (s = initialW)) Fin). repeat split.
    - apply infinite_filter_s_monotone.
    - apply infinite_filter_zero, I.
    - intros n. apply (initialW_partitions_in_W A).
      + apply infinite_filter_s_monotone.
      + apply infinite_filter_correct.
      + apply infinite_filter_correct.
      + apply infinite_filter_all.
  Qed.

  Lemma nfa_omega_iter'_correct: L_B nfa_omega_iter' =$= (L_S aut)^00.
  Proof.
    split. apply aut_accepts_nfa_omega_iter'. apply nfa_omega_iter'_accepts_aut.
  Qed.

  End OmegaIterNormalized.

  Definition nfa_omega_iter aut := nfa_omega_iter' (normalize_inital aut) (normalize_final aut).

  Lemma nfa_omega_iter_correct aut: L_B (nfa_omega_iter aut) =$= (L_S aut)^00.
  Proof.
    unfold nfa_omega_iter. rewrite nfa_omega_iter'_correct, <-normalize_correct.
    reflexivity. apply normalize_is_normalized.
  Qed.

End NFAOmegaIteration.

Closure under Prepending Regular Languages

Section PrependNFA.
  Context {X:finType}.

  Section PrependNormalizedNFA.

  Variable (aut_1 aut_2: NFA X).
  Variables (initialV finalV : state aut_1).
  Variable (norm: sautomaton_normalized initialV finalV).

  Definition prepend_state := (state aut_1) (x) (state aut_2).
  Implicit Types (s: prepend_state)(x:X).

  Definition prepend_transition s x s' := match s,s' with
      | (p, q) , (p',q') => (~ final_state p -> transition p x p' /\ initial_state q') /\
                            ( final_state p -> transition q x q' /\ p' = finalV)
  end.

  Definition prepend_state_final s := match s with (p, q) => final_state p /\ final_state q end.
  Definition prepend_state_initial s := match s with (p,q) => p = initialV /\ initial_state q end.

  Instance dec_prepend_transition s x s': dec (prepend_transition s x s'). Proof. destruct s,s'; simpl; auto. Qed.
  Instance dec_prepend_state_final s : dec (prepend_state_final s). Proof. destruct s; auto. Qed.
  Instance dev_prepend_state_initial s : dec (prepend_state_initial s). Proof. destruct s; auto. Qed.

  Definition prepend_nfa' := mknfa prepend_transition prepend_state_initial prepend_state_final.

  Arguments can_find_next_position [X] _ _ [w] [n] [m] _ _.

  Definition activeW (s:prepend_state) := match s with (q, _) => final_state q end.
  Instance decActivW s: dec (activeW s). Proof. destruct s. auto. Qed.

  Lemma switch_from_V_to_W r w : accepting (aut:=prepend_nfa') r w -> Sigma k, k > 0 /\ (forall n, n < k -> ~ activeW (r n)) /\ (forall n, activeW (r (n + k))).
  Proof.
    intros [V [I F]].
    assert (exists n, 0 <= n /\ activeW (r n)) as H. { destruct (F 0) as [n [P Q]]. exists n. split; auto. destruct (r n). apply Q. }
    exists (next_position_exists H). repeat split.
    - decide (next_position_exists H > 0); auto. exfalso.
      assert (next_position_exists H = 0) as H' by omega.
      pose proof (next_position_exists_correct H) as Q. rewrite H' in Q.
      unfold initial in I. destruct (r 0). apply norm. cbn in *. rewrite <-(proj1 I). now apply norm in Q.
    - intros n L. intros A. specialize (V n). destruct (r n) eqn:En. cbn in A.
      apply (next_position_exists_all (n:=0) (k:=n) (L:=H)).
      + split; oauto.
      + now rewrite En.
    - intros n. induction n.
      + cbn. pose proof (next_position_exists_correct H).
        destruct (r (next_position_exists H)) eqn:H'. cbn in *. now rewrite H'.
      + remember (next_position_exists H) as k. specialize (V ( n +k)). cbn.
        destruct (r (n+k)) as [s1 s2]. destruct (r (S (n +k))) as [s3 s4]. cbn in *.
        enough (s3 = finalV) as H2.
        * rewrite H2. apply norm.
        * now apply V.
  Qed.

  Lemma prepend_aut_is_prepend_omega: L_B prepend_nfa' <$= L_S aut_1 o L_B aut_2.
  Proof.
    intros w [r A].
    destruct (switch_from_V_to_W A) as [w_begin [G0 [AV AW]]].
    apply split_position_lang_prepend. exists (pred w_begin). destruct A as [V [I F]].
    split.
    - exists (fun n => match (r n) with (q,_) => q end).
      repeat split.
      + intros k L. simpl in L. specialize (V k). specialize (AV k).
        destruct (r k), (r (S k)). apply V, AV. omega.
      + unfold sinitial. compute in I. destruct (r 0). destruct I as [I _]. rewrite I. apply norm.
      + unfold sfinal. cbn. specialize (AW 0).
        rewrite_eq (S (pred w_begin) = w_begin). cbn in AW.
        destruct (r w_begin). apply AW.
    - exists (drop w_begin (fun n => match (r n) with (_,q) => q end)).
      repeat split.
      + intros k. specialize (V (k + w_begin)). specialize (AW k).
        rewrite_eq (S (pred w_begin) = w_begin). rewrite 3drop_correct'. cbn.
        destruct (r (k + w_begin)). destruct (r (S (k + w_begin ))). apply V, AW.
      + unfold initial. rewrite drop_correct'. specialize (V (pred w_begin)).
        rewrite_eq (S(pred w_begin) = w_begin) in V. cbn.
        specialize (AV (pred w_begin)). destruct (r w_begin).
        destruct (r (pred (w_begin))). cbn in V. apply V, AV. omega.
      + apply final_drop. intros n. destruct (F n) as [m [P Q]]. exists m. split; oauto.
        destruct (r m). apply Q.
  Qed.

  Lemma prepend_aut_accepts_prepend_omega: L_S aut_1 o L_B aut_2 <$= L_B prepend_nfa'.
  Proof.
   intros w [v [w' [E [[rv [Vv [Iv Fv]]] [rw [Vw [Iw Fw]]]]]]]. rewrite E.
   exists (mkstring (seq_zip rv (fun _ => rw 0)) (|v|) +++ (seq_zip (fun _ => finalV) rw)).
    split; [|split].
   - intros n. decide (n <= |v| ) as[D'|D'].
     + rewrite prepend_string_begin by comega.
       decide (S n <= |v|) as [D|D].
       * rewrite !prepend_string_begin by comega. cbn. split.
         -- intros nF. split. apply Vv. comega. apply Iw.
         -- intros F. exfalso. specialize (Vv n D'). apply norm in F. rewrite F in Vv. now apply norm in Vv.
       * assert (n = |v|) by omega. subst n. rewrite prepend_string_begin, prepend_string_rest by comega. cbn. split.
         -- intros nF. split.
            ++ unfold sfinal in Fv. cbn in Fv. apply norm in Fv. rewrite <-Fv. apply Vv. comega.
            ++ rewrite_eq (|v| - (|v|) = 0). apply Iw.
         -- intros F. exfalso. specialize (Vv (|v|) D'). apply norm in F. rewrite F in Vv. now apply norm in Vv.
     + rewrite 3prepend_string_rest by comega. cbn. split.
       * intros F. exfalso. apply F. apply norm.
       * specialize (E (n )). rewrite prepend_string_rest in E by omega. rewrite <-E.
         intros F. split; auto. specialize (Vw (n - S (|v|))).
         rewrite <-E in Vw.
         now rewrite_eq (S (n - S (|v|)) = n - (|v|)) in Vw.
   - unfold initial. rewrite prepend_string_begin by omega. cbn. split.
     apply norm, Iv. apply Iw.
   - apply final_prepend. intros n. destruct (Fw n) as [m [P Q]]. exists m. repeat split; oauto. apply norm.
   Qed.

  Lemma prepend_nfa'_correct: L_B prepend_nfa' =$= L_S aut_1 o L_B aut_2.
  Proof.
    split. apply prepend_aut_is_prepend_omega. apply prepend_aut_accepts_prepend_omega.
  Qed.

  End PrependNormalizedNFA.

  Definition prepend_nfa aut_1 aut_2 := prepend_nfa' aut_2 (normalize_inital aut_1) (normalize_final aut_1).
  Lemma prepend_nfa_correct aut_1 aut_2 : L_B (prepend_nfa aut_1 aut_2) =$= (L_S aut_1) o (L_B aut_2).
  Proof.
    unfold prepend_nfa. rewrite prepend_nfa'_correct, <-normalize_correct.
    reflexivity. apply normalize_is_normalized.
  Qed.

End PrependNFA.

Section ConcatInfPrependNFA.

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

  Variable strings: Seq (String X).
  Variable runs: Seq (String (state aut)).

Facts showing that Composing the Sequence carry over to the Run
If the sequence is obtained by prepending, we can split the run accordingly.
  Lemma partition_run_on_prepend_string w0 w r : valid_run (aut:=aut) r (w0 +++ w) ->
     exists r0 r', (r0 +++ r') === r /\ (|r0| = |w0|) /\ (r0 [S(|r0|)] = r' 0) /\ valid_path (seq r0) w0 /\ valid_run r' w.
  Proof.
   intros V.
   exists (mkstring r (|w0|)); exists (drop (S(|w0|)) r). repeat split.
   - now rewrite revert_drop.
   - cbn. rewrite drop_correct. f_equal. omega.
   - assert (w0 == mkstring (w0 +++w) (|w0|)) as H. { split;cbn;oauto. intros n L. now rewrite prepend_string_begin. }
     rewrite H. now apply valid_run_is_path_from_begin.
   - rewrite <-revert_prepend_string with (v:= w0). now apply valid_run_drop.
  Qed.

Likewise, if the sequence was obtained by infinite concattenation, the run can be partitioned into infinitely many strings
  Lemma partition_run_on_concat_inf W r : valid_run (aut:=aut) r (concat_inf W) ->
     exists R, concat_inf R === r /\
        (forall k, |R k| = |W k| /\ valid_path (seq (R k)) (W k)) /\
         (forall k, (R k)[ S(|R k|)] = (R (S k)) [0]) .
  Proof.
    intros V.
    exists (fun n => extract (begin_in W n) (begin_in W (S n)) r). repeat split.
    - intros n.
      unfold concat_inf.
      destruct (concat_inf_indices) as [w i] eqn:H.
      simpl. rewrite drop_correct.
      apply concat_inf_index_to_begin in H. destruct H as [H _].
      rewrite H. f_equal. f_equal. apply begin_in_equal. intros k. comega.
    - comega.
    - cbn. intros n L.
      rewrite 2drop_correct', <-concat_inf_correct by auto. cbn. apply V.
    - intros k. cbn. rewrite 2drop_correct. f_equal. omega.
  Qed.

End ConcatInfPrependNFA.

Decidability of word problem for UP Sequences


Definition exact_up_nfa (X:finType) (u v : String X):= prepend_nfa (os_nfa u) (nfa_omega_iter (os_nfa v)).
Lemma exact_up_nfa_correct (X:finType) (u v : String X): L_B (exact_up_nfa u v) =$= fun w => w === u +++ v to_omega.
Proof.
 unfold exact_up_nfa.
 rewrite prepend_nfa_correct, nfa_omega_iter_correct, 2os_nfa_correct.
 intros w. split.
 - intros [u' [w' [E1 [E2 [w'' [E3 E4]]]]]].
   now rewrite E1, E2, E4, (concat_inf_extensional E3).
 - intros E. exists u, (v to_omega). repeat split; auto.
   exists (fun _ => v). repeat split; auto.
Qed.

Lemma dec_up_in_lang (X: finType)(v w : String X) (A: NFA X): dec (L_B A (v+++w to_omega)).
Proof.
  destruct (dec_language_empty_informative (intersect A (exact_up_nfa v w))) as [D|D].
  - left. destruct D as [w' [L1 L2%exact_up_nfa_correct] % intersect_correct].
    now rewrite <-L2.
  - right. intros L.
    apply (D (v +++ w to_omega)). apply intersect_correct. split.
    + apply L.
    + now apply exact_up_nfa_correct.
Qed.