Set Implicit Arguments.

Require Import Utils.
Require Import Strings.

Sequences

Abstract Sequences

To parameterise S1S over AS and UP sequences, we abstract from sequences and UP sequences and define S1S over this abstraction. By instantiating with sequences or UP sequences, we will obtain S1S with AS or UP semantics.
Abstract sequences provide a head, a tail, and a cons operation:

Class AbstractSequence := {
   Seq : Type -> Type;
   hd : forall X, Seq X -> X;
   tl : forall X, Seq X -> Seq X;
   scons: forall X, X -> Seq X -> Seq X;
   
   drop := fun (X: Type) => fix drop (sigma: Seq X) (n: nat) : Seq X := match n with | 0 => sigma| S n => drop (tl sigma) n end;
   nth := fun X (sigma: Seq X) n => hd (drop sigma n);
   seq_equiv := fun X (sigma tau: Seq X)=> forall n, nth sigma n = nth tau n;
   
   hd_correct : forall X (a:X) sigma, hd (scons a sigma) = a;
   tl_correct : forall X (a:X) sigma, seq_equiv (tl (scons a sigma)) sigma
}.

As we do not assume functional extensionality, sequence equivalence (pointwise equality) is crucial. Moreover, equivalent UP sequences are not necessarily equal. We will use setoid_rewriting for sequence equivalence massively.

Notation "a ':::' sigma" := (scons a sigma) (at level 40).
Notation "sigma == tau" := (seq_equiv sigma tau) (at level 65).

We use nth as a coercion and can write sigma nth as we would do for sequences as functions.
Coercion nth: Seq >-> Funclass.

We define basic operations that can be defined with head, tail, and cons.

Section BaseSeqOperations.

  Context (AS: AbstractSequence).
  Context (X:Type).
  Implicit Types (sigma tau : Seq X).

  Lemma nth_step_tl sigma n : (sigma) (S n) = (tl sigma) n.
  Proof. reflexivity. Qed.

  Lemma nth_first_hd sigma: sigma 0 = hd sigma.
  Proof. reflexivity. Qed.

  Lemma drop_step sigma n : drop sigma (S n) = drop (tl sigma) n.
  Proof. reflexivity. Qed.

  Lemma drop_tl sigma n: tl (drop sigma n) = drop (tl sigma) n.
  Proof.
    revert sigma; induction n; intros sigma; simpl; auto.
  Qed.

  Lemma drop_plus sigma n m : drop (drop sigma n) m = drop sigma (n + m).
  Proof.
    revert sigma. induction n; intros sigma; simpl; auto.
  Qed.

  Lemma drop_nth sigma n m: (drop sigma n) m = sigma (n + m).
  Proof.
    unfold nth. now rewrite drop_plus.
  Qed.

  Lemma drop_nth' sigma n m: (drop sigma n) m = sigma (m + n).
  Proof.
    now rewrite drop_nth, plus_comm.
  Qed.

  Fixpoint prefix sigma n := match n with
    | 0 => nil
    | S n => (hd sigma) :: (prefix (tl sigma) n) end.

  Fixpoint closed_prefix sigma n : NStr X := match n with
    | 0 => sing (hd sigma)
    | S n => ncons (hd sigma) (closed_prefix (tl sigma) n) end.

  Definition substr sigma n m := prefix (drop sigma n) (m - n).
  Definition closed_substr sigma n m := closed_prefix (drop sigma n) (m - n).

  Lemma nonempty_prefix_is_closed n sigma : prefix sigma (S n) = closed_prefix sigma n.
  Proof.
    revert sigma. induction n; intros sigma.
    - reflexivity.
    - simpl. f_equal. apply IHn.
  Qed.

  Lemma nonempty_substr_is_closed n m sigma : m <=n -> substr sigma m (S n) = closed_substr sigma m n.
  Proof.
    intros L.
    unfold closed_substr, substr. rewrite_eq (S n - m = S(n - m)).
    apply nonempty_prefix_is_closed.
  Qed.

  Lemma closed_prefix_delta n sigma : delta (closed_prefix sigma n) = n.
  Proof.
    revert sigma. induction n ; intros sigma; simpl; auto.
  Qed.

  Lemma prefix_length n sigma : length (prefix sigma n) = n.
  Proof.
    revert sigma. induction n ; intros sigma; simpl; auto.
  Qed.

  Lemma closed_substr_delta sigma n m : delta (closed_substr sigma n m) = m - n.
  Proof.
    unfold closed_substr. now rewrite closed_prefix_delta.
  Qed.

  Lemma substr_length sigma n m : length (substr sigma n m) = m - n.
  Proof.
    unfold substr. now rewrite prefix_length.
  Qed.

  Lemma closed_prefix_nth n m sigma: m <= n -> (closed_prefix sigma n) m = sigma m.
  Proof.
    intros L. revert sigma n L; induction m; intros sigma n L; simpl.
    - destruct n; auto.
    - destruct n.
      + now exfalso.
      + rewrite nth_step_tl. simpl. apply IHm. omega.
  Qed.

  Lemma nstr_concat'_step (a:X) x y : nstr_concat' (ncons a x) y = ncons a (nstr_concat' x y).
  Proof. reflexivity. Qed.

  Lemma closed_prefix_step sigma n : closed_prefix sigma (S n) = ncons (hd sigma) (closed_prefix (tl sigma) n).
  Proof. reflexivity. Qed.

  Lemma closed_prefix_plus n m sigma : closed_prefix sigma (S (n + m)) = nstr_concat' (closed_prefix sigma n) (closed_prefix (drop sigma (S n)) m).
  Proof.
    revert sigma m. induction n; intros sigma m.
    - reflexivity.
    - setoid_rewrite closed_prefix_step at 1 2 3.
      rewrite drop_step, nstr_concat'_step. now rewrite <-IHn.
  Qed.

  Lemma prefix_nth {D: Dummy X} n m sigma: m < n -> str_nth (prefix sigma n) m = sigma m.
  Proof.
    intros L. revert sigma n L; induction m; intros sigma n L; simpl.
    - destruct n; auto.
    - destruct n.
      + now exfalso.
      + rewrite nth_step_tl. simpl. apply IHm. omega.
  Qed.

  Lemma closed_substr_nth sigma n m k : k <= m - n -> (closed_substr sigma n m) k = sigma (k + n).
  Proof.
    intros L. unfold closed_substr.
    rewrite closed_prefix_nth by assumption.
    now rewrite drop_nth'.
  Qed.

  Lemma closed_substr_nth' sigma n m k : k <= m - n -> (closed_substr sigma n m) k = sigma (n + k).
  Proof.
    intros L. now rewrite closed_substr_nth, plus_comm by assumption.
  Qed.

  Lemma closed_substr_begin sigma n: closed_substr sigma 0 n = closed_prefix sigma n.
  Proof.
    unfold closed_substr. simpl. f_equal. omega.
  Qed.

  Lemma closed_substr_step sigma n m: closed_substr (tl sigma) n m = closed_substr sigma (S n) (S m).
  Proof. reflexivity. Qed.

  Lemma closed_substr_step_last sigma n m : n <= m -> closed_substr sigma n (S m) = nstr_concat' (closed_substr sigma n m) (sing (sigma (S m))).
  Proof.
    revert sigma m. induction n; intros sigma m L.
    - unfold closed_substr. simpl. revert sigma. induction L; intros sigma.
      + simpl. reflexivity.
      + simpl. f_equal. rewrite (IHL (tl sigma)). f_equal. f_equal. omega.
    - destruct L; rewrite <-2closed_substr_step, IHn by auto; reflexivity.
  Qed.

  Lemma closed_substr_shift sigma n m k: closed_substr (drop sigma k) n m = closed_substr sigma (k + n) (k + m).
  Proof.
    revert sigma. unfold closed_substr. induction k; intros sigma; simpl; auto.
  Qed.

  Lemma closed_substr_singleton sigma n: closed_substr sigma n n = sing (sigma n).
  Proof.
    unfold closed_substr. rewrite Nat.sub_diag. simpl. now rewrite <-nth_first_hd, drop_nth'.
  Qed.

  Lemma substr_nth {D:Dummy X} sigma n m k : k < m - n -> str_nth (substr sigma n m) k = sigma (k + n).
  Proof.
    intros L. unfold substr.
    rewrite prefix_nth by assumption.
    now rewrite drop_nth'.
  Qed.

  Lemma closed_substr_nstr_drop sigma n m : n <= m -> closed_substr sigma n m = nstr_drop (closed_prefix sigma m) n.
  Proof.
     unfold closed_substr. revert sigma n. induction m; intros sigma [|n]; simpl; auto.
  Qed.

  Fixpoint prepend x sigma := match x with
    | nil => sigma
    | a::x => a ::: (prepend x sigma) end.
  Notation "x +++ sigma" := (prepend x sigma) (at level 60).

From abstract sequences one can obtain dummy values.

  Global Instance SeqDummy : Seq X -> Dummy X.
  Proof.
    intros sigma. exact (hd sigma).
  Qed.

  Global Instance SeqNStrDummy : Seq (NStr X) -> Dummy X.
  Proof.
    intros sigma. exact (hd sigma 0).
  Qed.


  Global Instance seq_equiv_equiv : Equivalence (@seq_equiv _ X).
  Proof.
    repeat split.
    - intros sigma tau E n. now rewrite E.
    - intros sigma_1 sigma_2 sigma_3 E1 E2 n. now rewrite E1, E2.
  Qed.

  Definition substr' (sigma: Seq X) i j := closed_substr sigma i (pred j).

   Global Instance hd_proper : Proper (@seq_equiv _ _ ==> eq) (@hd _ X).
  Proof.
    intros sigma tau E. apply (E 0).
  Qed.

  Global Instance tl_proper : Proper (@seq_equiv _ _ ==> @seq_equiv _ _) (@tl _ X).
  Proof.
    intros sigma tau E n. apply (E (S n)).
  Qed.

  Global Instance drop_proper : Proper (@seq_equiv _ _ ==> eq ==> @seq_equiv _ _ ) (@drop _ X) .
  Proof.
    intros sigma tau E n m <-. revert sigma tau E. induction n; intros sigma tau E.
    - assumption.
    - simpl. apply IHn. now rewrite E.
  Qed.

  Global Instance nth_proper : Proper (@seq_equiv _ _ ==> eq ==> eq) (@nth _ X).
  Proof.
    intros sigma tau E n m <-. unfold nth. now rewrite E.
  Qed.



  Global Instance prefix_proper : Proper (@seq_equiv _ _==> eq ==> eq) prefix.
  Proof.
    intros sigma tau E n m <-. revert sigma tau E. induction n; intros sigma tau E.
    - reflexivity.
    - simpl. f_equal.
      + now rewrite E.
      + apply IHn. now rewrite E.
  Qed.

  Global Instance closed_prefix_proper: Proper (@seq_equiv _ _ ==> eq ==> eq) closed_prefix.
  Proof.
    intros sigma tau E n m <-. revert sigma tau E. induction n; intros sigma tau E; simpl.
    - f_equal. now rewrite E.
    - rewrite (hd_proper E). f_equal. apply IHn. now rewrite E.
  Qed.

  Global Instance closed_substr_proper: Proper (@seq_equiv _ _ ==> eq ==> eq ==> eq) closed_substr.
  Proof.
    intros sigma tau E n m <- i j <-.
    unfold closed_substr. now rewrite E.
  Qed.

  Global Instance substr_proper: Proper (@seq_equiv _ _ ==> eq ==> eq ==> eq) substr.
  Proof.
    intros sigma tau E n m <- i j <-.
    unfold substr. now rewrite E.
  Qed.

  Global Instance substr'_proper: Proper (@seq_equiv _ _==> eq ==> eq ==> eq) substr'.
  Proof.
    intros sigma tau E n n' <- m m' <-. unfold substr'. now rewrite E.
  Qed.

  Lemma substr'_delta (sigma: Seq X) i j : i < j -> delta (substr' sigma i j) = pred (j - i).
  Proof.
    intros L. unfold substr'. rewrite closed_substr_delta. omega.
  Qed.

  Lemma substr'_nth (sigma: Seq X) i j n : i < j -> n < j - i -> (substr' sigma i j) n = sigma (n + i).
  Proof.
    intros L1 L2. unfold substr'. rewrite closed_substr_nth; auto.
  Qed.

  Global Instance scons_proper: Proper (eq ==> @seq_equiv _ _ ==> @seq_equiv _ _) (@scons _ X).
  Proof.
    intros a b <- sigma tau E n. unfold nth.
    destruct n; simpl.
    - now rewrite 2hd_correct.
    - now rewrite 2tl_correct, E.
  Qed.

  Global Instance prepend_proper: Proper (eq ==> @seq_equiv _ _ ==> @seq_equiv _ _) prepend .
  Proof.
    intros x y <- sigma tau E. induction x.
    - assumption.
    - simpl. now rewrite IHx.
  Qed.

  Lemma scons_correct sigma: sigma == (hd sigma) ::: (tl sigma).
  Proof.
    intros n. unfold nth. destruct n; simpl.
    - now rewrite hd_correct.
    - now rewrite tl_correct.
  Qed.

  Lemma nth_first sigma a : (a ::: sigma) 0 = a.
  Proof.
    unfold nth. simpl. now rewrite hd_correct.
  Qed.

  Lemma nth_step sigma a n : (a ::: sigma) (S n) = sigma n.
  Proof.
    unfold nth. simpl. now rewrite tl_correct.
  Qed.


  Hint Immediate SeqDummy : typeclass_instances.
  Lemma prepend_nth_first (x: Str X) sigma n : n < |x| -> (x +++ sigma) n = str_nth x n.
  Proof.
    intros L. revert n L. induction x; intros n L.
    - now exfalso.
    - destruct n.
      + simpl. now rewrite nth_first.
      + simpl. rewrite nth_step. apply IHx. simpl in L. omega.
  Qed.

  Lemma prepend_nstr_nth_first (x:NStr X) sigma n : n <= delta x -> (x +++ sigma) n = x n.
  Proof.
    intros L. rewrite prepend_nth_first.
    - now rewrite str_nth_nstr.
    - rewrite <-nstr_to_str_length. omega.
  Qed.

  Lemma prepend_nth_rest (x: Str X) (sigma: Seq X) n : (x +++ sigma) (length x + n) = sigma n.
  Proof.
    induction x.
    - reflexivity.
    - simpl. now rewrite nth_step.
  Qed.

  Lemma prepend_nth_rest_sub (x: Str X) (sigma: Seq X) n: |x| <= n -> (x +++ sigma) n = sigma (n - |x|).
  Proof.
    revert n. induction x; simpl; intros [|n] L; simpl; auto.
    rewrite nth_step. auto.
  Qed.

  Lemma prepend_nstr_nth_rest (x: NStr X) (sigma: Seq X) n : (x +++ sigma) (S(delta x) + n) = sigma n.
  Proof.
    now rewrite nstr_to_str_length, prepend_nth_rest.
  Qed.

  Lemma prepend_nth_rest' (x: Str X) (sigma: Seq X) n : (x +++ sigma) (n + length x) = sigma n.
  Proof.
    now rewrite plus_comm, prepend_nth_rest.
  Qed.

  Lemma prepend_nstr_nth_rest_sub (x: NStr X) (sigma: Seq X) n : delta x < n -> (x +++ sigma) n = sigma (n - S (delta x)).
  Proof.
    revert n. induction x; simpl; intros [|n] L; simpl.
    - now exfalso.
    - rewrite nth_step. f_equal. omega.
    - now exfalso.
    - now rewrite nth_step, IHx by omega.
  Qed.

  Lemma prepend_nstr_assoc (x y : NStr X) (sigma: Seq X): x +++ (y +++ sigma) == (nstr_concat' x y) +++ sigma.
  Proof.
    induction x.
    - reflexivity.
    - simpl. apply scons_proper; auto.
  Qed.

  Lemma prepend_nstr_first (x:NStr X) (sigma : Seq X): (x +++ sigma) 0 = x 0.
  Proof.
    destruct x; simpl; now rewrite nth_first.
  Qed.

  Lemma revert_prepend (x: Str X) (sigma : Seq X) : drop (x +++ sigma) (length x) == sigma.
  Proof.
    induction x.
    - reflexivity.
    - simpl. now rewrite tl_correct.
  Qed.

  Lemma revert_nstr_prepend (x: NStr X) (sigma : Seq X) : drop (x +++ sigma) (S(delta x)) == sigma.
  Proof.
    induction x.
    - simpl. now rewrite tl_correct.
    - simpl. now rewrite tl_correct, IHx.
  Qed.

  Lemma revert_drop (sigma: Seq X) n: sigma == (prefix sigma n) +++ (drop sigma n).
  Proof.
    revert sigma; induction n; intros sigma.
    - reflexivity.
    - simpl. setoid_rewrite scons_correct at 1. apply scons_proper; auto.
  Qed.

  Lemma closed_prefix_eq (x: NStr X) (sigma :Seq X) : closed_prefix (x +++ sigma) (delta x) = x.
  Proof.
    induction x as [|a x].
    - simpl. now rewrite hd_correct.
    - simpl. rewrite hd_correct. f_equal.
      now rewrite tl_correct.
  Qed.

  Lemma closed_substr_prepend (x: NStr X) tau i : i <= delta x ->
         closed_substr (x +++ tau) i (delta x) = nstr_drop x i.
  Proof.
    revert i. induction x; intros i H.
    - simpl in H. destruct i; try (now exfalso).
      cbn. now rewrite hd_correct.
    - destruct i.
      + now rewrite closed_substr_begin, closed_prefix_eq.
      + simpl. unfold closed_substr. rewrite drop_step, tl_correct.
        unfold closed_substr in IHx. simpl. apply IHx. simpl in H. omega.
  Qed.

  Lemma substr'_prepend' ( sigma: Seq X) x i j : i < j -> substr' (x +++ sigma) (|x| + i) (|x|+ j) = substr' sigma i j.
  Proof.
    intros L1.
    unfold substr'.
    setoid_rewrite <-(revert_prepend x sigma) at 2.
    rewrite closed_substr_shift.
    f_equal; omega.
  Qed.

  Lemma substr'_split (sigma: Seq X) i j k : i < j < k -> substr' sigma i k = nstr_concat' (substr' sigma i j) (substr' sigma j k).
  Proof.
    intros L.
    unfold substr', closed_substr.
    remember (k - j - 1) as m. assert (k = S (j + m)) by omega. subst k. simpl.
    remember (j - i - 1) as n. assert (j = S (i + n)) by omega. subst j.
    rewrite_eq (S (i + n) + m - i = S (n + m)).
    rewrite closed_prefix_plus. f_equal.
    - f_equal. omega.
    - rewrite drop_plus. f_equal.
      + f_equal. omega.
      + omega.
  Qed.


End BaseSeqOperations.

Arguments SeqDummy {_} {_}.
Hint Immediate SeqDummy : typeclass_instances.

Arguments SeqNStrDummy {_} {_}.
Hint Immediate SeqNStrDummy : typeclass_instances.

Notation "x +++ sigma" := (prepend x sigma) (at level 60).

Abstract Sequences with More Operations

For minimal S1S abstract sequences suffices, but to formalise the reduction from full S1S to minimal S1S we need more operations on abstract sequences, that cannot be defined only with head, tail, and cons:
  • a const operation yielding a constant abstract sequences
  • a map operation
  • a zip operation
We split const from map and zip to be precisly define when which operations are required but in prinicple one could group them.

Constant Sequence


Class WithConst (SS: AbstractSequence) := {
    const : forall X, X -> Seq X;
    const_correct : forall X (x:X), const x == x ::: const x
}.

Section WithConstLemmas.
  Context {SS: AbstractSequence}.
  Context {WC: WithConst SS}.

  Lemma const_nth X (a: X) n : const a n = a.
  Proof.
    induction n; rewrite const_correct.
    - now rewrite nth_first.
    - now rewrite nth_step.
  Qed.

End WithConstLemmas.

Map and Zip


Class WithZipMap (SS: AbstractSequence) := {
    map : forall X Y, (X -> Y) -> Seq X -> Seq Y;
    zip : forall X Y, Seq X -> Seq Y -> Seq (X * Y);
    map_correct : forall X Y (f: X-> Y) sigma, map f sigma == (f (hd sigma)):::(map f (tl sigma));
    zip_correct : forall X Y (sigma:Seq X) (tau:Seq Y), zip sigma tau == (hd sigma, hd tau) ::: (zip (tl sigma) (tl tau))
}.

Section WithZipMapLemmas.
  Context {SS: AbstractSequence}.
  Context {WZM : WithZipMap SS}.

  Global Instance map_proper X Y: Proper (eq ==> @seq_equiv _ X ==> @seq_equiv _ Y) (@map _ _ X Y).
  Proof.
    intros f g <- sigma tau E n. revert sigma tau E.
    induction n; intros sigma tau E; setoid_rewrite map_correct at 1 2.
    - rewrite 2nth_first. now rewrite E.
    - rewrite 2nth_step. apply IHn. now rewrite E.
  Qed.

  Global Instance zip_proper X Y : Proper (@seq_equiv _ X ==> @seq_equiv _ Y ==> @seq_equiv _ (X*Y)) (@zip _ _ X Y).
  Proof.
    intros sigma_1 sigma_2 E_1 tau_1 tau_2 E_2 n. revert sigma_1 sigma_2 E_1 tau_1 tau_2 E_2.
    induction n; intros sigma_1 sigma_2 E_1 tau_1 tau_2 E_2; setoid_rewrite zip_correct at 1 2.
    - rewrite 2nth_first. f_equal; now apply hd_proper.
    - rewrite 2nth_step. apply IHn; now apply tl_proper.
  Qed.

  Lemma zip_nth X Y (sigma: Seq X)(tau: Seq Y) n : zip sigma tau n = (sigma n, tau n).
  Proof.
    revert sigma tau; induction n; intros sigma tau; setoid_rewrite zip_correct at 1 2; simpl.
    - now rewrite nth_first.
    - rewrite nth_step. rewrite 2 nth_step_tl. apply IHn.
  Qed.

  Lemma zip_drop X Y (sigma: Seq X) (tau: Seq Y) n : drop (zip sigma tau) n == zip (drop sigma n) (drop tau n).
  Proof.
    intros m. now rewrite zip_nth, !drop_nth, !zip_nth.
  Qed.

  Lemma map_nth X Y (f: X -> Y) sigma n: map f sigma n = f (sigma n).
  Proof.
    revert sigma; induction n; intros sigma; setoid_rewrite map_correct at 1 2; simpl.
    - now rewrite nth_first.
    - rewrite nth_step. rewrite nth_step_tl. apply IHn.
  Qed.

  Lemma zip_map_fst X Y (sigma: Seq X) (tau : Seq Y) : map fst (zip sigma tau) == sigma.
  Proof.
    intros n. now rewrite map_nth, zip_nth.
  Qed.

  Lemma map_nstr_prepend X Y (f: X -> Y) sigma (x:NStr X) : map f (x +++ sigma) == nstr_map f x +++ map f sigma.
  Proof.
    induction x.
    - simpl. now rewrite map_correct, hd_correct, tl_correct.
    - simpl. now rewrite map_correct, hd_correct, tl_correct, IHx.
  Qed.

  Lemma drop_map X Y (sigma: Seq X) (f: X -> Y) n : drop (map f sigma) n == map f (drop sigma n).
  Proof.
    intros m. now rewrite drop_nth, 2map_nth, drop_nth.
  Qed.

  Lemma closed_prefix_map (X Y : Type) (f: X -> Y) sigma n : closed_prefix (map f sigma) n = nstr_map f (closed_prefix sigma n).
  Proof.
    revert sigma. induction n; intros sigma; cbn; rewrite map_correct, hd_correct; auto.
    f_equal. rewrite tl_correct. apply IHn.
  Qed.


Zipping Finitely many Abstract Sequences

For simplicity we assume a const function here that allows use to produce sequences from a single element. This is useful for recursively zipping a list os sequences if the list itself is empty.

  Section BigZip.

    Context {WC: WithConst SS}.

    Context{X:finType}{Y:finType}.
    Implicit Types (x:X)(y:Y)(L:list Y).

    Definition zipFinTypes y L: (X * X^^L) -> X^^(y::L).
    Proof.
      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.
    Defined.

    Fixpoint bigzip' L (f: (finType_fromList L)-> Seq X) {struct L}: Seq (X^^L).
    Proof.
      destruct L as [| y L].
      - apply const. apply vectorise. intros [x P]. exfalso. now apply pure_equiv in P.
      - apply (map (@zipFinTypes y L)).
        apply zip.
        + 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.
    Defined.

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

    Definition bigzip (f: Y -> Seq X): (Seq (X^Y)).
    Proof.
      apply (map elemToFinType). apply bigzip'.
      intros [i _]. exact (f i).
    Defined.

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

    Lemma bigzip_correct (f : Y -> Seq X) y n: applyVect ((bigzip f) n) y = (f y) n.
    Proof.
      unfold bigzip. rewrite map_nth. unfold elemToFinType.
      now rewrite apply_vectorise_inverse, bigzip_correct'.
    Qed.

    Definition bigpi : Seq (X^Y) -> Y -> Seq X.
    Proof.
      intros w i.
      apply (map (fun v => applyVect v i)). exact w.
    Defined.

    Lemma bigpi_correct (w: Seq (X^Y)) y n : (bigpi w y) n = applyVect (w n) y.
    Proof.
      unfold bigpi. now rewrite map_nth.
    Qed.

    Global Instance bigpi_proper: Proper (@seq_equiv _ (X^Y) ==> eq ==> @seq_equiv _ X) bigpi.
    Proof.
      intros sigma tau E x y <- n.
      now rewrite 2bigpi_correct, E.
    Qed.

    Lemma bigpi_bigzip_inv (f : Y -> Seq X) y :f y == (bigpi (bigzip f)) y.
    Proof.
      intros n. now rewrite bigpi_correct, bigzip_correct.
    Qed.

  End BigZip.

End WithZipMapLemmas.

Sequences nat -> X

Apart from the semantics of S1S, we are only interested in sequences as functions nat -> X but we want to be able to reuse the lemmas from abstract sequences. Note that the nth operation is different from just applying a function nat -> X to some arguments. Furthermore directly using functions nat -> X yields unintended reduction behavior, problems with setoid rewriting with sequence equivalence, and sometimes make inductive proofs more complicated and one tends to get in trouble with arithmetic.
Hence we wrap functions nat -> X in a structure such that sigma n will use the nth coercion definied on abstract sequences.
Sequences will be registered as default instance of abstract sequence. Unless one really needs pure UP sequences, sequences are used by default and one can make use all following operations.

Section Sequences.

Wrapping a function. The only use of this is that for sigma:WSeq X the expression sigma n is ill-typed and Coq will (after declaring WSeq an instance) use the nth coercion.
Structure WSeq X := wrp { unwrp : nat -> X}.

Global Instance Sequence : AbstractSequence := {|
   hd := fun X (sigma : WSeq X ) => unwrp sigma 0;
   tl := fun X (sigma : WSeq X ) => wrp (fun n => unwrp sigma (S n));
   scons := fun X (x:X) (sigma : WSeq X) => wrp (fun n => match n with
                                               | 0 => x
                                               | S n => unwrp sigma n end) |}.
Proof.
- now intros X a sigma.
- intros X a sigma n. revert sigma. induction n; intros sigma; cbn; auto.
Defined.

Lemma seq_nth (X: Type) (sigma : Seq X) n : sigma n = unwrp sigma n.
Proof.
  unfold nth. cbn.
  revert sigma. induction n; intros sigma; simpl; auto.
  rewrite IHn. reflexivity.
Qed.

Global Instance SequenceWithConst : WithConst Sequence := {|
  const := fun X (x:X) => wrp (fun n => x) : @Seq Sequence X
|}.
Proof.
- intros X x n. rewrite !seq_nth. now destruct n.
Defined.

Global Instance SequenceWithZipMap: WithZipMap Sequence := {|
  map := fun X Y (f: X -> Y) (sigma : @Seq Sequence X) => wrp (fun n => f (unwrp sigma n));
  zip := fun X Y (sigma : @Seq Sequence X) (tau: Seq Y) => wrp (fun n => (unwrp sigma n, unwrp tau n));
|}.
Proof.
- intros X Y f sigma n. rewrite !seq_nth. now destruct n.
- intros X Y sigma tau n. rewrite !seq_nth. now destruct n.
Defined.

End Sequences.

Nothing should reduce with simpl or cbn as we do not want to see the definition but only use the lemmas specifing the functions.
Global Arguments map : simpl never.
Global Arguments hd: simpl never.
Global Arguments tl: simpl never.
Global Arguments nth: simpl never.
Global Arguments scons: simpl never.
Global Arguments zip: simpl never.
Global Arguments const: simpl never.
Global Arguments Seq: simpl never.

More Operations on Sequences

Section MoreSequences.

We give another wrap function. The difference between wrap and wrp is that wrap has result type @Seq Sequence and not WSeq with wrp has. Always use wrap.

  Definition wrap (X:Type) (f: nat-> X) : Seq X := wrp f.
  Lemma wrap_correct (X:Type) (f: nat -> X) n : wrap f n = f n.
  Proof.
    now rewrite seq_nth.
  Qed.
  Global Arguments wrap: simpl never.

Flattening a Sequence of Nonempty Strings

Given a sequence of nonempty strings, we define the infinite concatenation (or flatting) of this sequence. We first give the definition on nat -> X and then wrap it to Seq and give a hint to never unfold it. This will be the common scheme for writing functions os sequences.

  Fixpoint seq_flatten (X: Type) (sigma: Seq (NStr X)) (n: nat) :=
    match n with
    | 0 => hd sigma 0
    | S n=> match (hd sigma) with
          | sing a => seq_flatten (tl sigma) n
          | ncons a y => seq_flatten (scons y (tl sigma)) n
        end
  end.

  Definition flatten (X: Type) (sigma : Seq (NStr X)) := wrap (seq_flatten sigma).
  Global Arguments flatten : simpl never.

  Lemma flatten_step X (sigma: Seq (NStr X)):
                          flatten sigma == match (hd sigma) with
                             | sing a => a ::: (flatten (tl sigma))
                             | ncons a x => a ::: (flatten (x ::: tl sigma)) end.
  Proof.
    unfold flatten. intros n. rewrite wrap_correct.
    now destruct n; cbn; destruct (hd sigma); rewrite ?nth_step, ?nth_first, ?wrap_correct.
  Qed.

  Global Instance flatten_proper X : Proper (@seq_equiv _ (NStr X) ==> @seq_equiv _ X) (@flatten X).
  Proof.
    intros sigma tau E.
    intros n. revert sigma tau E. induction n; intros sigma tau E;
      setoid_rewrite flatten_step at 1 2; rewrite E.
    - destruct (hd tau) as [a | a x]; now rewrite 2nth_first.
    - destruct (hd tau) as [a | a x]; rewrite 2nth_step; apply IHn; now rewrite E.
  Qed.

  Lemma flatten_correct (X:Type) (sigma: Seq (NStr X)): flatten sigma == hd sigma +++ flatten (tl sigma).
  Proof.
    rewrite (scons_correct sigma) at 1.
    generalize (tl sigma) as tau. generalize (hd sigma) as x.
    intros x. induction x; intros tau.
    - now rewrite flatten_step, hd_correct, tl_correct.
    - now rewrite flatten_step, hd_correct, tl_correct, IHx.
  Qed.

  Lemma flatten_prepend X (x: NStr X) sigma : x +++ flatten sigma == flatten (sing x +++ sigma).
  Proof.
    simpl. symmetry. now rewrite flatten_correct, hd_correct, tl_correct.
  Qed.

  Lemma flatten_map X Y (f : X -> Y) sigma : map f (flatten sigma) == flatten (map (nstr_map f) sigma).
  Proof.
    intros n. revert sigma. induction n; intros sigma.
    - setoid_rewrite flatten_step at 1 2.
      setoid_rewrite map_correct at 1 2.
      rewrite hd_correct. destruct (hd sigma) as [a | a x]; simpl; now rewrite hd_correct, 2nth_first.
    - setoid_rewrite flatten_step at 1 2.
      setoid_rewrite map_correct at 1 2.
      rewrite hd_correct. destruct (hd sigma) as [a | a x]; simpl; rewrite tl_correct,2nth_step.
      + setoid_rewrite map_correct at 2. rewrite tl_correct. apply IHn.
      + rewrite IHn. setoid_rewrite map_correct at 1. rewrite tl_correct, hd_correct.
        setoid_rewrite map_correct at 2. now rewrite tl_correct.
  Qed.



Sequences Satisfying a Predicate Infinitely Often

A sequence satisfies a predicate p infinitely often, if there are infinitely many positions where p holds. We declare it a class to automatically derive proofs in simple situations.


  Class inf_often (X: Type) (P: X -> Prop) (sigma: Seq X) := Inf : forall n, exists m, n <= m /\ P (sigma m).

  Global Instance inf_often_tl (X:Type) (P: X -> Prop) sigma : inf_often P sigma -> inf_often P (tl sigma).
  Proof.
    intros H n. destruct (H (S n)) as [m [L Q]].
    exists (pred m). split.
    - omega.
    - destruct m; auto. exfalso. omega.
  Qed.

  Global Instance inf_often_drop (X:Type) (P: X -> Prop) sigma n: inf_often P sigma -> inf_often P (drop sigma n).
  Proof.
    induction n; intros H; simpl; auto.
    rewrite <-drop_tl. apply inf_often_tl. now apply IHn.
  Qed.

  Section InfOften.
    Context {X Y: Type}.
    Variable (P : X -> Prop) (P2: Y ->Prop).

    Lemma inf_often_cons a sigma : inf_often P sigma <-> inf_often P (a ::: sigma).
    Proof.
      split.
      - intros H n. destruct (H n) as [m [L Q]].
        exists (S m). split; auto.
        now rewrite nth_step.
      - intros H n. destruct (H (S n)) as [m [L Q]].
        destruct m.
        + now exfalso.
        + exists m. rewrite nth_step in Q. split; auto.
    Qed.

    Global Instance inf_often_cons_instance a sigma : inf_often P sigma -> inf_often P (a ::: sigma).
    Proof. apply inf_often_cons. Qed.

    Lemma inf_often_prepend x sigma: inf_often P sigma <-> inf_often P (prepend x sigma).
    Proof.
      split; induction x; simpl; intros H; simpl; auto.
      apply IHx. apply <-inf_often_cons. apply H.
    Qed.

    Global Instance inf_often_prepend_instance x sigma: inf_often P sigma -> inf_often P (prepend x sigma).
    Proof. apply inf_often_prepend. Qed.


    Global Instance inf_often_proper X (P: X -> Prop) : Proper (@seq_equiv _ X ==> iff) (@inf_often X P).
    Proof.
      intros sigma tau E. split; intros Inf n; destruct (Inf n) as [m [L Q]]; exists m; split; auto; [rewrite <-E | rewrite E]; trivial.
    Qed.

    Global Instance inf_often_flatten_tl sigma: inf_often P (flatten sigma) -> inf_often P (flatten (tl sigma)).
    Proof.
      intros H.
      rewrite flatten_correct in H.
      rewrite <-revert_prepend with (x:= hd sigma). auto.
    Qed.

A predicate holds in infinitely many strings in a sequence of nonempty strings if and only if it holds infinitely often in the flattend sequence.

    Definition once (x: NStr X) := exists n, n <= delta x /\ P ( x n).

    Lemma inf_often_flatten sigma : inf_often once sigma <-> inf_often P (flatten sigma).
    Proof.
      split.
      - intros H n.
        destruct (H n) as [m [ Q1 [k [L Q2]]]].
        remember (m - n) as j. assert (m = j + n) as H2 by omega. subst m. clear Heqj Q1.

        revert sigma H L Q2. induction j; intros sigma H L Q2.
        + simpl in *. revert sigma H L Q2. induction n; intros sigma H L Q2.
          * exists k. split; auto.
            rewrite nth_first_hd in L, Q2.
            now rewrite flatten_correct, prepend_nstr_nth_first.
          * specialize (IHn (tl sigma)).
            destruct IHn as [m [Q3 Q4]]; auto.
            exists (S(delta (hd sigma)) + m). split; auto.
             now rewrite flatten_correct, prepend_nstr_nth_rest.
        + specialize (IHj (tl sigma)).
          destruct IHj as [m [Q3 Q4]]; auto.
          exists (S (delta (hd sigma)) + m). split; auto.
          now rewrite flatten_correct, prepend_nstr_nth_rest.
      - intros H n.
        revert sigma H. induction n; intros sigma H.
        + destruct (H 0) as [m [Q1 Q2]]. clear Q1. revert sigma H Q2. induction m; intros sigma H Q2.
          * exists 0. split; auto. exists 0. split; auto.
          * rewrite flatten_step in Q2. destruct hd as [a | a x] eqn:E; simpl in P; rewrite nth_step in Q2.
            -- destruct (IHm (tl sigma)) as [j [Q3 Q4]]; auto.
               exists (S j). split; auto.
            -- destruct (IHm (x ::: tl sigma)) as [[|j] [Q3 [i [L Q4]]]]; auto.
               ++ rewrite flatten_correct, tl_correct. auto.
               ++ exists 0. split; auto. exists (S i). split.
                  ** rewrite nth_first_hd, E. simpl.
                     rewrite nth_first in L. omega.
                  ** rewrite nth_first_hd, E. now rewrite nth_first in Q4.
               ++ exists (S j). split; auto. exists i. split.
                  ** now rewrite nth_step in L.
                  ** rewrite nth_step_tl. now rewrite nth_step in Q4.
        + destruct (H (S(delta (hd sigma)) + n)) as [m [Q1 Q2]].
          destruct (IHn (tl sigma)) as [k [Q3 Q4]]; auto.
          exists (S k). split; auto.
    Qed.

    Lemma inf_often_map (f: X -> Y) sigma: (forall x, P x -> P2 (f x)) -> inf_often P sigma -> inf_often P2 (map f sigma).
    Proof.
      intros E Inf n.
      destruct (Inf n) as [m [Q1 Q2]]. exists m. split; auto.
      rewrite map_nth. now apply E.
    Qed.


  End InfOften.




Factorizing a Sequence by a Predicate that Holds Infinitely Often

We cut a sequence into a sequence of nonempty strings given a decidable predicates that holds infinitely often in this sequence, such that it holds exactly at the begin of all nonempty strings in the resulting sequence.


  Fixpoint seq_factorize (X: Type) (P: X -> Prop) {Dec:forall x, dec (P x)} sigma {Inf:inf_often P sigma} (n: nat) : NStr X.
  Proof.
    destruct n.
    - exact (closed_prefix sigma (cc_nat_first_geq_exists (Inf 0))).
    - apply (seq_factorize) with (P:=P) (sigma:= drop sigma (S (cc_nat_first_geq_exists (Inf 0)))); [auto | auto |].
      exact n.
  Defined.

  Definition factorize X (P: X -> Prop) {Dec:forall x, dec (P x)} sigma {Inf:inf_often P sigma} := wrap (seq_factorize (Inf:= Inf)).
  Global Arguments factorize {X} P {Dec} sigma {Inf} : rename, simpl never.

  Lemma factorize_correct X (sigma: Seq X) (P: X -> Prop) {Dec:forall x, dec (P x)} (H:inf_often P sigma):
      factorize P sigma == closed_prefix sigma (cc_nat_first_geq_exists (H 0)) ::: factorize P (drop sigma (S (cc_nat_first_geq_exists (H 0)))).
  Proof.
    unfold factorize. intros [|n]; rewrite wrap_correct; cbn.
    - now rewrite nth_first.
    - now rewrite nth_step, wrap_correct.
  Qed.


  Section Factorize.

    Context {X: Type}.
    Variable (P: X -> Prop).
    Context {Dec: forall x, dec (P x)}.

    Implicit Type (sigma : Seq X).


    Lemma factorize_proper (sigma tau: Seq X) (H1: inf_often P sigma)(H2: inf_often P tau) (E: sigma == tau):
       factorize P sigma == factorize P tau (Inf:= H2).
    Proof.
      intros n.
      revert sigma tau H1 H2 E. induction n; intros sigma tau H1 H2 E; setoid_rewrite factorize_correct.
      - rewrite 2nth_first. apply closed_prefix_proper. apply E.
        apply cc_nat_first_geq_exists_extensional, E.
      - rewrite 2nth_step. apply IHn. apply drop_proper; auto.
        f_equal. apply cc_nat_first_geq_exists_extensional, E.
    Qed.

    Lemma flatten_factorize_inv (sigma: Seq X) (H: inf_often P sigma) : flatten (factorize P sigma) == sigma.
    Proof.
      enough (forall m, (prefix sigma m) +++ flatten (factorize P (drop sigma m) ) == sigma) as Q.
      - specialize (Q 0). cbn in Q. rewrite factorize_proper. apply Q. reflexivity.
      - intros m n. revert m sigma H. induction n; intros m sigma H.
        + destruct m.
          * cbn. rewrite factorize_correct, flatten_correct, hd_correct, prepend_nstr_first, closed_prefix_nth; auto.
          * cbn. now rewrite nth_first.
        + destruct m.
          * cbn. rewrite factorize_correct, flatten_correct, hd_correct, tl_correct, <-nonempty_prefix_is_closed. cbn.
            rewrite nth_step. rewrite factorize_proper. rewrite IHn. reflexivity. reflexivity.
          * cbn. rewrite nth_step. rewrite factorize_proper, IHn. reflexivity. reflexivity.
    Qed.


  End Factorize.


ω-Iteration

The ω-iteration of a nonempty string x is just defined as the flattening of the sequence that is constant x. We establish some lemmas for ω-iteration that are useful for manipulating UP sequences later.

  Section OmegaIteration.

    Context {X: Type}.
    Implicit Types (x y : NStr X).

    Definition omega_iter x := flatten (const x).

    Lemma omega_iter_correct x : omega_iter x == x +++ omega_iter x.
    Proof.
      unfold omega_iter.
      rewrite const_correct at 1. rewrite flatten_correct at 1.
      now rewrite hd_correct, tl_correct.
    Qed.

    Lemma nstr_concat_swap x b y: nstr_concat' x (ncons b y) = nstr_concat' (nstr_concat' x (sing b)) y.
    Proof.
      revert b y. induction x as [a|a x]; simpl; intros b [c |c y]; simpl; auto; f_equal; auto.
    Qed.

    Lemma nstr_concat_sing b y: ncons b y = nstr_concat' (sing b) y.
    Proof. reflexivity. Qed.

    Lemma nstr_concat_assoc x y z: nstr_concat' x (nstr_concat' y z) = nstr_concat' (nstr_concat' x y) z.
    Proof.
      revert y z. induction x as [a|a x]; intros y z; simpl; f_equal; auto.
    Qed.

    Lemma flatten_rotate x y: flatten (x ::: const (nstr_concat' y x)) == flatten (const (nstr_concat' x y)).
    Proof.
      intros n. revert y x. induction n; intros y x;
      rewrite !flatten_step, !hd_correct; setoid_rewrite const_correct at 1; rewrite hd_correct.
      - destruct x as [b | b x]; simpl; now rewrite !nth_first.
      - destruct x as [b | b x]; simpl; rewrite !nth_step, tl_correct;
        setoid_rewrite const_correct at 2; rewrite tl_correct.
        + now rewrite <-IHn.
        + now rewrite nstr_concat_swap, nstr_concat_sing, 2IHn, nstr_concat_assoc.
    Qed.

    Corollary omega_iter_rotate x y : omega_iter (nstr_concat' x y) == x +++ omega_iter (nstr_concat' y x).
    Proof.
      unfold omega_iter. now rewrite <-flatten_rotate, flatten_correct, hd_correct, tl_correct.
    Qed.

    Lemma omega_iter_step x : omega_iter x == match x with
                                | sing a => a ::: omega_iter (sing a)
                                | ncons a b => a ::: omega_iter (nstr_concat' b (sing a)) end.
    Proof.
      intros n. destruct x.
      - now rewrite omega_iter_correct at 1.
      - now rewrite nstr_concat_sing, omega_iter_rotate.
    Qed.

    Lemma flatten_fin_iter x (tau: Seq nat) y : x +++ flatten (map (nstr_finIter y) tau) == x +++ flatten (const y).
    Proof.
      intros n. revert x y tau. induction n; intros x y tau.
      - destruct x as [a | a x]; simpl; now rewrite !nth_first.
      - destruct x as [a | a x]; simpl; rewrite !nth_step.
        + setoid_rewrite flatten_correct at 1 2.
          rewrite map_correct, const_correct, !hd_correct, !tl_correct.
          destruct (hd tau) as [| m].
          * simpl. apply IHn.
          * simpl. rewrite <-prepend_nstr_assoc.
            enough (nstr_finIter y m +++ flatten (map (nstr_finIter y) (tl tau)) == flatten (map (nstr_finIter y) (m ::: tl tau))) as H.
            -- rewrite H. apply IHn.
            -- symmetry. now rewrite flatten_correct, map_correct, !hd_correct, !tl_correct.
        + apply IHn.
    Qed.

    Corollary omega_iter_iter x n: omega_iter x == omega_iter (nstr_finIter x n).
    Proof.
      unfold omega_iter.
      enough (const (nstr_finIter x n) == map (nstr_finIter x) (const n)) as H.
      - rewrite H. setoid_rewrite flatten_correct at 1 2.
        setoid_rewrite map_correct at 1 2.
        setoid_rewrite const_correct at 1 2 3 4 5 6.
        rewrite !hd_correct, !tl_correct. destruct n.
        + simpl. now rewrite flatten_fin_iter.
        + simpl. rewrite <-prepend_nstr_assoc.
          enough ((nstr_finIter x n +++ flatten (map (nstr_finIter x) (const (S n)))) == flatten (map (nstr_finIter x) (n ::: const (S n)))) as H2.
          * rewrite H2. now rewrite flatten_fin_iter.
          * symmetry. now rewrite flatten_correct, map_correct, !hd_correct, !tl_correct.
      - intros m. now rewrite const_nth, map_nth, const_nth.
    Qed.

    Lemma omega_iter_sing a : omega_iter (sing a) == const a.
    Proof.
      intros n. induction n; rewrite omega_iter_correct, const_correct; simpl.
      - now rewrite 2nth_first.
      - now rewrite 2 nth_step.
    Qed.



  End OmegaIteration.

  Lemma omega_iter_map X Y (f: X -> Y) x: map f (omega_iter x) == omega_iter (nstr_map f x).
  Proof.
    unfold omega_iter. rewrite flatten_map. apply flatten_proper.
    intros n. now rewrite map_nth, 2const_nth.
  Qed.

  Section Annotate.

    Context{X:Type}.
    Variable (P:X -> Prop).
    Context {decP: forall x, dec (P x)}.


    Definition annotate (sigma:Seq X) (H: forall n, P (sigma n)) : Seq {x | P x }:= map (fun x => match decision (P x) with
                                                     |left H => exist _ x H
                                                     |right _ => exist _ (sigma 0) (H 0) end ) sigma.

    Lemma annotate_correct (sigma:Seq X) (H: forall n, P(sigma n)) : forall n, proj1_sig (annotate H n) = sigma n.
    Proof.
      intros n. unfold annotate. rewrite map_nth. destruct decision as [D|D].
      - reflexivity.
      - exfalso. apply D, H.
    Qed.

  End Annotate.



Cutting a Seqs into Strings of Given Length

Given some sequence sigma and a sequence of numbers tau, we can factorize sigma such that the nth string has length tau n - 1. Taking the predecessor is useful as one do not need a proof that tau is always greater 0.

  Fixpoint cut_seq (X:Type) (sigma: Seq X) (tau: Seq nat) n := match n with
    | 0 => closed_prefix sigma (hd tau)
    | S n => (cut_seq (drop sigma (S (hd tau))) (tl tau)) n
  end.

  Definition cut (X:Type) (sigma: Seq X) (tau: Seq nat) := wrap (cut_seq sigma tau).
  Global Arguments cut: simpl never.

  Lemma cut_correct (X: Type) (sigma : Seq X) tau : cut sigma tau == (closed_prefix sigma (hd tau)) ::: (cut (drop sigma (S (hd tau))) (tl tau)).
  Proof.
    unfold cut. intros n. rewrite wrap_correct. destruct n; cbn.
    - now rewrite nth_first.
    - now rewrite nth_step, wrap_correct.
  Qed.

  Global Instance cut_proper X : Proper (@seq_equiv _ X ==> @seq_equiv _ nat ==> @seq_equiv _ (NStr X)) (@cut X).
  Proof.
    intros sigma1 sigma2 Es tau1 tau2 Et n. revert sigma1 sigma2 Es tau1 tau2 Et.
    induction n; intros sigma1 sigma2 Es tau1 tau2 Et; setoid_rewrite cut_correct at 1 2; rewrite (hd_proper Et).
    - rewrite 2 nth_first; now rewrite Es.
    - rewrite 2 nth_step. apply IHn. now rewrite Es. now rewrite Et.
  Qed.

  Lemma cut_delta X (sigma : Seq X) tau : map delta (cut sigma tau) == tau.
  Proof.
    intros n. revert sigma tau. induction n; intros sigma tau; rewrite cut_correct, map_correct, hd_correct, tl_correct.
    - now rewrite nth_first, closed_prefix_delta.
    - rewrite nth_step, nth_step_tl. apply IHn.
  Qed.

  Lemma flatten_cut_inv X (sigma: Seq X)( tau: Seq nat): flatten (cut sigma tau) == sigma.
  Proof.
    enough (forall m, (prefix sigma m) +++ flatten (cut (drop sigma m) tau) == sigma) as H by apply (H 0).
    intros m n. revert m sigma tau. induction n; intros m sigma tau.
    - destruct m.
      + rewrite cut_correct, flatten_correct, hd_correct, tl_correct. destruct (hd tau); simpl; now rewrite nth_first.
      + simpl. now rewrite nth_first.
    - destruct m.
      + simpl. rewrite cut_correct, flatten_correct, hd_correct, tl_correct, <-nonempty_prefix_is_closed.
        simpl. rewrite nth_step. apply IHn.
      + simpl. rewrite nth_step. apply IHn.
  Qed.

  Lemma cut_flatten_inv X (sigma: Seq (NStr X)): cut (flatten sigma) (map delta sigma) == sigma.
  Proof.
    intros n. revert sigma. induction n; intros sigma.
    - rewrite flatten_correct, cut_correct. rewrite nth_first.
      unfold nth. simpl. rewrite map_correct, hd_correct.
      apply closed_prefix_eq.
    - rewrite flatten_correct, cut_correct. rewrite nth_step.
      rewrite map_correct, hd_correct, tl_correct, delta_length, revert_prepend.
      apply IHn.
  Qed.

  Lemma flatten_concat X (sigma: Seq (NStr X)) x y : flatten (nstr_concat' x y ::: sigma) == flatten ( x:::(y:::sigma)).
  Proof.
    intros n. revert x y sigma. induction n; intros [a | a x] y sigma; simpl; setoid_rewrite flatten_step at 1 2; simpl.
    - now rewrite 2nth_first.
    - now rewrite 2nth_first.
    - rewrite 2 nth_step. now rewrite 2tl_correct.
    - rewrite 2nth_step. rewrite 2tl_correct. apply IHn.
  Qed.

  Lemma double_flatten_cut_inv (Y: Type) (sigma: Seq (NStr Y)) tau: flatten (map nstr_flatten (cut sigma tau)) == flatten sigma.
  Proof.
    revert sigma tau.

    enough (forall (sigma: Seq (NStr Y)) tau x n , flatten (x ::: (nstr_flatten (closed_prefix sigma n) ::: map nstr_flatten (cut (drop sigma (S n)) tau))) == flatten (x ::: sigma)).
    { intros sigma tau. rewrite cut_correct, map_correct, hd_correct, tl_correct.
      destruct (hd tau).
      - simpl.
        rewrite cut_correct, map_correct, hd_correct, tl_correct.
        setoid_rewrite (scons_correct sigma) at 4. apply H.
      - simpl. rewrite flatten_concat,H. apply flatten_proper.
        now rewrite <-scons_correct. }
    intros sigma tau x k n. revert sigma tau x k. induction n; intros sigma tau x k.
    - setoid_rewrite flatten_step at 1 2; rewrite !hd_correct; destruct x; simpl; now rewrite 2 nth_first.
    - setoid_rewrite flatten_step at 1 2.
      rewrite !hd_correct. destruct x; simpl; rewrite 2nth_step, !tl_correct.
      + destruct k.
        * simpl. rewrite cut_correct, map_correct, hd_correct, tl_correct.
          setoid_rewrite (scons_correct sigma) at 4. apply IHn.
        * simpl. setoid_rewrite (scons_correct sigma) at 4.
          rewrite flatten_concat. apply IHn.
      + apply IHn.
  Qed.

  Lemma cut_map X Y (sigma: Seq X) (f: X -> Y) tau : cut (map f sigma) tau == map (nstr_map f) (cut sigma tau).
  Proof.
    intros n. revert sigma tau. induction n; intros sigma tau.
    - rewrite cut_correct. setoid_rewrite cut_correct at 2.
      setoid_rewrite map_correct at 3.
      rewrite 2nth_first, hd_correct. generalize (hd tau) as m.
      intros m. revert sigma. induction m; intros sigma.
      + simpl. now rewrite map_correct, hd_correct.
      + simpl. f_equal.
        rewrite map_correct, tl_correct. apply IHm.
    - rewrite cut_correct. setoid_rewrite map_correct at 3.
      rewrite 2nth_step. setoid_rewrite cut_correct at 2.
      rewrite tl_correct, drop_map. apply IHn.
  Qed.

Languages (or Predicates) of Sequences

We see predicates on sequences as languages and define the usual operations on them.

  Section Languages.

    Definition PreImage(X Y :Type)(f: X -> Y)(L: Language (Seq Y)) : Language (Seq X) := fun sigma => L (map f sigma).
    Definition Image (X Y: Type)(f: X -> Y)(L: Language (Seq X)) : Language (Seq Y) := fun sigma => exists tau, map f tau == sigma /\ L tau.

    Definition Prepend (X:Type) (L1: Language (Str X))(L2: Language (Seq X)) : Language (Seq X) :=
       fun sigma => exists x tau, L1 x /\ L2 tau /\ sigma == x +++ tau.
    Definition PrependN (X:Type) (L1: Language (NStr X))(L2: Language (Seq X)) : Language (Seq X) :=
       fun sigma => exists x tau, L1 x /\ L2 tau /\ sigma == x +++ tau.
    Definition OmegaIter (X:Type) (L : Language (NStr X)) : Language (Seq X):=
       fun sigma => exists (tau: Seq (NStr X)), (forall n, L ( tau n)) /\ (sigma == flatten tau).

    Global Instance PreImageProper X Y (f: X-> Y): Proper (@language_eq (Seq Y) ==> @language_eq (Seq X)) (@PreImage X Y f).
    Proof.
      intros L1 L2 E sigma. unfold PreImage. split; apply E.
    Qed.

    Global Instance ImageProper X Y (f: X-> Y): Proper (@language_eq (Seq X) ==> @language_eq (Seq Y)) (@Image X Y f).
    Proof.
      intros L1 L2 E sigma. unfold Image. split; intros [tau [H1 H2]]; exists tau; split; auto; now apply E.
    Qed.

    Global Instance OmegaIterProper X: Proper (@language_eq (NStr X) ==> @language_eq (Seq X)) (@ OmegaIter X).
    Proof.
      intros L1 L2 E sigma. split;
      intros [tau [AL F]]; exists tau; split; auto; intros n; now apply E.
    Qed.

    Global Instance PrependProper X: Proper (@language_eq (Str X) ==> @language_eq (Seq X) ==> @language_eq (Seq X)) (@Prepend X).
    Proof.
      intros L1 L1' E1 L2 L2' E2 sigma. split;
      intros [x [tau [M1 [M2 ]]]]; exists x, tau; repeat split; auto; try apply E1; now try apply E2.
    Qed.

    Global Instance PrependNProper X: Proper (@language_eq (NStr X) ==> @language_eq (Seq X) ==> @language_eq (Seq X)) (@PrependN X).
    Proof.
      intros L1 L1' E1 L2 L2' E2 sigma. split;
      intros [x [tau [M1 [M2 ]]]]; exists x, tau; repeat split; auto; try apply E1; now try apply E2.
    Qed.

    Lemma prepend_lang_split_position X L1 L2 (sigma:Seq X) :
        (exists n, L1 (prefix sigma n) /\ L2 (drop sigma n)) -> (Prepend L1 L2) sigma.
    Proof.
      intros [n [LP LD]]. exists (prefix sigma n), (drop sigma n). repeat split; auto.
      apply revert_drop.
    Qed.

  End Languages.

End MoreSequences.

Notation "l ^00" := (OmegaIter l) (at level 20).
Notation "l1 'o' l2" := (Prepend l1 l2) (at level 50).
Notation "l1 'o'' l2" := (PrependN l1 l2) (at level 50).

(* Tactic for destruction annotate expression must be on the toplevel.

   it changes (proj1_sig (annotate H) n) to (sigma n) and adds
   P (sigma n) to Context.
   
   H: name of the proof of forall n, P (sigma n)
   n: index
   P: pattern for destructing P(sigma n)  *)
Ltac destruct_annotate H n P := let Q := fresh in
                                    let x := fresh in
                                      pose proof (annotate_correct H n) as Q;
                                      destruct (annotate H n) as [x P];
                                      simpl proj1_sig in *;
                                      subst x.
Tactic Notation "destruct_annotate" constr(H) constr(n) "as" simple_intropattern(P) := destruct_annotate H n P.

Arguments annotate {X} {P} {decP} {sigma} H.

Lemma test_destruct_annotate (X:finType) (P: X -> Prop) (decP: forall x, dec (P x)) (x_D: X)(H_D: P x_D) (sigma: Seq X) (H: forall n, P (sigma n)): forall n, P( map (@proj1_sig _ _) (annotate H) n ).
Proof.
  intros n. rewrite map_nth. now destruct_annotate H n as Q.
Qed.