Set Implicit Arguments.

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

Open Scope list_scope.
Close Scope string_scope.

Admissible Sequence Structures

Class SequenceStructure := mkSequenceStructure {
   ASeq: finType -> Type;
   aseq_to_seq: forall (X:finType), ASeq X -> Seq X;
   azip: forall (X Y: finType), ASeq X -> ASeq Y -> ASeq (X (x) Y);
   amap: forall (X Y:finType), (X -> Y) -> ASeq X -> ASeq Y;
   exact_at: forall (X: finType), X -> X -> nat -> ASeq X;
   azip_correct: forall (X Y: finType) (w:ASeq X) (w':ASeq Y),(aseq_to_seq (azip w w')) === seq_zip(aseq_to_seq w)(aseq_to_seq w');
   amap_correct : forall (X Y: finType) (f: X -> Y) (w: ASeq X), aseq_to_seq (amap f w) === seq_map f (aseq_to_seq w);
   exact_at_correct: forall (X:finType) (x y : X) (n : nat), x <> y -> forall m, aseq_to_seq (exact_at x y n) m = x <-> m = n

Arguments ASeq {A} X : rename.
Arguments aseq_to_seq {A} {X} : rename.
Arguments azip {A}{X}{Y} : rename.
Arguments azip_correct {A}{X}{Y} w w': rename.
Arguments amap {A}{X}{Y}: rename.
Arguments amap_correct {A}{X}{Y}:rename.

Coercion aseq_to_seq: ASeq >-> Seq .
Identity Coercion applySeq: Seq >-> Funclass .

Section BigZip.

  Context {CC: SequenceStructure}.

  Definition aseq_equal (A: finType) : ASeq A -> ASeq A -> Prop := @seq_equal A.

  Instance aseq_equal_equiv (A:finType): Equivalence (@aseq_equal A).
    repeat split; unfold aseq_equal.
    - intros w w' E. symmetry. apply E.
    - intros w1 w2 w3 E1 E2. now rewrite E1, <-E2.

  Instance amap_proper (A B:finType)(f: A-> B): Proper ((@aseq_equal A ) ==> (@aseq_equal B)) (amap f).
    intros w w' E n. rewrite !amap_correct. unfold seq_map. now rewrite E.

  Notation "w ==== w'" := (aseq_equal w w') (at level 71).
  Lemma test (A B: finType) (w w': ASeq A) (f: A -> B) : w ==== w' -> (amap f w) ==== (amap f w').
    intros E. now rewrite E.

  Implicit Types (x:X)(y:Y)(L:list Y).

  Definition const (X:finType) (x:X) := amap (fun _ => x) (exact_at x x 0).
  Lemma const_correct x: const x === fun _ => x.
    intros n. unfold const. now rewrite amap_correct.

  Definition zipFinTypes y L: (X * X^^L) -> X^^(y::L).
    intros [C V].
    apply vectorise. intros [x P].
    decide (x = y) as [<-|D].
    - exact C.
    - apply (applyVect V). exists x. apply pure_equiv in P. destruct P as [P|P].
      + exfalso. auto.
      + now apply pure_equiv.

  Fixpoint bigzip' L (f: (finType_fromList L)-> ASeq X) {struct L}: ASeq (X^^L).
    destruct L as [| y L].
    - apply const. apply vectorise. intros [x P]. exfalso. now apply pure_equiv in P.
    -apply (amap (@zipFinTypes y L)).
     apply azip.
      + apply f. exists y. apply pure_equiv. now left.
      + apply bigzip'. intros [x P]. apply f. exists x. apply pure_equiv. right. now apply pure_equiv in P.

  Definition elemToFinType : X^^(elem Y) -> X^Y.
    intros Z. apply vectorise. intros i.
    apply (applyVect Z). exists i. apply pure_equiv. auto.

  Definition bigzip (f: Y -> ASeq X): (ASeq (X^Y)).
    apply (amap elemToFinType). apply bigzip'.
    intros [i _]. exact (f i).

  Lemma bigzip_correct' L (f: (finType_fromList L)-> ASeq X) (Z:finType_fromList L) n: applyVect ((bigzip' f) n) Z = (f Z) n.
    induction L as [|x L].
    - exfalso. destruct Z as [x P]. now apply pure_equiv in P.
    - cbn. rewrite amap_correct.
      destruct Z as [z P].
      unfold seq_map, zipFinTypes. cbn. rewrite azip_correct. unfold seq_zip.
      rewrite apply_vectorise_inverse. destruct decision as [<- | D].
      + cbn. repeat f_equal. apply pure_eq.
      + rewrite IHL. repeat f_equal. apply pure_eq.

  Lemma bigzip_correct (f : Y -> ASeq X) y n: applyVect ((bigzip f) n) y = (f y) n.
    unfold bigzip. rewrite amap_correct. unfold seq_map, elemToFinType.
    now rewrite apply_vectorise_inverse, bigzip_correct'.

  Definition bigpi : ASeq (X^Y) -> Y -> ASeq X.
    intros w i.
    apply (amap (fun v => applyVect v i)). exact w.

  Lemma bigpi_correct (w: ASeq (X^Y)) y n : (bigpi w y) n = applyVect (w n) y.
    unfold bigpi. now rewrite amap_correct.

End BigZip.

  Notation "w ==== w'" := (aseq_equal w w') (at level 71).

Definition L_A {CC: SequenceStructure} (A:finType) (aut : NFA A) : Language (ASeq A) := fun w => L_B aut (aseq_to_seq w).
Definition LAmap {CC: SequenceStructure} (X Y :finType) (f: X->Y) (L : Language (ASeq X)) : Language (ASeq Y) := fun w => exists w', amap f w' ==== w /\ L w'.
Definition APreImage {CC: SequenceStructure} (X Y: finType) (f: X -> Y) (L: Language (ASeq Y )) : Language (ASeq X) := fun w => L (amap f w).

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

Class AdmissibleSequenceStructure := mkAdmissibleSequenceStructure {
   CC :> SequenceStructure;
   dec_alanguage_empty_informative: forall (A: finType) (aut: NFA A), {exists w, L_A aut w} + {L_A aut =$= {}};
   totality: forall (A:finType) (aut: NFA A) (w : ASeq A), exists (V W:EqClass(aut:=aut)), ({[V]}o({[W]})^00 )(aseq_to_seq w);
   aseq_run: forall (A:finType) (aut: NFA A) (w: ASeq A), L_A aut w -> (exists (r: ASeq (state aut)), accepting (aseq_to_seq r) (aseq_to_seq w));

   map_aut_acorrect : forall (X Y:finType) (f: X ->Y) (aut: NFA X) , L_A (image_aut f aut) =$= LAmap f (L_A aut)


Closure Properties transfer to AS Structures

Section ClosureProperties.

  Variable (AC: AdmissibleSequenceStructure).
  Variable (X Y: finType).

  Lemma empty_aut_acorrect: L_A (empty_aut (X:=X)) =$= {}.
    intros a. split; intros B; exfalso.
    - now apply empty_aut_correct in B.
    - assumption.

  Lemma preimage_aut_acorrect (f: X-> Y) (aut: NFA Y): L_A (preimage_aut f aut) =$= APreImage f (L_A aut).
    - intros LA. apply preimage_aut_correct in LA. unfold APreImage,L_A. now rewrite amap_correct.
    - intros LA. unfold L_A, APreImage in *. apply preimage_aut_correct.
       now rewrite amap_correct in LA.

  Lemma union_acorrect (aut_1 aut_2 :NFA X): L_A (union aut_1 aut_2) =$= L_A aut_1 \$/ L_A aut_2.
    intros w. split; eauto using union_correct.
    - intros [B|B] % union_correct; [now left | now right].
    - intros [B|B]; apply union_correct; [now left| now right].

  Lemma intersect_acorrect (aut_1 aut_2 :NFA X): L_A (intersect aut_1 aut_2) =$= L_A aut_1 /$\ L_A aut_2.
    intros w. split.
    - intros B % intersect_correct. split; apply B.
    - intros [B1 B2]. apply intersect_correct. now split.

  Lemma big_union_acorrect (l:list (NFA X)) :
             L_A (big_union l) =$= fun w => exists a, (a el l) /\ L_A a w.
    intros w. split.
    - intros [a [P Q]] % big_union_correct. exists a. split; auto.
    - intros [a [P Q]]. apply big_union_correct. exists a. split; auto.

  Lemma dec_alanguage_empty (aut: NFA X): dec (L_A aut =$= {}).
      destruct (dec_alanguage_empty_informative aut) as [D|D].
      - right. intros E. destruct D as [w D]. now apply E in D.
      - now left.

Correctness of Complementation

  Section Complement.

  Variable (aut: NFA X).

  Implicit Types ( V W : EqClass (aut:=aut)).

    Lemma autC_disjoint: L_A aut /$\ L_A (complement aut) =$= {}.
      apply language_empty_iff. intros w [LA LC].
      destruct (totality aut w) as [V [W P]].
      unfold complement in LC. apply big_union_acorrect in LC. destruct LC as [b [IC LB]].
      unfold complement_auts in IC. apply in_map_iff in IC. destruct IC as [vw [AVW Q]].
      apply in_filter_iff in Q. destruct Q as [Q1 Q2].
      apply (Q2 (aseq_to_seq w)).
      apply intersect_acorrect. split.
      - now rewrite AVW.
      - assumption.

    Definition toL_A (L : SeqLang X) := fun (aseq : ASeq X) => (L (aseq_to_seq aseq)).

    Lemma part_of_complement_implies_complement V W: VW_part_of_complement (V,W) -> toL_A ({[V]}o{[W]}^00) <$= L_A (complement aut).
     intros PC w VW.
     apply big_union_acorrect.
     exists (VW_aut V W). split.
     - unfold complement_auts.
       apply in_map_iff.
       exists (V,W). split;auto.
       apply in_filter_iff. split.
       + apply elementIn.
       + unfold VW_part_of_complement. simpl.
         apply language_empty_iff. intros w' L. now apply (PC w').
     - now apply VW_aut_correct.

    Lemma not_part_of_complement_implies_aut V W: ~VW_part_of_complement (V,W) -> toL_A ({[V]}o{[W]}^00) <$= L_A aut.
     intros nPC w VW.
     unfold VW_part_of_complement in nPC.
     destruct (dec_language_empty_informative (intersect (VW_aut V W) aut )) as [D|D].
     - destruct D as [w' L]. apply intersect_correct in L.
       apply (compatibility (w:=w') (V:=V)(W:=W)).
       + destruct L as [L1 L2]. now apply VW_aut_correct in L1.
       + assumption.
     - cbn in nPC. exfalso. apply nPC. intros w'. split.
       + intros B. specialize (D w'). exfalso. apply D. auto.
       + intros E. exfalso. auto.

    Lemma complement_complete : L_A (complement aut) \$/ L_A aut =$= universal_language.
     apply language_universal_iff. intros w.
     destruct (totality aut w) as [V [W P]].
     destruct (dec_VW_part_of_complement (V,W)) as [D|D].
     - left. now apply (part_of_complement_implies_complement D).
     - right. now apply (not_part_of_complement_implies_aut D).

    Lemma complement_correct: L_A (complement aut) =$= (L_A aut)^$~.
      intros w. destruct (complement_complete w). pose (autC_disjoint w).
      autounfold in *. tauto.

    Lemma complement_correct2: (L_A (complement aut))^$~ =$= L_A aut.
      intros w. destruct (complement_complete w). pose (autC_disjoint w).
      autounfold in *. tauto.
  End Complement.

Decision Corallaries

  Section ComplementCorollaries.

   Corollary dec_language_universal (aut:NFA X) : dec(L_A aut =$= universal_language).
    destruct (dec_alanguage_empty (complement aut)) as [D|D].
    - left. apply language_universal_iff. intros w. specialize (D w).
      destruct (complement_complete aut w). autounfold in *. tauto.
    - right. intros L. apply D. intros w. pose (complement_correct2 aut w).
      autounfold in *. specialize (L w). tauto.

   Corollary dec_language_inclusion (aut1 aut2:NFA X): dec (L_A aut1 <$= L_A aut2).
     destruct (dec_alanguage_empty (intersect aut1 (complement aut2))) as [D|D].
     - left. intros w L. specialize (D w).
       destruct (complement_complete aut2 w) as [_ [D'| D']].
       + auto.
       + exfalso. apply D. now apply intersect_acorrect.
       + assumption.
     - right. intros I. apply D. apply language_empty_iff.
       intros w L. apply intersect_acorrect in L. destruct L as [L1 L2].
       apply complement_correct in L2. auto.

   Corollary dec_language_eq (aut1 aut2:NFA X): dec (L_A aut1 =$= L_A aut2).
     pose (language_eq_iff (L_A aut1) (L_A aut2)) as P.
     apply dec_trans with (P:=language_inclusion (L_A aut1) (L_A aut2) /\ language_inclusion (L_A aut2) (L_A aut1)).
     - auto using and_dec, dec_language_inclusion.
     - split; apply language_eq_iff.

   Corollary xm_word_problem (aut: NFA X) w : L_A aut w \/ ~ L_A aut w.
     destruct (complement_complete aut w) as [_ H].
     destruct (H I).
     - right. now apply complement_correct.
     - left. assumption.

  End ComplementCorollaries.

End ClosureProperties.

Instatiations of AS Structures


Definition OmegaSequenceStructure : SequenceStructure.
  apply (mkSequenceStructure
    (ASeq := Seq)
    (aseq_to_seq := fun (X:finType) (w:Seq X) => w)
    (azip := fun(X Y:finType) => @seq_zip X Y)
    (amap := fun(X Y:finType) => @seq_map X Y)
    (exact_at := fun (X:finType)(x y : X) n m => if (decision (n = m)) then x else y)).
  - now reflexivity.
  - now reflexivity.
  - intros X x y n D m. destruct decision; split ;intros K; congruence.

Definition OmegaStructure (AR: forall C, AdditiveRamsey C): AdmissibleSequenceStructure.
  apply (mkAdmissibleSequenceStructure (CC:=OmegaSequenceStructure)).
  - intros A aut. apply dec_language_empty_informative.
  - intros A aut w. apply ramseyTotality. apply AR.
  - eauto.
  - intros A B aut. unfold LAmap, L_A. apply image_aut_correct.


Definition UPSequenceStructure : SequenceStructure.
  apply (mkSequenceStructure
    (ASeq := UPSeq)
    (aseq_to_seq := unfold)
    (amap := fun (X Y:finType) => @up_map X Y)
    (azip := fun (X Y:finType) => @up_zip X Y)
    (exact_at := fun (X:finType) (x y : X) (n : nat) => mkUPSeq (mkstring (fun m => if (decision (m = n)) then x else y) n)( mkstring (fun n => y) 0))).
  - intros X Y w w'. now apply up_zip_correct.
  - intros X Y f w. now apply up_map_correct.
  - intros X x y n D m. unfold unfold; rewrite up_prefix, up_loop. decide (m <= n).
    + rewrite prepend_string_begin by comega. cbn. destruct decision as [<-|D']. tauto. split; intros Z; exfalso; auto.
    + rewrite prepend_string_rest by comega. cbn. split; intros Z; exfalso. auto. omega.

Instance seq_dec_exists_bounded (X: Type)(P: X -> Prop) (decP: forall n, dec (P n)) (w : Seq X) n: dec( exists k, k <= n /\ P (w k)).
Proof. auto.

Section UPAdmissible.

  Existing Instance UPSequenceStructure.
Every accepted UP Sequence has an accepting UP run
  Section PeriodicRun.

  Open Scope string_scope.

  Variable (aut: NFA A).

  Lemma prepend_string_valid_run q r v w: |q| = (|v|) -> valid_path (seq q) v -> transition (q [(|q|)]) (v[(|v|)]) (r 0) -> valid_run (aut:=aut) r w -> valid_run (q +++ r) (v +++ w).
    intros E VP T VR.
    intros n. decide (n < |v|) as [D|D].
    - repeat rewrite prepend_string_begin by omega. apply VP. omega.
    - decide (n = |v|) as [D' | D'].
      + repeat rewrite prepend_string_begin by omega. rewrite prepend_string_rest by omega.
        rewrite E. subst n. rewrite_eq (S(|v|) - S(|v|) = 0). rewrite E in T. apply T.
      + repeat rewrite prepend_string_rest by omega. rewrite_eq (S n - S (| q |) = S (n - S(|q|))). rewrite E. apply VR.

  Lemma valid_path_prepended_string (r: Run aut) v w: valid_run r (v +++ w) -> valid_path r v.
    intros V n L. specialize (V n). now rewrite prepend_string_begin in V.

  Lemma omega_iteration_valid_run (r: String (state aut)) w: |r| = |w| -> valid_path (seq r) w -> transition (r [(|r|)]) (w[(|w|)]) (r [0]) -> valid_run (r to_omega) (w to_omega).
    (* This proof is kind of duplicated as in NFA, but I do not want to depent on these old proofs anymore *)
    intros E V P n. unfold omega_iteration, concat_inf.
    rewrite (concat_inf_index_equal (f:=(fun _ : nat => w)) (g:=(fun _ : nat => r))) by auto.
    destruct (concat_inf_indices (fun _ : nat => r)) as [wi i] eqn:H.
    destruct (concat_inf_index_step_correct H) as [J|J]; cbn; cbn in J; rewrite H in J; rewrite H; cbn.
    - rewrite J. cbn. apply V. rewrite <-E. apply (concat_inf_index_in_bounds H).
    - destruct decision; cbn.
      + subst i. now rewrite <-E in P.
      + apply V. omega.

  Lemma valid_periodic_run v w (q r : String (state aut)) : |q| = |v| -> |r| = |w| -> valid_path (seq q) v -> transition (q [(|q|)]) (v[(|v|)]) (r [0])
                                                                                   -> valid_path (seq r) w -> transition (r [(|r|)]) (w[(|w|)]) (r [0])
                                                                 -> valid_run (q +++ r to_omega) (v +++ w to_omega).
    intros E1 E2 V1 T1 V2 T2.
    apply prepend_string_valid_run, omega_iteration_valid_run; auto.

  Variable (vw : UPSeq A).

  Definition critical_index_unfold (r:Run aut) n k k' := k' <= |loop vw| /\ (final_state (r (n + k')) /\ S(|prefix vw|) + k * (S(|loop vw|)) = n) .
  Definition critical_index (r: Run aut) n := exists k k', critical_index_unfold r n k k'.

  Instance dec_critical_index_unfold r n k k': dec (critical_index_unfold r n k k').
  Proof. auto. Qed.

  Lemma critical_index_unfold_bound r n k k': critical_index_unfold r n k k' -> k <= n.
    intros [_ [_ C]]. rewrite <-C.
    enough (k <= k * S(|loop vw|)) by omega.
    rewrite <-Nat.mul_1_r with (n := k) at 1.
    apply Nat.mul_le_mono_nonneg_l; omega.

  Instance dec_ciritcal_index r n : dec (critical_index r n).
    apply dec_trans with (P:= exists k, k <= n /\ exists k', critical_index_unfold r n k k').
    - apply (seq_dec_exists_bounded (P:=fun k => (exists k' : nat, critical_index_unfold r n k k'))). intros k.
      unfold critical_index_unfold.
                apply (seq_dec_exists_bounded (P:= fun k' => final_state (r (n + k')) /\ S(| prefix vw |) + k * S (| loop vw |) = n)). intros k'. auto.
    - split.
      + firstorder.
      + intros [k [k' C]]. exists k. split.
        * apply (critical_index_unfold_bound C).
        * firstorder.

  Lemma critical_index_unfold_monotone r n1 n2 k1 k2 k'1 k'2: critical_index_unfold r n1 k1 k'1 -> critical_index_unfold r n2 k2 k'2 -> n1 < n2 -> k1 < k2.
    intros [_[_ C1]] [_[_ C2]] L.
    enough (k1 * S(|loop vw|) < k2 * S(|loop vw|)).
    - rewrite Nat.mul_lt_mono_pos_r with (p:= S(|loop vw|)); oauto.
    - omega.

  Lemma critical_index_unfold_ge_zero r n k k': critical_index_unfold r n k k' -> S (| prefix vw |) < n -> 0 < k.
    intros [_ [_ C]] L.
    enough (0 < k * S(|loop vw|)).
    - rewrite Nat.mul_pos_cancel_r in H; omega.
    - omega.

  Lemma critical_index_unfold_pred_index r n k k': critical_index_unfold r n k k' -> 0 < k -> unfold vw (n - 1) = (loop vw) [|loop vw|].
    intros [C1 [_ C2]] L.
    unfold unfold. subst n.
    assert (0 < k * S(|loop vw|)). { rewrite Nat.mul_pos_cancel_r; omega. }
    rewrite prepend_string_rest.
    - rewrite_eq (S (| prefix vw |) + k * S (| loop vw |) - 1 - S (| prefix vw |) = k * S (| loop vw |) - 1).
      rewrite omega_iter_unfold with (n := k). rewrite prepend_string_begin.
      + apply fin_iter_last_index. omega.
      + rewrite fin_iter_length. enough (k * S (| loop vw |) <= S k * S (| loop vw |) ) by omega. apply Nat.mul_le_mono_nonneg_r; omega.
    - omega.

  Lemma critical_index_unfold_distance r n1 n2 k1 k2 k'1 k'2: critical_index_unfold r n1 k1 k'1 -> critical_index_unfold r n2 k2 k'2 -> k1 < k2 -> |loop vw| <= n2 - S n1.
    intros [_ [_ C1]] [_ [_ C2]] L.
    subst n1 n2.
    enough (| loop vw | <= k2 * S (| loop vw |) - S (k1 * S (| loop vw |))) by omega.
    destruct k2.
    - exfalso. omega.
    - rewrite Nat.mul_succ_l.
      enough (k1 * S(|loop vw|) <= k2 * S(|loop vw|)) by omega.
      apply Nat.mul_le_mono_nonneg_r; omega.

  Lemma critical_index_unfold_distance' r n1 n2 k1 k2 k'1 k'2: critical_index_unfold r n1 k1 k'1 -> critical_index_unfold r n2 k2 k'2 -> k1 < k2 -> k'1 <= n2 - S n1.
    intros C1 C2 L. assert ( k'1 <= |loop vw|) by apply C1.
    enough (|loop vw| <= n2 - S n1) by omega.
    now apply (critical_index_unfold_distance C1 C2).

  Lemma find_multiplicative n m : 0 < m -> exists k, k <= S n /\ n < k * m <= n + m.
    intros L.
    decide (m = 1).
    - subst m. exists (S n). omega.
    - destruct n.
      + exists 1. repeat split; omega.
      + exists (S(S n / m)). repeat split.
        * enough ((S n / m) < (S n)) by omega. apply Nat.div_lt ; omega.
        * rewrite Nat.mul_comm. apply (Nat.mul_succ_div_gt (S n) m). omega.
        * rewrite Nat.mul_comm, Nat.mul_succ_r. cbn. enough (m * (S n / m) <= S n) by omega. apply (Nat.mul_div_le (S n) m). omega.

  Lemma final_state_eq (r:Run aut) n m : final_state (r n) -> n = m -> final_state (r m).
    intros Fs E. now rewrite <-E.

  Lemma final_to_critical r n : final_state (r (n + S(|prefix vw|) + S(|loop vw|))) -> exists m, m >= n /\ critical_index r m.
    intros F.
    destruct (find_multiplicative (n) (m:=S(|loop vw|))) as [k [L M]]. { omega. }
    exists (S(|prefix vw|) + k * (S (|loop vw|))). repeat split.
    - omega.
    - exists k, ((n + S (|loop vw|)) - k * (S(|loop vw|))).
      repeat split.
      + omega.
      + apply (final_state_eq F). omega.

  Lemma infinite_final_implies_infinite_critical r : final r -> forall n, exists m, m >= n /\ critical_index r m.
    intros F n.
    destruct (F (n + S(|prefix vw|) + S (|loop vw|))) as [m' [L' F']].
    pose (n' := m' - S(|prefix vw|) - S (|loop vw|)).
    enough (exists m, m >= n' /\ critical_index r m).
    - destruct H as [m'' C]. exists m''. split.
      + subst n'. omega.
      + tauto.
    - apply final_to_critical. subst n'.
      apply (final_state_eq F'). omega.

  Lemma split_critical_index_begin r n k k': critical_index_unfold r n k k' -> k > 0 -> S(|prefix vw|) + S (|(fin_iter (loop vw) (pred k))|) = n.
    intros [_ [_ C]] G.
    cbn. rewrite fin_iter_length. rewrite_eq (S (pred k) = k). subst n. remember (k * S (|loop vw|)) as Z.
    enough (0 < Z) by omega.
    subst Z. apply Nat.mul_pos_cancel_r; omega.

  Lemma periodic_run: L_B aut (unfold vw) -> exists rs, accepting (aut:=aut) (unfold rs) (unfold vw).
    intros [r [V [I F]]].

    pose (r_f := infinite_filter (infinite_final_implies_infinite_critical F)).
    destruct (can_find_duplicate' (S(S(|prefix vw|))) (S (Cardinality (state aut))+ S(S(|prefix vw|))) (fun n => r (r_f n))) as [[n1 [n2 [P Q]]]|D].
    - unfold unfold. exists (mkUPSeq (extract 0 (r_f n1) r) (extract (r_f n1) (r_f n2) r)).
     destruct (infinite_filter_correct (infinite_final_implies_infinite_critical F) n1) as [k1 [k1' H1]].
     destruct (infinite_filter_correct (infinite_final_implies_infinite_critical F) n2) as [k2 [k2' H2]].
     assert (0 < n1 < n2) by omega.
     assert (0 < k1 < k2). {split.
        - apply (critical_index_unfold_ge_zero H1).
          enough (n1 <= infinite_filter (infinite_final_implies_infinite_critical F) n1) by omega.
          apply s_monotone_ge, infinite_filter_s_monotone.
        - apply (critical_index_unfold_monotone H1 H2). apply s_monotone_strict_order_preserving.
          + apply infinite_filter_s_monotone.
          + omega. }
     repeat split.
      + rewrite (omega_iter_unfold (loop vw) (pred k1) ).
        rewrite <-concat_prepend_string_associative.
        apply prepend_string_valid_run.
        * cbn. enough (r_f n1 > 0) as Z.
          -- subst r_f. pose (split_critical_index_begin H1) as Eq. cbn in Eq. omega.
          -- enough (n1 <= r_f n1) by omega. apply s_monotone_ge. subst r_f. apply infinite_filter_s_monotone.
        * cbn. intros n L. specialize (V n). cbn in V. unfold unfold in V. rewrite (omega_iter_unfold (loop vw) (pred k1)) in V.
          rewrite <-concat_prepend_string_associative in V. rewrite prepend_string_begin in V by auto. apply V.
        * rewrite concat_string_rest by comega. cbn. rewrite drop_correct.
          enough (((| prefix vw |) + S (| fin_iter (loop vw) (pred k1) |))= r_f n1 - 1) as Q'.
          -- rewrite Q'.
             assert ( (fin_iter (loop vw) (pred k1)) [r_f n1 -1- S (| prefix vw |)] = (unfold vw (r_f n1 -1 ))) as H'. {
                unfold unfold. rewrite prepend_string_rest by omega.
                rewrite (omega_iter_unfold (loop vw) (pred k1)).
                now rewrite prepend_string_begin by omega.
             rewrite H'. assert (r_f n1 > 0). { enough (r_f n1 >= n1) by omega. apply s_monotone_ge, infinite_filter_s_monotone. }
             rewrite_eq (r_f n1 + 0 = S(r_f n1 - 1)). apply V.
          -- subst r_f. rewrite <-(proj2 (proj2 H1)). rewrite fin_iter_length. rewrite_eq (S(pred k1) = k1).
             remember (k1 * S (|loop vw|)) as Z. enough (0 < Z ) by omega. subst Z. apply Nat.mul_pos_cancel_r; omega.
        * cbn. rewrite (fin_iter_to_omega (loop vw) (pred (k2 - k1))). apply omega_iteration_valid_run.
          -- cbn. rewrite fin_iter_length. rewrite_eq (S (pred (k2 - k1)) = k2 - k1).
             pose (split_critical_index_begin H1) as Eq1.
             pose (split_critical_index_begin H2) as Eq2. cbn in Eq1,Eq2. rewrite fin_iter_length in Eq1,Eq2.
             rewrite_eq (S (pred k1) = k1) in Eq1. rewrite_eq (S (pred k2) = k2) in Eq2.
             subst r_f. rewrite <-Eq1, <-Eq2 by oauto. rewrite (Nat.mul_sub_distr_r).
             remember (k2 * S (| loop vw |)) as Z2. remember (k1 * S (| loop vw |)) as Z1.
             enough (0 < Z1 /\ 0 < Z2) by omega.
             split; [subst Z1 | subst Z2]; apply Nat.mul_pos_cancel_r; omega.
          -- intros n L.
             cbn. repeat rewrite drop_correct.
             enough ((fin_iter (loop vw) (pred (k2 - k1))) [n] = (unfold vw) (r_f n1 + n)) as H'.
             ++ rewrite H'. rewrite_eq (r_f n1 + S n = S (r_f n1 + n)). apply V.
             ++ unfold unfold. rewrite prepend_string_rest. destruct H1 as [_ [_ H1]].
                unfold r_f. rewrite <-H1. rewrite (omega_iter_unfold (loop vw) (pred k1)).
                rewrite prepend_string_rest.
                ** rewrite (omega_iter_unfold (loop vw) (pred (k2 - k1))).
                   rewrite prepend_string_begin.
                   --- f_equal. rewrite fin_iter_length.
                        rewrite_eq (S (pred k1) = k1). remember (k1 * (S(|loop vw|))) as C.
                        enough (0 < C) by omega. subst C. apply Nat.mul_pos_cancel_r; omega.
                   --- rewrite fin_iter_length in L. repeat rewrite fin_iter_length.
                        rewrite_eq (S(pred (k2 - k1)) = k2 - k1). rewrite_eq (S(pred (k2 - k1)) = k2 - k1) in L.
                        rewrite_eq (S (pred k1) = k1).
                        remember (k1 * S(|loop vw|)) as C.
                        enough (0 < C) by (rewrite_eq (S(C-1) = C); omega).
                        subst C. apply Nat.mul_pos_cancel_r; omega.
                ** rewrite fin_iter_length. rewrite_eq (S (pred k1) = k1). remember (k1 * S(|loop vw|)) as C.
                   enough (0 < C) by omega. subst C. apply Nat.mul_pos_cancel_r; omega.
                ** subst r_f. destruct H1 as [_ [_ H1]]. rewrite <-H1. remember (k1 * S(|loop vw|)) as C. omega.
          -- cbn. rewrite drop_correct. rewrite fin_iter_length. rewrite drop_correct.
             remember (r_f n1) as N1. remember (r_f n2) as N2.
             assert (N1 < N2). { subst N1 N2. apply s_monotone_strict_order_preserving. subst r_f. apply infinite_filter_s_monotone. omega. }
             rewrite_eq (N1 + (N2 - S N1) = N2 - 1). rewrite_eq (S (pred (k2 - k1)) = k2 - k1).
             rewrite fin_iter_last_index.
             ++ destruct Q as [_ Q]. rewrite_eq (N1 + 0 = N1). rewrite Q.
                specialize (V (N2 -1)). rewrite_eq (S (N2 -1) = N2) in V.
                enough (unfold vw (N2 -1) = (loop vw)[|loop vw|]) as H'.
                ** now rewrite <-H'.
                ** subst N2 r_f. apply ( critical_index_unfold_pred_index H2). omega.
             ++ omega.
      + unfold initial. rewrite prepend_string_begin by omega. cbn. apply I.
      + apply final_prepend. cbn. apply omega_iteration_final with (k := k1').
        * cbn. subst r_f. now apply (critical_index_unfold_distance' H1 H2).
        * cbn. unfold critical_index_unfold in H1. subst r_f. rewrite drop_correct. tauto.
   - exfalso. omega.
End PeriodicRun.

Close Scope list_scope.
Open Scope string_scope.

Lemma periodic_run_matching_pseq_size (A:finType) (aut: NFA A) (w : UPSeq A) (r: UPSeq (state aut)) : accepting (unfold r) (unfold w) ->
         exists r' w', accepting (unfold r') (unfold w') /\
                        r ==== r' /\ w ==== w' /\
                       |prefix r'| = |prefix w'| /\ |loop r'| = |loop w'|.
  intros Acc.
  exists (up_map fst (up_zip r w)), (up_map snd (up_zip r w)). split; [|repeat split].
  - apply (accepting_extensional (r := unfold r) (w:= unfold w)); auto.
    + now rewrite up_zip_proj1.
    + now rewrite up_zip_proj2.
  - now rewrite up_zip_proj1.
  - now rewrite up_zip_proj2.

Correctness of image NFA
Lemma map_aut_up_correct (X Y:finType) (f: X ->Y) (aut: NFA X) : L_A (CC:=UPSequenceStructure) (image_aut f aut) =$= LAmap f (L_A aut).

    unfold L_A, LAmap, ASeq, azip, amap. simpl. split.
    - intros [r [r' [w' [[V [I F]] [Er [Ew [Ef Es]]]]]] % periodic_run_matching_pseq_size] % periodic_run.

    assert (forall n, {x : X | f x = (unfold w' n)/\ transition (aut:=aut) (unfold r' n) x (unfold r' (S n))}) as H. {
        intros n. apply finType_cc.
        - auto.
        - apply V.
    pose (w1 := mkstring (fun n => proj1_sig (H n)) (|prefix r'|)).
    pose (w2 := mkstring (fun n => proj1_sig (H ((S (|prefix r'|))+n ))) (| loop r' |)).

    exists (mkUPSeq w1 w2). rewrite Ew. split.
       unfold up_map. rewrite !up_prefix, !up_loop.
       apply prepend_string_proper; unfold string_map, seq_map.
       - split; auto. intros n L. cbn in *. destruct H as [x [E T]]. cbn. unfold unfold in E. now rewrite prepend_string_begin in E by comega.
       - apply omega_iteration_proper.
         split; auto. intros n L. cbn in *. rewrite_eq (S (|prefix r'| +n) = S(|prefix r'|) + n). destruct H as [x [E T]]. cbn. unfold unfold in E. rewrite Ef in E. rewrite prepend_string_rest' in E.
          now rewrite omega_iter_first in E by omega.
     exists (unfold r'). repeat split; auto.
     destruct r' as [r1 r2]. simpl in Ef,Es. unfold unfold. simpl prefix. simpl loop.
     simpl in r1 , r2.
     apply (valid_prepend_path' (X:=X) (aut:=aut)); auto.
     + intros n L. subst w1. simpl. destruct (H n) as[x T]. simpl. simpl in L.
        unfold unfold in T. now rewrite 3prepend_string_begin in T by comega.
     + simpl. destruct (H (|r1|)) as [x T]. simpl.
       unfold unfold in T. rewrite 2prepend_string_begin in T by comega.
       rewrite_eq (S(|r1|) = S(|r1|)+0) in T.
       now rewrite prepend_string_rest' in T.
     + unfold omega_iteration. apply (concat_inf_is_valid'' (X:=X)).
       intros _. repeat split.
       * intros n L. subst w2. simpl seq. rewrite_eq (S(|r1| + n) = S(|r1|) + n).
         destruct (H ((S (| r1 |))+ n)) as [x [E T]].
          unfold unfold in T. simpl in L. simpl prefix in T. simpl loop in T. simpl.
          rewrite_eq (S(S (|r1|) + n) = S (|r1|) + S n) in T.
          rewrite 2prepend_string_rest' in T.
          now rewrite 2omega_iter_first in T by comega.
       * subst w2. simpl. rewrite_eq (S(|r1| + |r2|) = S(|r1|) + |r2|). destruct (H ((S (| r1 |)) + |r2|)) as [x [E T]].
         unfold unfold in T. simpl prefix in T. simpl loop in T. simpl.
         rewrite_eq (S(S (|r1|) + |r2|) = S (|r1|) + S (|r2|)) in T.
          rewrite 2prepend_string_rest' in T.
           rewrite omega_iter_first in T by auto.
           simpl. now rewrite omega_iter_first_new in T.
  - intros [w' [E [r [V [In Fin]]]]].
    exists r. repeat split; auto.
      intros n. exists (unfold w' n). split.
      + unfold aseq_equal, aseq_to_seq in E. simpl in E. rewrite up_map_correct in E. apply E.
      + apply V.

End UPAdmissible.

Definition UPStructure : AdmissibleSequenceStructure.
  apply ( mkAdmissibleSequenceStructure (CC:=UPSequenceStructure)).
  - intros A aut. unfold L_A. simpl. destruct (dec_language_empty_informative_periodic aut ) as [D|D].
    + left. destruct D as [v [w L]]. exists (mkUPSeq v w). auto.
    + right. intros vw. apply (D (unfold vw)).
  - intros A aut [v w]. exists (buechi_eq_class v), (buechi_eq_class w). simpl. unfold unfold.
    auto using in_lang_prepend, eq_classes_extensional, lang_omega_iteration_extensional, buechi_eq_class_correct, string_omega_omega_iteration.
  - intros *. apply periodic_run.
  - apply map_aut_up_correct.