Set Implicit Arguments.

Require Import Coq.Init.Nat.
Require Import BA.External.
Require Import BasicDefs.

# Sequences

General operations and facts about sequences

Definition Seq (X:Type) := nat -> X.

Definition SeqLang (X:Type) := Language (Seq X).
Notation "x ^0\$0" := (universal_language (X:=Seq x)) (at level 20).

## Basic Operations on Sequences

Section SeqOperations.

Context {X:Type}.

Dropping the first n elements of a sequence
Fixpoint drop n (w:Seq X) := match n with
| 0 => w
| S n => drop n (fun n => w (S n))
end.

Prepending an element to a sequence
Definition prepend a (w:Seq X) := fun n => match n with
| 0 => a
| S n => w n
end.

prepend_path prepends the first k+1 values of the sequence p on the sequence w, k+1 makes sence with respect to the definition of strings
Fixpoint prepend_path k (p:Seq X) (w:Seq X) : Seq X := match k with
| 0 => prepend (p 0) w
| S k => prepend (p 0) (prepend_path k (drop 1 p) w)
end.

Cutting something from n exlusively to m inclusively out of a sequence
Definition cut n m (w:Seq X) := prepend_path n w (drop m w).

Lemma drop_correct n (w:Seq X) : forall m, (drop n w) m = w (n + m).
Proof.
revert w.
induction n; intros w m.
- reflexivity.
- apply IHn with (w:= (fun n => w ( S n))) (m:=m).
Qed.

Lemma prepend_first_correct a (w:Seq X): ((prepend a w) 0) = a.
Proof.
reflexivity.
Qed.

Lemma prepend_rest_correct a (w:Seq X): forall n, ((prepend a w) (S n)) = w n.
Proof.
reflexivity.
Qed.

Lemma prepend_rest_correct2 a (w: Seq X): forall n , n > 0 -> (prepend a w) n = w (pred n).
Proof.
intros n L.
destruct n; oauto.
Qed.

Lemma prepend_path_begin_correct k p w n: n <= k -> prepend_path k p w n = p n.
Proof.
revert p w n.
induction k; intros p w n L.
- simpl. rewrite_eq (n = 0).
apply prepend_first_correct.
- simpl.
destruct n.
+ apply prepend_first_correct.
+ rewrite prepend_rest_correct2 by omega.
change (prepend_path k (drop 1 p) w n = (drop 1 p) n).
apply IHk.
omega.
Qed.

Lemma prepend_path_first k p w: (prepend_path k p w) 0 = p 0.
Proof.
apply prepend_path_begin_correct. omega.
Qed.

Lemma prepend_path_rest_correct k p w n: (prepend_path k p w) (S k + n) = w n.
Proof.
revert p w n.
induction k; intros p w n.
- now reflexivity.
- simpl. rewrite_eq (S (k + n) = S k +n).
apply IHk.
Qed.

Lemma prepend_path_rest_correct2 k p w m n: (m = S k + n) -> (prepend_path k p w) m = w n.
Proof.
intros H.
rewrite H.
apply prepend_path_rest_correct.
Qed.

Lemma cut_front_correct n m w : forall k, k <= n -> (cut n m w) k = w k.
Proof.
intros k L.
unfold cut.
now rewrite prepend_path_begin_correct.
Qed.

Lemma cut_rest_correct n m w: forall k, (cut n m w) (S n + k) = w (m + k).
Proof.
intros k.
unfold cut.
rewrite prepend_path_rest_correct.
now rewrite drop_correct.
Qed.

Lemma revert_prepend_path k (w w': Seq X): forall n, drop (S k) (prepend_path k w' w) n = w n.
Proof.
intros n.
rewrite drop_correct.
now rewrite prepend_path_rest_correct.
Qed.

Lemma revert_drop_path k (w : Seq X) : forall n, prepend_path k w (drop (S k) w) n = w n.
Proof.
intros n.
decide (n <= k).
- rewrite prepend_path_begin_correct; auto.
- remember (n - S k ) as z.
rewrite_eq (n = S k + z).
rewrite prepend_path_rest_correct.
now rewrite drop_correct.
Qed.

Mapping function on sequences
Definition seq_map (A1 A2 : Type) (f: A1 -> A2) (w : Seq A1) : (Seq A2) := fun n => f (w n).

End SeqOperations.

## An element occuring infinitely often in a Sequence

Section Infinite.
Context {X:Type}.

Definition infinite (x:X) (w:Seq X) := forall n, exists m, m>=n /\ (w m) = x.

Lemma finite_prefix_preserves_infinite k p w s: infinite s w -> infinite s (prepend_path k p w).
Proof.
intros I n.
destruct (I n) as [m [P Q]].
exists (S k + m).
split.
- omega.
- now rewrite prepend_path_rest_correct.
Qed.

Lemma drop_preserves_finite s w n: infinite s w -> infinite s (drop n w).
Proof.
intros I k.
destruct (I (k+n)) as [m [P Q]].
exists (m-n). split.
- omega.
- rewrite drop_correct.
rewrite <-Q. f_equal. omega.
Qed.
End Infinite.

## Pointwise equiality of sequences

Definition seq_equal (X:Type)(w1 w2 : Seq X) := forall n, w1 n = w2 n.
Notation "w1 === w2" := (seq_equal w1 w2) (at level 70).
Hint Unfold seq_equal.

## Decidability of bounded quantifiers on Sequences

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.
induction n.
- decide (P (w 0)) as [D|D].
+ left. firstorder.
+ right. intros [k [L Q]]. now rewrite_eq (k = 0) in Q.
- decide (P (w (S n))) as [D|D].
+ left. exists (S n); auto.
+ destruct (IHn) as [D'|D'].
* left. firstorder.
* right. intros [k [L Q]].
decide (k <= n).
-- apply D'. exists k; auto.
-- apply D. now rewrite_eq (S n = k).
Defined.

Instance dec_bounded_nat_forall (P: nat -> Prop) (decP: forall n, dec (P n)) m : dec (forall n, n <= m -> P n).
Proof.
destruct (seq_dec_exists_bounded (P:= fun n => ~ P n) _ (fun (n:nat) => n) m).
- right. firstorder.
- left. firstorder.
Defined.

Instance dec_strict_bounded_nat_forall (P: nat -> Prop) (decP: forall n, dec (P n)) m : dec (forall n, n < m -> P n).
Proof.
destruct m.
- left. intros n L. exfalso. omega.
- destruct (dec_bounded_nat_forall decP m).
+ left. firstorder.
+ right. firstorder.
Defined.

Lemma seq_prop_dec_exists_bounded (X:Type) (p: X ->Prop) (L: Seq X) (l: nat): (forall x, p x \/ ~ p x) -> (exists i, i <= l /\ p (L i)) \/ (forall i, i <= l -> ~ p (L i)).
Proof.
intros pD.
induction l.
- simpl. destruct (pD (L 0)) as [H|H].
+ left. firstorder.
+ right. intros i O. now rewrite_eq (i = 0).
- destruct IHl as [[i [O P]] | IHl].
+ simpl in O,P. left. firstorder.
+ destruct (pD (L (S l))) as [H|H].
* left. firstorder.
* right. intros i O.
decide (i = S l) as [D|D].
-- now subst i.
-- apply (IHl i). omega.
Qed.

Delimit Scope string_scope with string.

# Strings

A String is a nonempty prefix on a sequence: lastindex is the last index in seq which belongs to the string Deriving strings from sequences makes operations on both uinform on easier
Structure String (X:Type) := mkstring {seq :> Seq X; lastindex : nat}.

Notation "| v |" := (lastindex v) : string_scope.
Notation "v [ k ]" := ((seq v) k) (at level 10) : string_scope.

Open Scope string_scope.

## Equality Relation on Strings

Because strings consist of sequences, there is no usable equality on them. Define the pointwise equality relation.
Section StringsEq.
Context {X: Type}.

Definition strings_equal (w w': String X):= |w| = |w'| /\ (forall n, n <= |w| -> w [n] = w' [n]).

Lemma string_equal_reflexive: reflexive (String X) strings_equal.
Proof.
intros w. split; auto.
Qed.

Lemma string_equal_symmetric : symmetric (String X) strings_equal.
Proof.
intros w w' [EL EW]. split.
- omega.
- intros n L. symmetry. apply (EW n). omega.
Qed.
End StringsEq.

## Simple Operations on Strings

Section StringOperations.
Context {X:Type}.

Definition concat_strings (v w : String X ) : String X := mkstring (prepend_path (|v|) v w) ((|v|) + S(|w|)).

Definition drop_string_begin n (w: String X) := mkstring (drop n w) ((|w|) - n).
Definition drop_string_end n (w: String X) := mkstring w ((|w|) - n).

Extracts the string from w starting at index n (inclusively) until index m (exclusively)
Definition extract n m (w : Seq X) : String X:= mkstring(drop n w) (m - S n).

Lemma extract_correct n m w: forall k, (extract n m w) [k] = w (n + k).
Proof.
intros k.
simpl.
apply drop_correct.
Qed.

End StringOperations.

Notation "v ++ w" := (concat_strings v w) : string_scope.
Notation "v +++ w" := (prepend_path (|v|) v w) (at level 60) : string_scope .
Notation "v == w" := (strings_equal v w) (at level 65): string_scope.

## Equality of results of some string operations

Lemma revert_concat_first (X:Type)(v w:String X): v == drop_string_end (S(|w|)) (v ++ w).
Proof.
unfold drop_string_end. simpl. split.
- simpl. omega.
- intros n L. simpl. now rewrite prepend_path_begin_correct.
Qed.

Lemma revert_concat_second (X:Type)(v w:String X): w == drop_string_begin (S(|v|)) (v ++ w).
Proof.
unfold drop_string_begin. split.
- simpl. omega.
- intros n L. simpl. rewrite drop_correct.
rewrite_eq (S((|v|) + n) = S (|v|) + n). now rewrite prepend_path_rest_correct.
Qed.

Lemma concat_extract (X:Type) (w : Seq X) i1 i2 i3: i1 < i2 -> i2 < i3 -> ((extract i1 i2 w) ++ (extract i2 i3 w)) == (extract i1 i3 w).
Proof.
intros L1 L2.
split.
- simpl. omega.
- intros n L.
simpl. decide (n <= (i2 - S i1)) as [D|D].
+ now rewrite prepend_path_begin_correct by omega.
+ remember (n - S(i2 - S i1)) as z.
rewrite_eq (n = S(i2 - S i1) + z).
rewrite prepend_path_rest_correct.
repeat rewrite drop_correct. f_equal. omega.
Qed.

Lemma extract_from_drop (X:Type) (w:Seq X) n m k: (extract n m (drop k w)) == (extract (n + k) (m + k) w).
Proof.
repeat split; simpl; oauto.
intros i B. simpl. repeat rewrite drop_correct.
f_equal. omega.
Qed.

## Languages of Strings

Definition StringLang (A: Type) := Language (String A).

Extensionality on strings: a string language is extensional if it does only care about the values of the valid indicies of w
Definition StringLang_Extensional (A:Type) (l: StringLang A):= forall (w w' : String A ), l w -> w == w' -> l w'.