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.
Instance seq_equal_Equivalence X :
Equivalence (@seq_equal X).
Proof.
constructor.
- constructor.
- intros w_1 w_2 E n. now rewrite E.
- intros w_1 w_2 w_3 E_1 E_2 n. now rewrite <-E_2, E_1.
Qed.
Notation "w1 === w2" := (seq_equal w1 w2) (at level 70).
Hint Unfold seq_equal.
Instance seq_equal_Equivalence X :
Equivalence (@seq_equal X).
Proof.
constructor.
- constructor.
- intros w_1 w_2 E n. now rewrite E.
- intros w_1 w_2 w_3 E_1 E_2 n. now rewrite <-E_2, E_1.
Qed.
Dropping the first n elements of a sequence
Prepending an element to a sequence
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_prefix k w' w : Seq X:= match k with
| 0 => prepend (w' 0) w
| S k => prepend_prefix k w' (prepend (w' (S k)) w)
end.
Lemma drop_correct n w : 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 drop_correct' n w m : (drop n w) m = w (m + n).
Proof.
rewrite_eq (m + n = n + m). apply drop_correct.
Qed.
Lemma drop_correct'' n w m : n <= m -> (drop n w) (m - n) = w m.
Proof.
intros L. rewrite drop_correct. f_equal. omega.
Qed.
Lemma prepend_first a (w:Seq X): ((prepend a w) 0) = a.
Proof.
reflexivity.
Qed.
Lemma prepend_rest a (w:Seq X): forall n, ((prepend a w) (S n)) = w n.
Proof.
reflexivity.
Qed.
Lemma prepend_rest2 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_prefix_rest k w' w n : prepend_prefix k w' w (S k + n) = w n.
Proof.
revert w' w n. induction k; intros w' w n; cbn.
- reflexivity.
- rewrite_eq (S (S (k + n)) = S k + S n).
now rewrite IHk.
Qed.
Lemma prepend_prefix_rest2 k w' w n : n > k -> prepend_prefix k w' w n = w (n - S k).
Proof.
intros L. remember (n - S k) as m. rewrite_eq (n = S k + m). subst m.
apply prepend_prefix_rest.
Qed.
Lemma prepend_prefix_rest' k w' w n : prepend_prefix k w' w (n + S k) = w n.
Proof.
rewrite_eq (n + S k = S k + n). apply prepend_prefix_rest.
Qed.
Lemma prepend_prefix_begin k w' w n : n <= k -> prepend_prefix k w' w n = w' n.
Proof.
revert k w' w n.
induction k; intros w' w n L; cbn.
- now rewrite_eq (n = 0).
- decide (n = S k) as [->|D].
+ rewrite prepend_prefix_rest2 by omega.
now rewrite_eq (S k - S k = 0).
+ apply IHk. omega.
Qed.
| 0 => prepend (w' 0) w
| S k => prepend_prefix k w' (prepend (w' (S k)) w)
end.
Lemma drop_correct n w : 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 drop_correct' n w m : (drop n w) m = w (m + n).
Proof.
rewrite_eq (m + n = n + m). apply drop_correct.
Qed.
Lemma drop_correct'' n w m : n <= m -> (drop n w) (m - n) = w m.
Proof.
intros L. rewrite drop_correct. f_equal. omega.
Qed.
Lemma prepend_first a (w:Seq X): ((prepend a w) 0) = a.
Proof.
reflexivity.
Qed.
Lemma prepend_rest a (w:Seq X): forall n, ((prepend a w) (S n)) = w n.
Proof.
reflexivity.
Qed.
Lemma prepend_rest2 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_prefix_rest k w' w n : prepend_prefix k w' w (S k + n) = w n.
Proof.
revert w' w n. induction k; intros w' w n; cbn.
- reflexivity.
- rewrite_eq (S (S (k + n)) = S k + S n).
now rewrite IHk.
Qed.
Lemma prepend_prefix_rest2 k w' w n : n > k -> prepend_prefix k w' w n = w (n - S k).
Proof.
intros L. remember (n - S k) as m. rewrite_eq (n = S k + m). subst m.
apply prepend_prefix_rest.
Qed.
Lemma prepend_prefix_rest' k w' w n : prepend_prefix k w' w (n + S k) = w n.
Proof.
rewrite_eq (n + S k = S k + n). apply prepend_prefix_rest.
Qed.
Lemma prepend_prefix_begin k w' w n : n <= k -> prepend_prefix k w' w n = w' n.
Proof.
revert k w' w n.
induction k; intros w' w n L; cbn.
- now rewrite_eq (n = 0).
- decide (n = S k) as [->|D].
+ rewrite prepend_prefix_rest2 by omega.
now rewrite_eq (S k - S k = 0).
+ apply IHk. omega.
Qed.
Mapping function on sequences
Definition seq_map (Y : Type) (f: X -> Y) w : (Seq Y) := fun n => f (w n).
Definition seq_zip (X Y: Type) (w: Seq X) (w': Seq Y) := fun n => (w n, w' n).
Global Instance seq_zip_proper (X Y: Type) : Proper (@seq_equal X ==> @seq_equal Y ==> @seq_equal (X*Y)) (@seq_zip X Y).
Proof.
intros w_1 w_1' E_1 w_2 w_2' E_2 n. unfold seq_zip. now rewrite E_1, E_2.
Qed.
Global Instance seq_map_proper (Y: Type) (f: X -> Y): Proper (@seq_equal X ==> @seq_equal Y) (seq_map f).
Proof.
intros w w' E n. unfold seq_map. now rewrite E.
Qed.
End SeqOperations.
Delimit Scope string_scope with string.
Definition seq_zip (X Y: Type) (w: Seq X) (w': Seq Y) := fun n => (w n, w' n).
Global Instance seq_zip_proper (X Y: Type) : Proper (@seq_equal X ==> @seq_equal Y ==> @seq_equal (X*Y)) (@seq_zip X Y).
Proof.
intros w_1 w_1' E_1 w_2 w_2' E_2 n. unfold seq_zip. now rewrite E_1, E_2.
Qed.
Global Instance seq_map_proper (Y: Type) (f: X -> Y): Proper (@seq_equal X ==> @seq_equal Y) (seq_map f).
Proof.
intros w w' E n. unfold seq_map. now rewrite E.
Qed.
End SeqOperations.
Delimit Scope string_scope with string.
Strings as Prefixes
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.
Notation "| v |" := (lastindex v) : string_scope.
Notation "v [ k ]" := ((seq v) k) (at level 10) : string_scope.
Open Scope string_scope.
Equivalence on Strings
Because strings consist of sequences, there is no usable equality on them. Define the pointwise equality relation.
Section StringsEq.
Context {X: Type}.
Implicit Types (u v : String X).
Definition strings_equal u v := |u| = |v| /\ (forall n, n <= |u| -> u [n] = v [n]).
Lemma strings_equal_reflexive: reflexive (String X) strings_equal.
Proof.
intros w. split; auto.
Qed.
Lemma strings_equal_symmetric : symmetric (String X) strings_equal.
Proof.
intros w w' [EL EW]. split.
- omega.
- intros n L. symmetry. apply (EW n). omega.
Qed.
Lemma strings_equal_transitive : transitive (String X) strings_equal.
Proof.
intros w_1 w_2 w_3 [EL EW] [FL FW]. split.
- omega.
- intros n L. rewrite EW by omega. apply FW. omega.
Qed.
Global Instance strings_equal_Equivalence: Equivalence strings_equal.
Proof.
constructor.
- apply strings_equal_reflexive.
- apply strings_equal_symmetric.
- apply strings_equal_transitive.
Qed.
Global Instance string_lastindex_proper: Proper (strings_equal ==> eq) (@lastindex X).
Proof.
now intros v v' [EL _].
Qed.
End StringsEq.
Context {X: Type}.
Implicit Types (u v : String X).
Definition strings_equal u v := |u| = |v| /\ (forall n, n <= |u| -> u [n] = v [n]).
Lemma strings_equal_reflexive: reflexive (String X) strings_equal.
Proof.
intros w. split; auto.
Qed.
Lemma strings_equal_symmetric : symmetric (String X) strings_equal.
Proof.
intros w w' [EL EW]. split.
- omega.
- intros n L. symmetry. apply (EW n). omega.
Qed.
Lemma strings_equal_transitive : transitive (String X) strings_equal.
Proof.
intros w_1 w_2 w_3 [EL EW] [FL FW]. split.
- omega.
- intros n L. rewrite EW by omega. apply FW. omega.
Qed.
Global Instance strings_equal_Equivalence: Equivalence strings_equal.
Proof.
constructor.
- apply strings_equal_reflexive.
- apply strings_equal_symmetric.
- apply strings_equal_transitive.
Qed.
Global Instance string_lastindex_proper: Proper (strings_equal ==> eq) (@lastindex X).
Proof.
now intros v v' [EL _].
Qed.
End StringsEq.
Section StringOperations.
Context {X:Type}.
Implicit Types (u v : String X).
Implicit Types (w : Seq X).
Definition prepend_string v w := prepend_prefix (|v|) v w.
Definition concat_strings u v := mkstring (prepend_string u v) ((|u|) + S(|v|)).
Definition drop_string_begin n u := mkstring (drop n u) ((|u|) - n).
Definition drop_string_end n u := mkstring u ((|u|) - n).
Context {X:Type}.
Implicit Types (u v : String X).
Implicit Types (w : Seq X).
Definition prepend_string v w := prepend_prefix (|v|) v w.
Definition concat_strings u v := mkstring (prepend_string u v) ((|u|) + S(|v|)).
Definition drop_string_begin n u := mkstring (drop n u) ((|u|) - n).
Definition drop_string_end n u := mkstring u ((|u|) - n).
Extracts the string from w starting at index n (inclusively) until index m (exclusively)
Cutting something from n exlusively to m inclusively out of a sequence
Definition cut n m w := prepend_string (mkstring w n) (drop m w).
Definition cut_string n m v := concat_strings (mkstring v n) (drop_string_begin m v).
Lemma extract_correct n m w: forall k, (extract n m w) [k] = w (n + k).
Proof.
intros k.
simpl.
apply drop_correct.
Qed.
Definition string_map (X Y: Type) (f: X -> Y) (v: String X) : String Y := (mkstring (seq_map f v) (|v|)).
End StringOperations.
Notation "v ++ w" := (concat_strings v w) : string_scope.
Notation "v +++ w" := (prepend_string v w) (at level 60) : string_scope .
Notation "v == w" := (strings_equal v w) (at level 65): string_scope.
Section StringOperationLemmas.
Context {X:Type}.
Implicit Types (u v : String X).
Implicit Types (w : Seq X).
Lemma wrap_string v n: n =|v| -> v == mkstring v n.
Proof.
intros ->.
destruct v; cbn. reflexivity.
Qed.
Lemma prepend_string_begin v w n : n <= |v| -> (v +++ w) n = v [n].
Proof.
intros L. unfold prepend_string. now rewrite prepend_prefix_begin.
Qed.
Lemma prepend_string_rest v w n : n > |v| -> (v +++ w) n = w (n - S(|v|)).
Proof.
intros L. unfold prepend_string. now rewrite prepend_prefix_rest2.
Qed.
Lemma prepend_string_rest' v w n : (v +++ w) (S (|v|) + n) = w n.
Proof.
rewrite prepend_string_rest by omega. f_equal. omega.
Qed.
Lemma prepend_string_rest'' v w n k : k = S(|v|) -> (v +++ w) (k + n) = w n.
Proof.
intros ->. apply prepend_string_rest'.
Qed.
Lemma revert_prepend_string v w : drop (S (|v|)) (v +++ w) === w.
Proof.
intros n. rewrite drop_correct. rewrite prepend_string_rest by omega. f_equal. omega.
Qed.
Lemma revert_drop k w : mkstring w k +++ (drop (S k) w) === w.
Proof.
intros n. decide (n <= k).
- now rewrite prepend_string_begin by comega.
- rewrite prepend_string_rest by comega. rewrite drop_correct. f_equal. comega.
Qed.
Lemma concat_string_begin u v n : n <= |u| -> (u ++ v) [n] = u [n].
Proof.
intros L. unfold concat_strings. cbn. now apply prepend_string_begin.
Qed.
Lemma concat_string_rest u v n : n > |u| -> (u ++ v) [n] = v [n - S(|u|)].
Proof.
intros L. unfold concat_strings. cbn. now apply prepend_string_rest.
Qed.
Lemma concat_strings_step k w v : (mkstring w (S k)) ++ v == (mkstring w k) ++ (mkstring (prepend (w (S k)) v) (S(|v|))).
Proof.
split; cbn; oauto.
Qed.
Lemma concat_strings_length (u v : String X): |u ++ v| = |u| + S(|v|).
Proof. reflexivity. Qed.
Lemma concat_prepend_string_associative u v w :(u ++ v) +++ w === u +++ (v +++ w).
Proof.
intros n.
decide (n <= |u|) as [D|D].
- repeat rewrite prepend_string_begin by comega. now rewrite concat_string_begin.
- symmetry. rewrite prepend_string_rest by comega.
decide (n <= |u| + S (|v|)) as [D'|D']; cbn in D'.
+ repeat rewrite prepend_string_begin by comega.
now rewrite concat_string_rest by comega.
+ repeat rewrite prepend_string_rest by comega. f_equal. cbn. omega.
Qed.
Lemma concat_strings_associative t u v : (t ++ u) ++ v == t ++ (u ++ v).
Proof.
split.
- cbn. omega.
- intros n L. apply concat_prepend_string_associative.
Qed.
Lemma revert_concat_first u v: u == drop_string_end (S(|v|)) (u ++ v).
Proof.
unfold drop_string_end. split; cbn.
- omega.
- intros n L. now rewrite prepend_string_begin.
Qed.
Lemma revert_concat_second u v: v == drop_string_begin (S(|u|)) (u ++ v).
Proof.
unfold drop_string_begin. split.
- simpl. omega.
- intros n L. simpl. rewrite drop_correct.
rewrite prepend_string_rest by omega. f_equal. omega.
Qed.
Lemma concat_extract w i_1 i_2 i_3: i_1 < i_2 -> i_2 < i_3 -> (extract i_1 i_2 w) ++ (extract i_2 i_3 w) == extract i_1 i_3 w.
Proof.
intros L1 L2. split.
- comega.
- intros n L.
decide (n <= (i_2 - S i_1)) as [D|D].
+ now rewrite concat_string_begin by comega.
+ rewrite concat_string_rest by comega.
unfold extract. cbn. repeat rewrite drop_correct. f_equal. omega.
Qed.
Lemma extract_from_drop w n m k: (extract n m (drop k w)) == (extract (n + k) (m + k) w).
Proof.
repeat split; cbn; oauto.
intros i B. simpl. repeat rewrite drop_correct. f_equal. omega.
Qed.
Lemma extract_from_drop' w n m k: k <=n-> (extract (n-k) (m-k) (drop k w)) == (extract n m w).
Proof.
intros L. split; cbn; oauto.
intros i B. simpl. repeat rewrite drop_correct. f_equal. omega.
Qed.
Lemma drop_extract w n m: (extract n (S m) w) == drop_string_begin n (mkstring w m).
Proof.
split; auto.
Qed.
Lemma extract_prepend v w n m : (extract (n + S (| v |)) (m + S (| v |)) (v +++ w )) == extract n m w.
Proof.
split.
- cbn. omega.
- intros k L. cbn. cbn in L. rewrite !drop_correct.
rewrite prepend_string_rest by comega. f_equal. omega.
Qed.
Lemma cut_string_cut i j w k: i < j <= k -> cut_string i j (mkstring w k) == (mkstring (cut i j w) (S k - j + i)).
Proof.
intros L. split.
- cbn. destruct j; omega.
- now intros.
Qed.
Lemma cut_front n m w : forall k, k <= n -> (cut n m w) k = w k.
Proof.
intros k L. unfold cut. now rewrite prepend_string_begin.
Qed.
Lemma cut_rest n m w: forall k, (cut n m w) (S n + k) = w (m + k).
Proof.
intros k. unfold cut. now rewrite prepend_string_rest', drop_correct.
Qed.
End StringOperationLemmas.
Instance seq_eq_index (X:Type) n: Proper (@seq_equal X ==> eq) (fun w => w n).
Proof.
intros w w' Ew . apply Ew.
Qed.
Instance drop_proper (X:Type): Proper (eq ==> @seq_equal X ==> @seq_equal X) drop.
Proof.
intros n n' En w w' Ew k.
rewrite !drop_correct. subst n. now apply Ew.
Qed.
Instance prepend_string_proper (X:Type): Proper (@strings_equal X ==> @seq_equal X ==> @seq_equal X) (fun v w => v +++ w).
Proof.
intros v v' [EvL Ev] w w' Ew n. decide (n <= |v|).
- repeat rewrite prepend_string_begin by (try rewrite <- EvL; auto). now apply Ev.
- repeat rewrite prepend_string_rest by (try rewrite <- EvL; omega). rewrite <-EvL. apply Ew.
Qed.
Instance prepend_string_proper_index (X:Type): Proper (@strings_equal X ==> @seq_equal X ==> @eq nat ==> @eq X) (fun v w n=> (v +++ w) n).
Proof.
intros v v' [EvL Ev] w w' Ew n n' En. subst n'. decide (n <= |v|).
- repeat rewrite prepend_string_begin by (try rewrite <- EvL; auto). now apply Ev.
- repeat rewrite prepend_string_rest by (try rewrite <- EvL; omega). rewrite <-EvL. apply Ew.
Qed.
Instance cancat_strings_proper (X:Type): Proper (@strings_equal X ==> @strings_equal X ==> @strings_equal X) (@concat_strings X).
Proof.
intros u u' [Eu1 Eu2] v v' [Ev1 Ev2]. split.
- cbn. rewrite Eu1, Ev1. omega.
- intros n L. decide (n <= |u|).
+ repeat rewrite concat_string_begin by (try rewrite <-Eu1; auto). now apply Eu2.
+ repeat rewrite concat_string_rest by (try rewrite <-Ev1; omega). rewrite <-Eu1. apply Ev2. cbn in L. omega.
Qed.
Instance extract_proper (X:Type) : Proper (eq ==> eq ==> (@seq_equal X) ==> strings_equal) extract.
Proof.
intros n n' <- m m' <- w w' Ew. split; auto.
intros k L. cbn. now rewrite !drop_correct, Ew.
Qed.
Section FiniteIterationOfString.
Context {X:Type}.
Implicit Type (u v t : String X).
Fixpoint fin_iter v n := match n with
| 0 => v
| S n => v ++ (fin_iter v n)
end.
Lemma fin_iter_step v n : fin_iter v (S n) == v ++ (fin_iter v n).
Proof.
reflexivity.
Qed.
Lemma fin_iter_base v : fin_iter v 0 == v.
Proof.
reflexivity.
Qed.
Lemma fin_iter_split u v n: fin_iter (u++v) (S n) == u ++ (fin_iter (v ++ u) n) ++ v.
Proof.
induction n; cbn.
- now rewrite !concat_strings_associative.
- rewrite IHn. now rewrite !concat_strings_associative.
Qed.
Lemma fin_iter_length v n : |fin_iter v n| = S n * S (|v|) - 1.
Proof.
induction n; cbn.
- omega.
- rewrite IHn. rewrite Nat.mul_succ_l. remember (n * S(|v|)) as Z. omega.
Qed.
Lemma fin_iter_length_bound v n : n <= |fin_iter v n| .
Proof.
induction n; cbn; omega.
Qed.
Lemma fin_iter_sum v n m : fin_iter v (S n + m) == (fin_iter v n) ++ (fin_iter v m).
Proof.
induction n.
- reflexivity.
- rewrite_eq (S (S n) + m = S (S n + m)). rewrite fin_iter_step. rewrite IHn. cbn. now rewrite concat_strings_associative.
Qed.
Lemma fin_iter_fin_iter v n m : (fin_iter (fin_iter v n) m) == (fin_iter v (S m * S n -1)).
Proof.
induction m; cbn.
- now rewrite_eq (n + 0 - 0= n).
- rewrite IHm. cbn. rewrite <-fin_iter_sum.
remember (m * S n) as Z. now rewrite_eq (S n + (n + Z - 0) = n + S(n + Z) - 0).
Qed.
End FiniteIterationOfString.
Definition cut_string n m v := concat_strings (mkstring v n) (drop_string_begin m v).
Lemma extract_correct n m w: forall k, (extract n m w) [k] = w (n + k).
Proof.
intros k.
simpl.
apply drop_correct.
Qed.
Definition string_map (X Y: Type) (f: X -> Y) (v: String X) : String Y := (mkstring (seq_map f v) (|v|)).
End StringOperations.
Notation "v ++ w" := (concat_strings v w) : string_scope.
Notation "v +++ w" := (prepend_string v w) (at level 60) : string_scope .
Notation "v == w" := (strings_equal v w) (at level 65): string_scope.
Section StringOperationLemmas.
Context {X:Type}.
Implicit Types (u v : String X).
Implicit Types (w : Seq X).
Lemma wrap_string v n: n =|v| -> v == mkstring v n.
Proof.
intros ->.
destruct v; cbn. reflexivity.
Qed.
Lemma prepend_string_begin v w n : n <= |v| -> (v +++ w) n = v [n].
Proof.
intros L. unfold prepend_string. now rewrite prepend_prefix_begin.
Qed.
Lemma prepend_string_rest v w n : n > |v| -> (v +++ w) n = w (n - S(|v|)).
Proof.
intros L. unfold prepend_string. now rewrite prepend_prefix_rest2.
Qed.
Lemma prepend_string_rest' v w n : (v +++ w) (S (|v|) + n) = w n.
Proof.
rewrite prepend_string_rest by omega. f_equal. omega.
Qed.
Lemma prepend_string_rest'' v w n k : k = S(|v|) -> (v +++ w) (k + n) = w n.
Proof.
intros ->. apply prepend_string_rest'.
Qed.
Lemma revert_prepend_string v w : drop (S (|v|)) (v +++ w) === w.
Proof.
intros n. rewrite drop_correct. rewrite prepend_string_rest by omega. f_equal. omega.
Qed.
Lemma revert_drop k w : mkstring w k +++ (drop (S k) w) === w.
Proof.
intros n. decide (n <= k).
- now rewrite prepend_string_begin by comega.
- rewrite prepend_string_rest by comega. rewrite drop_correct. f_equal. comega.
Qed.
Lemma concat_string_begin u v n : n <= |u| -> (u ++ v) [n] = u [n].
Proof.
intros L. unfold concat_strings. cbn. now apply prepend_string_begin.
Qed.
Lemma concat_string_rest u v n : n > |u| -> (u ++ v) [n] = v [n - S(|u|)].
Proof.
intros L. unfold concat_strings. cbn. now apply prepend_string_rest.
Qed.
Lemma concat_strings_step k w v : (mkstring w (S k)) ++ v == (mkstring w k) ++ (mkstring (prepend (w (S k)) v) (S(|v|))).
Proof.
split; cbn; oauto.
Qed.
Lemma concat_strings_length (u v : String X): |u ++ v| = |u| + S(|v|).
Proof. reflexivity. Qed.
Lemma concat_prepend_string_associative u v w :(u ++ v) +++ w === u +++ (v +++ w).
Proof.
intros n.
decide (n <= |u|) as [D|D].
- repeat rewrite prepend_string_begin by comega. now rewrite concat_string_begin.
- symmetry. rewrite prepend_string_rest by comega.
decide (n <= |u| + S (|v|)) as [D'|D']; cbn in D'.
+ repeat rewrite prepend_string_begin by comega.
now rewrite concat_string_rest by comega.
+ repeat rewrite prepend_string_rest by comega. f_equal. cbn. omega.
Qed.
Lemma concat_strings_associative t u v : (t ++ u) ++ v == t ++ (u ++ v).
Proof.
split.
- cbn. omega.
- intros n L. apply concat_prepend_string_associative.
Qed.
Lemma revert_concat_first u v: u == drop_string_end (S(|v|)) (u ++ v).
Proof.
unfold drop_string_end. split; cbn.
- omega.
- intros n L. now rewrite prepend_string_begin.
Qed.
Lemma revert_concat_second u v: v == drop_string_begin (S(|u|)) (u ++ v).
Proof.
unfold drop_string_begin. split.
- simpl. omega.
- intros n L. simpl. rewrite drop_correct.
rewrite prepend_string_rest by omega. f_equal. omega.
Qed.
Lemma concat_extract w i_1 i_2 i_3: i_1 < i_2 -> i_2 < i_3 -> (extract i_1 i_2 w) ++ (extract i_2 i_3 w) == extract i_1 i_3 w.
Proof.
intros L1 L2. split.
- comega.
- intros n L.
decide (n <= (i_2 - S i_1)) as [D|D].
+ now rewrite concat_string_begin by comega.
+ rewrite concat_string_rest by comega.
unfold extract. cbn. repeat rewrite drop_correct. f_equal. omega.
Qed.
Lemma extract_from_drop w n m k: (extract n m (drop k w)) == (extract (n + k) (m + k) w).
Proof.
repeat split; cbn; oauto.
intros i B. simpl. repeat rewrite drop_correct. f_equal. omega.
Qed.
Lemma extract_from_drop' w n m k: k <=n-> (extract (n-k) (m-k) (drop k w)) == (extract n m w).
Proof.
intros L. split; cbn; oauto.
intros i B. simpl. repeat rewrite drop_correct. f_equal. omega.
Qed.
Lemma drop_extract w n m: (extract n (S m) w) == drop_string_begin n (mkstring w m).
Proof.
split; auto.
Qed.
Lemma extract_prepend v w n m : (extract (n + S (| v |)) (m + S (| v |)) (v +++ w )) == extract n m w.
Proof.
split.
- cbn. omega.
- intros k L. cbn. cbn in L. rewrite !drop_correct.
rewrite prepend_string_rest by comega. f_equal. omega.
Qed.
Lemma cut_string_cut i j w k: i < j <= k -> cut_string i j (mkstring w k) == (mkstring (cut i j w) (S k - j + i)).
Proof.
intros L. split.
- cbn. destruct j; omega.
- now intros.
Qed.
Lemma cut_front n m w : forall k, k <= n -> (cut n m w) k = w k.
Proof.
intros k L. unfold cut. now rewrite prepend_string_begin.
Qed.
Lemma cut_rest n m w: forall k, (cut n m w) (S n + k) = w (m + k).
Proof.
intros k. unfold cut. now rewrite prepend_string_rest', drop_correct.
Qed.
End StringOperationLemmas.
Instance seq_eq_index (X:Type) n: Proper (@seq_equal X ==> eq) (fun w => w n).
Proof.
intros w w' Ew . apply Ew.
Qed.
Instance drop_proper (X:Type): Proper (eq ==> @seq_equal X ==> @seq_equal X) drop.
Proof.
intros n n' En w w' Ew k.
rewrite !drop_correct. subst n. now apply Ew.
Qed.
Instance prepend_string_proper (X:Type): Proper (@strings_equal X ==> @seq_equal X ==> @seq_equal X) (fun v w => v +++ w).
Proof.
intros v v' [EvL Ev] w w' Ew n. decide (n <= |v|).
- repeat rewrite prepend_string_begin by (try rewrite <- EvL; auto). now apply Ev.
- repeat rewrite prepend_string_rest by (try rewrite <- EvL; omega). rewrite <-EvL. apply Ew.
Qed.
Instance prepend_string_proper_index (X:Type): Proper (@strings_equal X ==> @seq_equal X ==> @eq nat ==> @eq X) (fun v w n=> (v +++ w) n).
Proof.
intros v v' [EvL Ev] w w' Ew n n' En. subst n'. decide (n <= |v|).
- repeat rewrite prepend_string_begin by (try rewrite <- EvL; auto). now apply Ev.
- repeat rewrite prepend_string_rest by (try rewrite <- EvL; omega). rewrite <-EvL. apply Ew.
Qed.
Instance cancat_strings_proper (X:Type): Proper (@strings_equal X ==> @strings_equal X ==> @strings_equal X) (@concat_strings X).
Proof.
intros u u' [Eu1 Eu2] v v' [Ev1 Ev2]. split.
- cbn. rewrite Eu1, Ev1. omega.
- intros n L. decide (n <= |u|).
+ repeat rewrite concat_string_begin by (try rewrite <-Eu1; auto). now apply Eu2.
+ repeat rewrite concat_string_rest by (try rewrite <-Ev1; omega). rewrite <-Eu1. apply Ev2. cbn in L. omega.
Qed.
Instance extract_proper (X:Type) : Proper (eq ==> eq ==> (@seq_equal X) ==> strings_equal) extract.
Proof.
intros n n' <- m m' <- w w' Ew. split; auto.
intros k L. cbn. now rewrite !drop_correct, Ew.
Qed.
Section FiniteIterationOfString.
Context {X:Type}.
Implicit Type (u v t : String X).
Fixpoint fin_iter v n := match n with
| 0 => v
| S n => v ++ (fin_iter v n)
end.
Lemma fin_iter_step v n : fin_iter v (S n) == v ++ (fin_iter v n).
Proof.
reflexivity.
Qed.
Lemma fin_iter_base v : fin_iter v 0 == v.
Proof.
reflexivity.
Qed.
Lemma fin_iter_split u v n: fin_iter (u++v) (S n) == u ++ (fin_iter (v ++ u) n) ++ v.
Proof.
induction n; cbn.
- now rewrite !concat_strings_associative.
- rewrite IHn. now rewrite !concat_strings_associative.
Qed.
Lemma fin_iter_length v n : |fin_iter v n| = S n * S (|v|) - 1.
Proof.
induction n; cbn.
- omega.
- rewrite IHn. rewrite Nat.mul_succ_l. remember (n * S(|v|)) as Z. omega.
Qed.
Lemma fin_iter_length_bound v n : n <= |fin_iter v n| .
Proof.
induction n; cbn; omega.
Qed.
Lemma fin_iter_sum v n m : fin_iter v (S n + m) == (fin_iter v n) ++ (fin_iter v m).
Proof.
induction n.
- reflexivity.
- rewrite_eq (S (S n) + m = S (S n + m)). rewrite fin_iter_step. rewrite IHn. cbn. now rewrite concat_strings_associative.
Qed.
Lemma fin_iter_fin_iter v n m : (fin_iter (fin_iter v n) m) == (fin_iter v (S m * S n -1)).
Proof.
induction m; cbn.
- now rewrite_eq (n + 0 - 0= n).
- rewrite IHm. cbn. rewrite <-fin_iter_sum.
remember (m * S n) as Z. now rewrite_eq (S n + (n + Z - 0) = n + S(n + Z) - 0).
Qed.
End FiniteIterationOfString.
Section StrictlyMonotoneSeqs.
Implicit Types (f: Seq nat).
Definition s_monotone (f: Seq nat):= forall n, f n < f ( S n).
Lemma s_monotone_id : s_monotone (fun n => n).
Proof.
intros n. omega.
Qed.
Lemma s_monotone_unbouded_ge (f: Seq nat): s_monotone f -> (forall n, Sigma i, f i > n).
Proof.
intros A n.
induction n.
- exists 1. specialize (A 0). omega.
- destruct IHn as [n' P].
exists (S n').
specialize (A n'). omega.
Qed.
Lemma s_monotone_unbouded (f: Seq nat): s_monotone f ->
(forall n, Sigma i, f i >= n).
Proof.
intros A n.
destruct (s_monotone_unbouded_ge A n) as [i P].
exists i. omega.
Qed.
Lemma s_monotone_ge f: s_monotone f -> forall n, n <= f n.
Proof.
intros F n.
induction n.
- omega.
- specialize (F n). omega.
Qed.
Lemma s_monotone_strict_order_preserving' f k m : s_monotone f -> f k < f (m + S k).
Proof.
intros F. induction m; cbn.
- apply F.
- specialize (F (m + S k)). omega.
Qed.
Lemma s_monotone_strict_order_preserving f k n: s_monotone f -> k < n -> f k < f n.
Proof.
intros F L.
remember (n - S k) as z. assert (n = z + S k) by omega. subst n.
now apply s_monotone_strict_order_preserving'.
Qed.
Lemma s_monotone_order_preserving f k n: s_monotone f -> k <= n -> f k <= f n.
Proof.
intros F L.
decide (k = n).
- subst n. omega.
- enough (f k < f n) by omega.
apply s_monotone_strict_order_preserving; oauto.
Qed.
Lemma s_monotone_order_preserving_backwards f k n: s_monotone f -> f k <= f n -> k <= n.
Proof.
intros F L.
decide (k <= n).
- auto.
- exfalso.
assert (n < k) as H by omega.
apply s_monotone_order_preserving with (f:=f) in H; auto.
specialize (F n). omega.
Qed.
Lemma s_monotone_ge_zero g: s_monotone g -> g 0 > 0 -> forall n, g n > 0.
Proof.
intros Inc GZ. intros n. destruct n; auto.
- enough (g (S n) >= S n) by omega. now apply s_monotone_ge.
Qed.
Lemma s_monotone_ge_zero' g: s_monotone g -> forall n, 1 <= n -> g n > 0.
Proof.
intros Inc n G. pose (s_monotone_ge Inc n ). omega.
Qed.
Lemma s_monotone_drop g k : s_monotone g -> s_monotone (drop k g).
Proof.
intros Inc n. repeat rewrite drop_correct'. apply Inc.
Qed.
Chaining strictly monotone sequences preserves strict monotonicity.
Lemma compose_s_monotone f g: s_monotone f -> s_monotone g -> s_monotone (fun n => g ( f n)).
Proof.
intros F G n.
apply s_monotone_strict_order_preserving; auto.
Qed.
Proof.
intros F G n.
apply s_monotone_strict_order_preserving; auto.
Qed.
For a given function f, fix f 0 = 0. This preserves strict monotonicity.
Definition fix_first_zero (f:nat -> nat) := fun n => match n with
| 0 => 0
| S n => f (S n) end.
Lemma fix_first_zero_s_monotone f : s_monotone f -> s_monotone (fix_first_zero f).
Proof.
intros IncF n. destruct n; simpl.
- specialize (IncF 0). omega.
- apply IncF.
Qed.
End StrictlyMonotoneSeqs.
| 0 => 0
| S n => f (S n) end.
Lemma fix_first_zero_s_monotone f : s_monotone f -> s_monotone (fix_first_zero f).
Proof.
intros IncF n. destruct n; simpl.
- specialize (IncF 0). omega.
- apply IncF.
Qed.
End StrictlyMonotoneSeqs.
Helper function which translates the indices: it returns a tuple (w, i) such that
(f w) [i] is the desired character at index n
Fixpoint concat_inf_indices f n := match n with
| 0 => (0,0)
| S n => match (concat_inf_indices f n) with (i, j) =>
if (decision (j = |f i|))
then (S i, 0)
else (i , S j) end end.
Definition concat_inf f : Seq X := fun n =>
(f (fst (concat_inf_indices f n )))[snd (concat_inf_indices f n)].
| 0 => (0,0)
| S n => match (concat_inf_indices f n) with (i, j) =>
if (decision (j = |f i|))
then (S i, 0)
else (i , S j) end end.
Definition concat_inf f : Seq X := fun n =>
(f (fst (concat_inf_indices f n )))[snd (concat_inf_indices f n)].
Calculates the begin index of (f n) in (concat_inf f)
Fixpoint begin_in f n := match n with
|0 => 0
|S n => S (| f n|) + (begin_in f n) end.
Lemma s_monotone_begin_in f: s_monotone (begin_in f).
Proof.
intros n. cbn. omega.
Qed.
|0 => 0
|S n => S (| f n|) + (begin_in f n) end.
Lemma s_monotone_begin_in f: s_monotone (begin_in f).
Proof.
intros n. cbn. omega.
Qed.
Various correctness lemmata
Lemma concat_inf_index_in_string f i n : concat_inf_indices f n = (i, 0) ->
forall k, k <= |f i| -> concat_inf_indices f (k + n) = (i , k).
Proof.
intros C.
apply (complete_induction (P:= fun k => (k <= |f i| -> concat_inf_indices f (k + n) = (i, k)))).
- auto.
- intros k IHk L. cbn.
rewrite IHk by omega.
destruct decision.
+ exfalso. omega.
+ reflexivity.
Qed.
Lemma concat_inf_index_begin f i: concat_inf_indices f (begin_in f i) = (i, 0).
Proof.
induction i ; cbn.
- reflexivity.
- rewrite concat_inf_index_in_string with (i:=i) by auto.
now trivial_decision.
Qed.
Lemma concat_inf_index_correct f i k: k <= |f i| -> concat_inf_indices f (k + begin_in f i) = (i, k).
Proof.
intros L.
apply concat_inf_index_in_string ; auto.
now apply concat_inf_index_begin.
Qed.
Lemma concat_inf_index_in_bounds f n i k : concat_inf_indices f n = (i , k) -> k <= |f i|.
Proof.
revert i; revert k.
induction n; intros k i C; cbn in C.
- assert (k = 0) as H by congruence.
rewrite H. omega.
- destruct (concat_inf_indices f n) as [i' k'] eqn:H.
destruct decision.
+ assert (k = 0) by congruence. subst k. omega.
+ assert (i' = i) by congruence. subst i.
assert (S k' = k) by congruence. subst k.
enough (k' <= |f i'|) by omega. auto.
Qed.
Lemma concat_inf_index_step_correct f n i k: concat_inf_indices f n = (i, k) ->
concat_inf_indices f (S n) = (i, (S k)) \/
(concat_inf_indices f (S n) = (S i, 0) /\ k = |f i|).
Proof.
intros L. cbn. rewrite L.
destruct decision; tauto.
Qed.
To show that concat_inf_indices is injective, we define the lexicographical order on pairs of natural numbers
and show that concat_inf_indices is strictly s_monotone
Definition nat_pair_le (x y : nat * nat) := (fst x < fst y) \/ (fst x = fst y /\ (snd x < snd y)).
Lemma nat_pair_le_not_equal (x y: nat * nat):nat_pair_le x y -> x <> y.
Proof.
intros E. unfold nat_pair_le in E. destruct x, y. cbn in E. destruct E.
- assert (n <> n1) by omega. congruence.
- assert (n0 <> n2) by omega. congruence.
Qed.
Lemma concat_inf_index_le f n m: n < m -> nat_pair_le (concat_inf_indices f n) (concat_inf_indices f m) .
Proof.
intros L. induction L; cbn.
- destruct (concat_inf_indices f n), decision; [left | right]; cbn; omega.
- destruct (concat_inf_indices f n) as [w i]; destruct (concat_inf_indices f m) as [w' i'].
destruct decision; unfold nat_pair_le in IHL; simpl in IHL; unfold nat_pair_le; simpl; omega.
Qed.
Lemma concat_if_indices_lower_bound f m n: m >= begin_in f n -> fst (concat_inf_indices f m) >= n.
Proof.
intros H'.
destruct (concat_inf_indices f m) as [w i] eqn:H.
decide (m = begin_in f n).
+ subst m. rewrite concat_inf_index_begin in H. cbn.
enough (w = n) by omega. congruence.
+ assert (begin_in f n < m) as D by omega.
pose proof (concat_inf_index_le f D) as Z.
rewrite concat_inf_index_begin,H in Z.
compute in Z. cbn. omega.
Qed.
Lemma concat_inf_index_injective f n n' : concat_inf_indices f n = concat_inf_indices f n' -> n = n'.
Proof.
decide (n = n').
- auto.
- intros H. exfalso. decide (n < n') as [D|D].
+ now apply (nat_pair_le_not_equal (concat_inf_index_le f D)).
+ assert (n' < n) as D' by omega.
now apply (nat_pair_le_not_equal (concat_inf_index_le f D')).
Qed.
Lemma concat_inf_index_to_begin f n i k : concat_inf_indices f n = (i, k) -> n = (begin_in f i) + k /\ (n < begin_in f (S i)).
Proof.
intros C.
assert ( k <= |f i|) by apply (concat_inf_index_in_bounds C).
rewrite <- (concat_inf_index_correct (f:=f)) in C by now apply concat_inf_index_in_bounds with (n:=n).
apply concat_inf_index_injective with (n:=n) in C.
split; cbn; oauto.
Qed.
Lemma concat_inf_correct f i k : k <= |f i| -> concat_inf f (k + (begin_in f i)) = (f i) [k].
Proof.
unfold concat_inf. intros L.
now rewrite concat_inf_index_correct.
Qed.
End InfiniteConcat.
Lemma begin_in_equal (X Y: Type) (f: Seq (String X)) (g:Seq (String Y)):
(forall n , |f n| = |g n|) -> begin_in f === begin_in g.
Proof.
intros EL n. induction n.
- reflexivity.
- cbn. now rewrite <-IHn, EL.
Qed.
Lemma concat_inf_index_equal (X Y: Type) (f: Seq (String X)) (g:Seq (String Y)):
(forall n , |f n| = |g n|) -> concat_inf_indices f === concat_inf_indices g.
Proof.
intros EL n. induction n.
- reflexivity.
- cbn. rewrite <-IHn.
destruct (concat_inf_indices f n) as [wi i].
now rewrite <-(EL wi).
Qed.
Lemma concat_inf_extensional (X:Type) (f f': Seq (String X)): (forall n, (f n == f' n)) -> concat_inf f === concat_inf f'.
Proof.
intros E n.
unfold concat_inf. rewrite <-concat_inf_index_equal with (f:=f)(g:=f').
- apply E. destruct (concat_inf_indices f n) eqn:H. now apply concat_inf_index_in_bounds in H.
- intros m. apply E.
Qed.
Lemma extract_concat_inf (X:Type) (W: Seq (String X)) n : extract (begin_in W n ) (begin_in W (S n) ) (concat_inf W) == W n.
Proof.
split.
- cbn. omega.
- intros m L. cbn. cbn in L. rewrite drop_correct.
now rewrite Nat.add_comm, concat_inf_correct by omega.
Qed.
Lemma nat_pair_le_not_equal (x y: nat * nat):nat_pair_le x y -> x <> y.
Proof.
intros E. unfold nat_pair_le in E. destruct x, y. cbn in E. destruct E.
- assert (n <> n1) by omega. congruence.
- assert (n0 <> n2) by omega. congruence.
Qed.
Lemma concat_inf_index_le f n m: n < m -> nat_pair_le (concat_inf_indices f n) (concat_inf_indices f m) .
Proof.
intros L. induction L; cbn.
- destruct (concat_inf_indices f n), decision; [left | right]; cbn; omega.
- destruct (concat_inf_indices f n) as [w i]; destruct (concat_inf_indices f m) as [w' i'].
destruct decision; unfold nat_pair_le in IHL; simpl in IHL; unfold nat_pair_le; simpl; omega.
Qed.
Lemma concat_if_indices_lower_bound f m n: m >= begin_in f n -> fst (concat_inf_indices f m) >= n.
Proof.
intros H'.
destruct (concat_inf_indices f m) as [w i] eqn:H.
decide (m = begin_in f n).
+ subst m. rewrite concat_inf_index_begin in H. cbn.
enough (w = n) by omega. congruence.
+ assert (begin_in f n < m) as D by omega.
pose proof (concat_inf_index_le f D) as Z.
rewrite concat_inf_index_begin,H in Z.
compute in Z. cbn. omega.
Qed.
Lemma concat_inf_index_injective f n n' : concat_inf_indices f n = concat_inf_indices f n' -> n = n'.
Proof.
decide (n = n').
- auto.
- intros H. exfalso. decide (n < n') as [D|D].
+ now apply (nat_pair_le_not_equal (concat_inf_index_le f D)).
+ assert (n' < n) as D' by omega.
now apply (nat_pair_le_not_equal (concat_inf_index_le f D')).
Qed.
Lemma concat_inf_index_to_begin f n i k : concat_inf_indices f n = (i, k) -> n = (begin_in f i) + k /\ (n < begin_in f (S i)).
Proof.
intros C.
assert ( k <= |f i|) by apply (concat_inf_index_in_bounds C).
rewrite <- (concat_inf_index_correct (f:=f)) in C by now apply concat_inf_index_in_bounds with (n:=n).
apply concat_inf_index_injective with (n:=n) in C.
split; cbn; oauto.
Qed.
Lemma concat_inf_correct f i k : k <= |f i| -> concat_inf f (k + (begin_in f i)) = (f i) [k].
Proof.
unfold concat_inf. intros L.
now rewrite concat_inf_index_correct.
Qed.
End InfiniteConcat.
Lemma begin_in_equal (X Y: Type) (f: Seq (String X)) (g:Seq (String Y)):
(forall n , |f n| = |g n|) -> begin_in f === begin_in g.
Proof.
intros EL n. induction n.
- reflexivity.
- cbn. now rewrite <-IHn, EL.
Qed.
Lemma concat_inf_index_equal (X Y: Type) (f: Seq (String X)) (g:Seq (String Y)):
(forall n , |f n| = |g n|) -> concat_inf_indices f === concat_inf_indices g.
Proof.
intros EL n. induction n.
- reflexivity.
- cbn. rewrite <-IHn.
destruct (concat_inf_indices f n) as [wi i].
now rewrite <-(EL wi).
Qed.
Lemma concat_inf_extensional (X:Type) (f f': Seq (String X)): (forall n, (f n == f' n)) -> concat_inf f === concat_inf f'.
Proof.
intros E n.
unfold concat_inf. rewrite <-concat_inf_index_equal with (f:=f)(g:=f').
- apply E. destruct (concat_inf_indices f n) eqn:H. now apply concat_inf_index_in_bounds in H.
- intros m. apply E.
Qed.
Lemma extract_concat_inf (X:Type) (W: Seq (String X)) n : extract (begin_in W n ) (begin_in W (S n) ) (concat_inf W) == W n.
Proof.
split.
- cbn. omega.
- intros m L. cbn. cbn in L. rewrite drop_correct.
now rewrite Nat.add_comm, concat_inf_correct by omega.
Qed.
Definition omega_iteration (X: Type) (u:String X) := concat_inf (fun _ => u).
Notation " w 'to_omega'" := (omega_iteration w) (at level 50).
Lemma omega_iteration_extensional (X:Type) (u v: String X) : u == v -> u to_omega === v to_omega.
Proof.
unfold omega_iteration. intros E. now apply concat_inf_extensional.
Qed.
Instance omega_iteration_proper X: Proper (@strings_equal X ==> @seq_equal X) (@omega_iteration X).
Proof.
intros A B D. now apply omega_iteration_extensional.
Qed.
Instance omega_iteration_proper_index X: Proper (@strings_equal X ==> eq ==> eq) (fun w n=> (@omega_iteration X w n)).
Proof.
intros A B E. intros n m D. rewrite D. now apply omega_iteration_extensional.
Qed.
Lemma extract_omega_iter (X:Type) (v: String X) k: extract (k *S(|v|) )((S k) * S(|v|) ) (v to_omega) == v.
Proof.
unfold omega_iteration.
assert (forall k, begin_in (fun _ => v) k = k * S(|v|))as H. {
clear k. intros k. induction k.
- reflexivity.
- simpl. rewrite IHk. reflexivity. }
rewrite <-2H.
apply extract_concat_inf.
Qed.
Section OmegaIteration.
Context {X:Type}.
Implicit Type t u v: String X.
Implicit Type w: Seq X.
Lemma concat_inf_indices_step (f: Seq (String X)) n: concat_inf_indices f (S n) = match (concat_inf_indices f n) with (i, j) =>
if (decision (j = |f i|))
then (S i, 0)
else (i , S j) end.
Proof. reflexivity. Qed.
Lemma concat_inf_indices_constant_first v i: i <= |v| -> i = snd (concat_inf_indices (fun _ => v) (i)).
Proof.
intros L. induction i.
- reflexivity.
- cbn. destruct concat_inf_indices. cbn in IHi. rewrite IHi; oauto. destruct decision as [D|D].
+ exfalso. rewrite <-IHi in D; oauto.
+ reflexivity.
Qed.
Lemma concat_inf_indices_constant_step v n : snd (concat_inf_indices (fun _ => v) n) = snd (concat_inf_indices (fun _ => v) (n + S(|v|))).
Proof.
induction n.
- cbn. destruct concat_inf_indices as [i j] eqn:H. rewrite decision_true.
+ reflexivity.
+ change (snd (i,j) = |v|). rewrite <-H. rewrite <-concat_inf_indices_constant_first; oauto.
- cbn. destruct (concat_inf_indices (fun _ : nat => v) n). destruct (concat_inf_indices (fun _ : nat => v) (n + S (| v |))).
cbn in IHn. rewrite IHn. now destruct decision.
Qed.
Lemma concat_inf_indices_constant_step' v n : n > |v| -> snd (concat_inf_indices (fun _ => v) n) = snd (concat_inf_indices (fun _ => v) (n - S(|v|))).
Proof.
intros L. remember (n - S(|v|)) as Z. rewrite_eq (n = Z + S(|v|)).
symmetry. apply concat_inf_indices_constant_step.
Qed.
Lemma vv_omega_unfold v : (v to_omega) === v +++ (v to_omega).
Proof.
intros n. unfold omega_iteration, concat_inf. cbn.
decide (n<= |v|).
- rewrite prepend_string_begin by auto. f_equal. symmetry.
now apply concat_inf_indices_constant_first.
- rewrite prepend_string_rest by omega. f_equal.
apply concat_inf_indices_constant_step'. omega.
Qed.
Lemma omega_iter_first v n: n <= |v| -> (v to_omega) n = v [n].
Proof.
intros L. rewrite vv_omega_unfold.
now rewrite prepend_string_begin by omega.
Qed.
Lemma omega_iter_first_new v : (v to_omega) (S(|v|)) = v[0].
Proof.
rewrite vv_omega_unfold. rewrite prepend_string_rest by omega.
rewrite omega_iter_first by omega. f_equal. omega.
Qed.
Lemma omega_iter_unfold v n : (v to_omega) === (fin_iter v n) +++ (v to_omega).
Proof.
induction n.
- apply vv_omega_unfold.
- rewrite fin_iter_step, concat_prepend_string_associative, <-IHn.
apply vv_omega_unfold.
Qed.
Lemma eq_string_access (v v': String X) n: n <= |v| -> v == v' -> v[n] = v'[n].
Proof.
intros L [E1 E2]. now apply E2.
Qed.
Lemma eq_string_access' (v v': String X) n: v == v' -> n <= |v| -> v[n] = v'[n].
Proof.
intros [E1 E2] L. now apply E2.
Qed.
Lemma nat_equation_1 n m: S m * S (S n) - 1 = S m + (S m * S n - 1).
Proof.
rewrite Nat.mul_succ_r, plus_comm.
remember (S m * S n) as Z. assert (Z > 0) by (subst Z ; apply mul_ge_0; omega).
now rewrite_eq ( S m + Z - 1 = S m + (Z - 1)).
Qed.
Lemma fin_iter_to_omega v n: v to_omega === (fin_iter v n) to_omega.
Proof.
induction n.
- reflexivity.
- intros m.
rewrite (omega_iter_unfold v m). rewrite (omega_iter_unfold (fin_iter v (S n)) m).
repeat rewrite prepend_string_begin by apply fin_iter_length_bound. symmetry.
rewrite eq_string_access with (v':= (fin_iter v m) ++ (fin_iter v (S m * (S n) -1))).
+ now rewrite concat_string_begin by apply fin_iter_length_bound.
+ apply fin_iter_length_bound.
+ now rewrite fin_iter_fin_iter, <-fin_iter_sum, nat_equation_1.
Qed.
Lemma fin_iter_index v n k l: l <= |v| -> k <= n -> (fin_iter v n) [k * (S (|v|)) + l] = v [l].
Proof.
intros Ll. revert k. induction n; intros k Lk.
- cbn. now rewrite_eq (k = 0).
- rewrite (eq_string_access' (fin_iter_step v n)).
+ destruct k.
* rewrite concat_string_begin; cbn; oauto.
* rewrite concat_string_rest.
-- cbn. rewrite <-IHn with (k := k) by omega. f_equal.
remember (k * S(|v|))as Z. omega.
-- enough (S k * S (| v |) > |v|) by omega.
cbn. remember (k * S (| v |)) as Z. omega.
+ rewrite fin_iter_length, Nat.mul_succ_l.
enough (k * S(|v|) <= S n * S(|v|)) by omega.
apply Nat.mul_le_mono_nonneg_r; omega.
Qed.
Lemma fin_iter_last_index v n k: 0 < k <= S n -> (fin_iter v n) [k * S(|v|) - 1] = v[|v|].
Proof.
intros L.
destruct k. {exfalso. omega. }
rewrite Nat.mul_succ_l.
remember (k * S(|v|)) as C. rewrite_eq (C + S (| v |) - 1 = C + |v|). subst C.
apply fin_iter_index; omega.
Qed.
Lemma le_add k n m : k <= n -> k <= n + m.
Proof. omega. Qed.
Lemma concat_strings_omega_unfold u v : (u ++ v) to_omega === u +++ (v ++ u) to_omega.
Proof.
intros m.
decide (m <= |u|) as [D|D].
- rewrite (omega_iter_unfold (u ++ v) m).
rewrite prepend_string_begin by apply fin_iter_length_bound.
rewrite prepend_string_begin by auto.
destruct m.
+ cbn. now rewrite prepend_string_begin.
+ assert (fin_iter (u ++ v) (S m) == (u ++ v) ++ (fin_iter (u++v) m)) as H. { now rewrite fin_iter_step. }
rewrite eq_string_access with(v':=(u ++ v) ++ (fin_iter (u++v) m)).
* now repeat rewrite concat_string_begin by (cbn;omega).
* apply fin_iter_length_bound.
* now rewrite fin_iter_step.
- rewrite (omega_iter_unfold (u++v) (S m)).
rewrite (omega_iter_unfold (v++u) (S m)).
rewrite prepend_string_begin by (rewrite <-fin_iter_length_bound; omega).
rewrite prepend_string_rest by omega.
rewrite prepend_string_begin by (rewrite <-fin_iter_length_bound; omega).
rewrite <-concat_string_rest by omega.
rewrite <-concat_string_begin with (v0:= u) by (rewrite <-fin_iter_length_bound; omega).
apply eq_string_access.
+ rewrite concat_strings_length. apply le_add. rewrite <-fin_iter_length_bound. omega.
+ rewrite (fin_iter_split v u).
repeat rewrite <-concat_strings_associative.
now rewrite <-fin_iter_step.
Qed.
End OmegaIteration.
Definition infiniteP X (P: X -> Prop) (w: Seq X) := forall n, exists m, m >= n /\ P (w m).
Section Infinite.
Context {X:Type}.
Implicit Types (w: Seq X) (v: String X) (x:X).
Notation infinite x w := (infiniteP (fun y => y = x) w).
Lemma finite_prefix_preserves_infiniteP v w P: infiniteP P w -> infiniteP P (v +++ w).
Proof.
intros I n. destruct (I n) as [m [L Q]].
exists (S (|v|) + m). split.
- omega.
- now rewrite prepend_string_rest'.
Qed.
Lemma finite_prefix_preserves_infinite x v w : infinite x w -> infinite x (v +++ w) .
Proof. apply finite_prefix_preserves_infiniteP. Qed.
Lemma drop_preserves_infiniteP w P n: infiniteP P w -> infiniteP P (drop n w).
Proof.
intros I k. destruct (I (k+n)) as [m [L Q]].
exists (m-n). split.
- omega.
- rewrite drop_correct''; oauto.
Qed.
Lemma drop_preserves_infinite s w n: infinite s w -> infinite s (drop n w).
Proof. apply drop_preserves_infiniteP. Qed.
Definition holdsIn P v:= exists k, k <= |v| /\ P (v[k]).
Implicit Types (f: Seq (String X)).
Lemma concat_inf_infiniteP P f:
infiniteP (holdsIn P) f -> infiniteP P (concat_inf f) .
Proof.
intros F.
intros n. destruct (F n) as [m [L [k [L' Fin]]]].
exists (k + (begin_in f m) ). split.
- enough (begin_in f m >= m) by omega.
apply s_monotone_ge, s_monotone_begin_in.
- now rewrite concat_inf_correct.
Qed.
Lemma concat_inf_infiniteP_inverse P f:
infiniteP P (concat_inf f) -> infiniteP (holdsIn P) f.
Proof.
intros Fin n. destruct (Fin (begin_in f n)) as [m [E Q]].
unfold concat_inf in Q. destruct (concat_inf_indices f m) as [w i]eqn:H.
exists w. split.
- apply concat_if_indices_lower_bound in E.
now rewrite H in E.
- exists i. split.
+ apply (concat_inf_index_in_bounds H).
+ assumption.
Qed.
Lemma omega_iteration_infiniteP P v: holdsIn P v -> infiniteP P (v to_omega).
Proof.
intros H. unfold omega_iteration. apply concat_inf_infiniteP.
intros m. exists m. split; oauto.
Qed.
Global Instance infiniteP_proper {P}: Proper (@seq_equal X ==> iff) (infiniteP P).
Proof.
intros w w' E. split; intros I n; destruct (I n) as [m Q]; exists m; [rewrite <-E | rewrite E]; auto.
Qed.
End Infinite.
Notation infinite x w := (infiniteP (fun y => y = x) w).
Section Infinite.
Context {X:Type}.
Implicit Types (w: Seq X) (v: String X) (x:X).
Notation infinite x w := (infiniteP (fun y => y = x) w).
Lemma finite_prefix_preserves_infiniteP v w P: infiniteP P w -> infiniteP P (v +++ w).
Proof.
intros I n. destruct (I n) as [m [L Q]].
exists (S (|v|) + m). split.
- omega.
- now rewrite prepend_string_rest'.
Qed.
Lemma finite_prefix_preserves_infinite x v w : infinite x w -> infinite x (v +++ w) .
Proof. apply finite_prefix_preserves_infiniteP. Qed.
Lemma drop_preserves_infiniteP w P n: infiniteP P w -> infiniteP P (drop n w).
Proof.
intros I k. destruct (I (k+n)) as [m [L Q]].
exists (m-n). split.
- omega.
- rewrite drop_correct''; oauto.
Qed.
Lemma drop_preserves_infinite s w n: infinite s w -> infinite s (drop n w).
Proof. apply drop_preserves_infiniteP. Qed.
Definition holdsIn P v:= exists k, k <= |v| /\ P (v[k]).
Implicit Types (f: Seq (String X)).
Lemma concat_inf_infiniteP P f:
infiniteP (holdsIn P) f -> infiniteP P (concat_inf f) .
Proof.
intros F.
intros n. destruct (F n) as [m [L [k [L' Fin]]]].
exists (k + (begin_in f m) ). split.
- enough (begin_in f m >= m) by omega.
apply s_monotone_ge, s_monotone_begin_in.
- now rewrite concat_inf_correct.
Qed.
Lemma concat_inf_infiniteP_inverse P f:
infiniteP P (concat_inf f) -> infiniteP (holdsIn P) f.
Proof.
intros Fin n. destruct (Fin (begin_in f n)) as [m [E Q]].
unfold concat_inf in Q. destruct (concat_inf_indices f m) as [w i]eqn:H.
exists w. split.
- apply concat_if_indices_lower_bound in E.
now rewrite H in E.
- exists i. split.
+ apply (concat_inf_index_in_bounds H).
+ assumption.
Qed.
Lemma omega_iteration_infiniteP P v: holdsIn P v -> infiniteP P (v to_omega).
Proof.
intros H. unfold omega_iteration. apply concat_inf_infiniteP.
intros m. exists m. split; oauto.
Qed.
Global Instance infiniteP_proper {P}: Proper (@seq_equal X ==> iff) (infiniteP P).
Proof.
intros w w' E. split; intros I n; destruct (I n) as [m Q]; exists m; [rewrite <-E | rewrite E]; auto.
Qed.
End Infinite.
Notation infinite x w := (infiniteP (fun y => y = x) w).
Given a sequence w on a type X, a decidable predicate on X, a number n and a proof that P holds at some m, n <= m,
we can construct the smallest greater equal n, at which P holds.
Define a function which gives the next index in the sequence starting at a given one
that fulfills the predicate
Section NextPosition.
Context {n m : nat}.
Variable (L : n <= m).
Variable (F : P (w m)).
Definition next_position: nat.
Proof.
pose (P' := fun j => P ((drop n w) j)).
assert(exists j, P' j) as H. { exists (m - n). subst P'. cbn. rewrite drop_correct. now rewrite_eq (n + (m - n) = m). }
apply cc_nat_first in H.
destruct H as [k _].
exact (n + k). auto.
Defined.
Lemma next_position_correct : P (w next_position).
Proof.
unfold next_position. cbn. destruct cc_nat_first as [k [Q _]]. now rewrite drop_correct in Q.
Qed.
Lemma next_position_bounds : n <= next_position <= m.
Proof.
unfold next_position. cbn. destruct cc_nat_first as [k [_ Q]]. split; oauto.
decide (n + k <= m); auto. exfalso.
specialize (Q (m-n)). apply Q; oauto. rewrite drop_correct. now rewrite_eq (n + (m - n) = m).
Qed.
Lemma next_position_all : forall j, n <= j < next_position -> ~ P(w j).
Proof.
unfold next_position. cbn. destruct cc_nat_first as [k [_ Q]].
intros j L'. specialize (Q (j - n)). rewrite drop_correct in Q.
rewrite_eq (n + (j - n) = j) in Q. apply Q. omega.
Qed.
Lemma can_find_next_position: (Sigma k, n <=k<=m /\ (P (w k)) /\ forall m', n <= m' < k -> ~(P (w m'))).
Proof.
exists next_position. auto using next_position_correct, next_position_bounds, next_position_all.
Qed.
End NextPosition.
Context {n m : nat}.
Variable (L : n <= m).
Variable (F : P (w m)).
Definition next_position: nat.
Proof.
pose (P' := fun j => P ((drop n w) j)).
assert(exists j, P' j) as H. { exists (m - n). subst P'. cbn. rewrite drop_correct. now rewrite_eq (n + (m - n) = m). }
apply cc_nat_first in H.
destruct H as [k _].
exact (n + k). auto.
Defined.
Lemma next_position_correct : P (w next_position).
Proof.
unfold next_position. cbn. destruct cc_nat_first as [k [Q _]]. now rewrite drop_correct in Q.
Qed.
Lemma next_position_bounds : n <= next_position <= m.
Proof.
unfold next_position. cbn. destruct cc_nat_first as [k [_ Q]]. split; oauto.
decide (n + k <= m); auto. exfalso.
specialize (Q (m-n)). apply Q; oauto. rewrite drop_correct. now rewrite_eq (n + (m - n) = m).
Qed.
Lemma next_position_all : forall j, n <= j < next_position -> ~ P(w j).
Proof.
unfold next_position. cbn. destruct cc_nat_first as [k [_ Q]].
intros j L'. specialize (Q (j - n)). rewrite drop_correct in Q.
rewrite_eq (n + (j - n) = j) in Q. apply Q. omega.
Qed.
Lemma can_find_next_position: (Sigma k, n <=k<=m /\ (P (w k)) /\ forall m', n <= m' < k -> ~(P (w m'))).
Proof.
exists next_position. auto using next_position_correct, next_position_bounds, next_position_all.
Qed.
End NextPosition.
Variant which requires m to be packed existentially
Section NextPositionExists.
Context{n: nat}.
Variable (L: exists m, n <= m /\ P (w m)).
Definition next_position_exists : nat.
Proof.
apply cc_nat in L. destruct L as [m [Q1 Q2]]. apply (next_position Q1 Q2). auto.
Defined.
Lemma next_position_exists_increasing : n <= next_position_exists.
Proof.
unfold next_position_exists. destruct cc_nat as [k [Q1 Q2]]. apply next_position_bounds.
Qed.
Lemma next_position_exists_correct: P (w (next_position_exists)).
Proof.
unfold next_position_exists. destruct cc_nat as [k [Q1 Q2]]. apply next_position_correct.
Qed.
Lemma next_position_exists_all : forall k, n <= k < next_position_exists -> ~ P (w k).
Proof.
unfold next_position_exists. destruct cc_nat as [k [Q1 Q2]]. apply next_position_all.
Qed.
End NextPositionExists.
End FindNextPosition.
Context{n: nat}.
Variable (L: exists m, n <= m /\ P (w m)).
Definition next_position_exists : nat.
Proof.
apply cc_nat in L. destruct L as [m [Q1 Q2]]. apply (next_position Q1 Q2). auto.
Defined.
Lemma next_position_exists_increasing : n <= next_position_exists.
Proof.
unfold next_position_exists. destruct cc_nat as [k [Q1 Q2]]. apply next_position_bounds.
Qed.
Lemma next_position_exists_correct: P (w (next_position_exists)).
Proof.
unfold next_position_exists. destruct cc_nat as [k [Q1 Q2]]. apply next_position_correct.
Qed.
Lemma next_position_exists_all : forall k, n <= k < next_position_exists -> ~ P (w k).
Proof.
unfold next_position_exists. destruct cc_nat as [k [Q1 Q2]]. apply next_position_all.
Qed.
End NextPositionExists.
End FindNextPosition.
Definition of the ω-Filter
Given a sequence w on a type X, a decidable predicate P on X and a proof that there are infinitely many
positions in w at which P holds, there is function infinite_filter : Seq nat which has the following
properties:
- infinite_filter gives a strictly monotone sequence
- P holds at all positions in w given by infinite_filter
- infinite_filter gives all positions in w, at which P holds
Context {X:Type}.
Variable (w: Seq X).
Variable (P : X -> Prop).
Context {decP: forall x, dec (P x)}.
Variable (infP: infiniteP P w).
Lemma ge_to_le n m : m >= n -> n <= m. Proof. omega. Qed.
Arguments cc_nat [p] [p_dec] _.
Arguments can_find_next_position [X] [P] [decP] [w] [n] [m] _ _.
Arguments next_position_exists [X] [P] [decP] [w] _ _.
Fixpoint infinite_filter (n : nat) : nat.
Proof.
induction n.
- apply (next_position_exists (w:=w) 0). apply infP.
- apply (next_position_exists (w:=w) (S(infinite_filter n))). apply infP.
Defined.
Lemma infinite_filter_s_monotone : s_monotone infinite_filter.
Proof.
intros n. cbn. pose (next_position_exists_increasing (infP (S (infinite_filter n)))). omega.
Qed.
Lemma infinite_filter_correct : (forall n, P ( w (infinite_filter n))).
Proof.
intros n. destruct n; cbn; apply next_position_exists_correct.
Qed.
Lemma infinite_filter_all n: forall k, infinite_filter n < k < infinite_filter (S n) -> ~ P (w k).
Proof.
simpl. apply next_position_exists_all.
Qed.
Lemma infinite_filter_zero: P (w 0) -> infinite_filter 0 = 0.
Proof.
intros P0. cbn. unfold next_position_exists. destruct cc_nat as [j [Q1 Q2]].
decide (next_position (X:=X) Q1 Q2 = 0); auto. exfalso.
eapply (next_position_all (X:=X) (L := Q1) (F:= Q2) (j := 0)(w:=w)); oauto.
Qed.
End InfiniteFilter.
Structure UPSeq (X:Type) := mkUPSeq
{ prefix: String X;
loop : String X
}.
Definition unfold (X:Type) (a :UPSeq X) := ((prefix a) +++ (loop a) to_omega).
Definition up_equal (X:Type) (a b: UPSeq X) := unfold a === unfold b.
Instance up_equal_Equivalence X :
Equivalence (@up_equal X).
Proof.
constructor.
- constructor.
- intros w_1 w_2 E n. now rewrite E.
- intros w_1 w_2 w_3 E_1 E_2 n. now rewrite <-E_2, E_1.
Qed.
Section UltimatelyPeriodicSequences.
Notation "a ==== b" := (up_equal a b) (at level 71).
Section Basic.
Context {X Y:Type}.
Implicit Types (u v : String X) (a b : UPSeq X).
Definition up_map (f: X -> Y) a : UPSeq Y := mkUPSeq (string_map f (prefix a)) (string_map f (loop a)).
Lemma up_map_correct (f: X -> Y) a: unfold (up_map f a) === seq_map f (unfold a).
Proof.
intros n. destruct a as [u v].
decide (n <= |u|) as [D|D]; unfold seq_map, unfold.
- now rewrite !prepend_string_begin by auto.
- rewrite !prepend_string_rest by comega. cbn. unfold seq_map. cbn. f_equal.
unfold omega_iteration, concat_inf. f_equal. f_equal. apply concat_inf_index_equal. auto.
Qed.
Lemma up_prefix u v: prefix (mkUPSeq u v) = u.
Proof. reflexivity. Qed.
Lemma up_loop u v: loop (mkUPSeq u v) = v.
Proof. reflexivity. Qed.
Global Instance unfold_proper: Proper (@up_equal X ==> @seq_equal X) (@unfold X).
Proof.
intros a b E. auto.
Qed.
Global Instance up_map_proper (f: X->Y) : Proper (@up_equal X ==> @up_equal Y) (fun a => up_map f a).
Proof.
intros a b E. unfold up_equal. rewrite !up_map_correct.
intros n. unfold seq_map. f_equal. apply E.
Qed.
End Basic.
Definition swap (X Y: Type) := fun (t:X * Y) => match t with (x,y) => (y,x) end.
Definition string_zip (X Y :Type) (v: String X) (u : String Y) : String (X * Y) := mkstring (seq_zip v u) (|v|).
Definition split_first (X:Type) (v: String X) k := (extract 0 k v).
Definition split_second (X:Type) (v: String X) k := (extract k (S (|v|)) v).
Lemma split_string_eq (X:Type) (v:String X) n : 0 < n <= |v| -> (split_first v n) ++ (split_second v n) == v.
Proof.
intros L. split.
- comega.
- intros k L'. decide (k < n).
+ now rewrite concat_string_begin by comega.
+ rewrite concat_string_rest by comega. cbn. rewrite drop_correct. f_equal. omega.
Qed.
Section StringZip.
Context{X Y: Type}.
Lemma string_zip_fst_up (u_1 v_1: String X) (u_2 v_2: String Y):
seq_map fst ((string_zip u_1 u_2) +++ (string_zip v_1 v_2) to_omega) === u_1 +++ v_1 to_omega.
Proof.
intros n. decide ( n <= |u_1|); unfold seq_map.
- now rewrite !prepend_string_begin by comega.
- rewrite !prepend_string_rest by comega. unfold omega_iteration, concat_inf. cbn.
f_equal. f_equal. now apply concat_inf_index_equal.
Qed.
Lemma string_zip_snd_up (u_1 v_1: String X) (u_2 v_2: String Y): |u_1| = |u_2| -> |v_1| = |v_2| ->
seq_map snd ((string_zip u_1 u_2) +++ (string_zip v_1 v_2) to_omega) === u_2 +++ v_2 to_omega.
Proof.
intros Lu Lv n. decide ( n <= |u_2|); unfold seq_map.
- now rewrite !prepend_string_begin by comega.
- rewrite !prepend_string_rest by comega. unfold omega_iteration, concat_inf. cbn.
f_equal. f_equal. rewrite Lu. now apply concat_inf_index_equal.
Qed.
End StringZip.
Section UPZip''.
Context {X Y : Type}.
Variables (a : UPSeq X) (b: UPSeq Y).
Notation split_pos := (|prefix a| - |prefix b|).
Notation loop'b := (fin_iter (loop b) (|prefix a|)).
Definition up_zip' : UPSeq Y :=
if (decision (|prefix a| = |prefix b|))
then b
else mkUPSeq (prefix b ++ split_first (loop'b) split_pos)
((split_second (loop'b) split_pos) ++ (split_first (loop'b) split_pos)).
Lemma up_zip'_equiv: |prefix a| >= |prefix b| -> up_zip' ==== b.
Proof.
intros L. unfold up_equal, unfold, up_zip'. destruct decision; auto.
rewrite up_prefix, up_loop, concat_prepend_string_associative, <-concat_strings_omega_unfold.
rewrite split_string_eq.
- now rewrite <-fin_iter_to_omega.
- rewrite <-fin_iter_length_bound. omega.
Qed.
Lemma up_zip'_prefix_length: |prefix a| >= |prefix b| -> |prefix a| = |prefix up_zip'|.
Proof.
intros L. unfold up_zip'. destruct decision; comega.
Qed.
Definition up_zip'' : UPSeq (X * Y) :=
mkUPSeq (string_zip (prefix a) (prefix b))
(string_zip (fin_iter (loop a) (|loop b|) ) (fin_iter (loop b) (|loop a|))).
Lemma up_zip''_proj1 : up_map fst up_zip'' ==== a.
Proof.
unfold up_equal. rewrite up_map_correct. unfold up_zip'', unfold.
now rewrite up_prefix, up_loop, string_zip_fst_up, <-fin_iter_to_omega.
Qed.
Lemma up_zip''_proj2 : |prefix a| = |prefix b| -> up_map snd up_zip'' ==== b.
Proof.
intros L. unfold up_equal. rewrite up_map_correct. unfold up_zip'', unfold.
rewrite up_prefix, up_loop, string_zip_snd_up, <-fin_iter_to_omega; auto.
rewrite !fin_iter_length. f_equal. rewrite Nat.mul_comm. f_equal.
Qed.
End UPZip''.
Section UPZip.
Context {X Y : Type}.
Variables (a : UPSeq X) (b: UPSeq Y).
Definition up_zip := if (decision (|prefix a| >= |prefix b|))
then up_zip'' a (up_zip' a b)
else up_zip''(up_zip' b a) b.
Lemma up_zip_proj1 : up_map fst up_zip ==== a.
Proof.
unfold up_zip. destruct decision as [D|D].
- now rewrite up_zip''_proj1.
- now rewrite up_zip''_proj1, up_zip'_equiv by omega.
Qed.
Lemma up_zip_proj2 : up_map snd up_zip ==== b.
Proof.
unfold up_zip. destruct decision as [D|D].
- rewrite up_zip''_proj2 by now apply up_zip'_prefix_length. now rewrite up_zip'_equiv.
- rewrite up_zip''_proj2.
+ reflexivity.
+ symmetry. apply up_zip'_prefix_length. omega.
Qed.
Lemma up_zip_correct: unfold up_zip === seq_zip (unfold a) (unfold b).
Proof.
intros n. unfold seq_zip.
enough (fst (unfold up_zip n) = unfold a n /\ snd (unfold up_zip n) = unfold b n) as [H1 H2].
- destruct (unfold up_zip n ). cbn in *. congruence.
- split.
+ pose up_zip_proj1 as Z. unfold up_equal in Z. rewrite up_map_correct in Z. unfold seq_map in Z. apply Z.
+ pose up_zip_proj2 as Z. unfold up_equal in Z. rewrite up_map_correct in Z. unfold seq_map in Z. apply Z.
Qed.
End UPZip.
Global Instance up_zip_proper (X Y : Type): Proper (@up_equal X ==> @up_equal Y ==> @up_equal (X*Y)) up_zip.
Proof.
intros a a' Ea b b' Eb. intros n.
rewrite 2up_zip_correct. unfold seq_zip. now rewrite Ea, Eb.
Qed.
End UltimatelyPeriodicSequences.
Lemma can_find_duplicate (X: finType) k (r: Seq X) : (Sigma n1 n2, n1 < n2 <= k /\ r n1 = r n2) + {k <= Cardinality X }.
Proof.
decide (k <= Cardinality X).
- now right.
- left.
assert (k > Cardinality X) as H by omega.
assert (dec (exists n2, n2 <= k /\ (exists n1, n1 < n2 /\ r n1 = r n2))) as [D|D] by auto.
+ apply cc_nat in D; auto using and_dec. destruct D as [n1 [L D]].
apply cc_nat in D; auto. destruct D as [n2 [L2 D]]. exists n2, n1 ; split; oauto.
+ enough (S k <= Cardinality X) by omega.
rewrite <-card_finType_Le_K.
apply (pidgeonHole_inj (f:= fun (k : finType_Le_K k) => r (proj1_sig k))).
intros x y E.
decide (x = y) as [D' |D']; auto.
exfalso. apply D. destruct x as [x px]; destruct y as [y py].
decide (x < y).
* exists y. split. now apply pure_le_k_iff. exists x. split; oauto.
* assert (y <> x). { intros <-. apply D'. f_equal. apply pure_eq. }
exists x. split. now apply pure_le_k_iff. exists y. split; oauto.
Qed.
Lemma can_find_duplicate' (X: finType) k_l k_u (r: Seq X): (Sigma n1 n2, k_l <= n1 < n2 /\ n2 <= k_u /\ r n1 = r n2) + {k_u - k_l <= Cardinality X }.
Proof.
destruct (can_find_duplicate (k_u - k_l) (drop k_l r)) as [[n1 [n2 [L E]]]|D].
- left. exists (k_l + n1), (k_l + n2). repeat rewrite drop_correct in E. repeat split; oauto.
- now right.
Qed.
Section StringsOfConstantLength.
Variable (m : nat).
Context {X : finType}.
Definition ConstLengthString := X^(finType_Le_K m).
Lemma dummy : (finType_Le_K m).
Proof.
exists 0. apply pure_equiv. unfold le_k. omega.
Qed.
Definition to_seq (b:ConstLengthString) := fun (n:nat) => match (decision (pure (le_k m) n) ) with
| left D => applyVect b (exist (pure (le_k m )) n D)
| right D => applyVect b dummy
end.
Definition to_bounded (w:Seq X): ConstLengthString := vectorise (fun (n:(finType_Le_K m)) => match n with exist _ n _ => w n end).
Lemma to_bounded_unchanged (w:Seq X) n (L: n <= m ): applyVect (to_bounded w) (create_Le_K L) = w n.
Proof.
unfold to_bounded. now rewrite apply_vectorise_inverse.
Qed.
Lemma to_seq_unchanged (b:ConstLengthString) n (L: n <= m ): to_seq b n = applyVect b (create_Le_K L).
Proof.
unfold to_seq.
destruct (decision (pure (le_k m) n)) as [D|D].
- f_equal. unfold create_Le_K.
f_equal. apply pure_eq.
- exfalso. apply D. now apply pure_equiv.
Qed.
Lemma to_seq_unchanged' (b:ConstLengthString) (N: finType_Le_K m): to_seq b (proj1_sig N) = applyVect b N.
Proof.
unfold to_seq. destruct decision as [D|D].
- f_equal. destruct N. f_equal. apply pure_eq.
- exfalso. apply D. now destruct N.
Qed.
Lemma bounded_unchanged (r:Seq X) n : n <=m-> to_seq (to_bounded r) n = r n.
Proof.
intros L.
rewrite (to_seq_unchanged (to_bounded r) L).
apply to_bounded_unchanged.
Qed.
Lemma bounded_unchanged_string (w: Seq X) : mkstring w m == mkstring (to_seq(to_bounded w)) m.
Proof.
split; cbn; auto. intros n L. now rewrite bounded_unchanged.
Qed.
End StringsOfConstantLength.
Arguments to_bounded {m} {X} w.
Variable (m : nat).
Context {X : finType}.
Definition ConstLengthString := X^(finType_Le_K m).
Lemma dummy : (finType_Le_K m).
Proof.
exists 0. apply pure_equiv. unfold le_k. omega.
Qed.
Definition to_seq (b:ConstLengthString) := fun (n:nat) => match (decision (pure (le_k m) n) ) with
| left D => applyVect b (exist (pure (le_k m )) n D)
| right D => applyVect b dummy
end.
Definition to_bounded (w:Seq X): ConstLengthString := vectorise (fun (n:(finType_Le_K m)) => match n with exist _ n _ => w n end).
Lemma to_bounded_unchanged (w:Seq X) n (L: n <= m ): applyVect (to_bounded w) (create_Le_K L) = w n.
Proof.
unfold to_bounded. now rewrite apply_vectorise_inverse.
Qed.
Lemma to_seq_unchanged (b:ConstLengthString) n (L: n <= m ): to_seq b n = applyVect b (create_Le_K L).
Proof.
unfold to_seq.
destruct (decision (pure (le_k m) n)) as [D|D].
- f_equal. unfold create_Le_K.
f_equal. apply pure_eq.
- exfalso. apply D. now apply pure_equiv.
Qed.
Lemma to_seq_unchanged' (b:ConstLengthString) (N: finType_Le_K m): to_seq b (proj1_sig N) = applyVect b N.
Proof.
unfold to_seq. destruct decision as [D|D].
- f_equal. destruct N. f_equal. apply pure_eq.
- exfalso. apply D. now destruct N.
Qed.
Lemma bounded_unchanged (r:Seq X) n : n <=m-> to_seq (to_bounded r) n = r n.
Proof.
intros L.
rewrite (to_seq_unchanged (to_bounded r) L).
apply to_bounded_unchanged.
Qed.
Lemma bounded_unchanged_string (w: Seq X) : mkstring w m == mkstring (to_seq(to_bounded w)) m.
Proof.
split; cbn; auto. intros n L. now rewrite bounded_unchanged.
Qed.
End StringsOfConstantLength.
Arguments to_bounded {m} {X} w.
Notation SeqLang X := (Language (Seq X)).
Notation "x ^0$0" := (universal_language (X:=Seq x)) (at level 20).
Notation StringLang X := (Language (String X)).
Notation "x ^0$0" := (universal_language (X:=Seq x)) (at level 20).
Notation StringLang X := (Language (String X)).
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 (X:Type) (l: StringLang X):= forall (v v' : String X ), l v -> v == v' -> l v'.
Definition SeqLang_Extensional (X:Type) (l: SeqLang X):= forall (w w' : Seq X ), l w -> w === w' -> l w'.
Definition SeqLang_Extensional (X:Type) (l: SeqLang X):= forall (w w' : Seq X ), l w -> w === w' -> l w'.
Definition PreImage(X Y :Type)(f: X -> Y) (L: SeqLang Y) :SeqLang X := fun w => L(seq_map f w).
Definition Image (X Y: Type) (f: X-> Y)(L : SeqLang X) : SeqLang Y := fun w => exists w', seq_map f w' === w /\ L w'.
Definition lang_o_iter (A:Type) (l : StringLang A) : SeqLang A := fun w =>
exists (f: Seq (String A)), (forall n, l ( f n)) /\ (w === concat_inf f).
Notation "l ^00" := (lang_o_iter l) (at level 20).
Section LanguageOmegaIteration.
Context{A:Type}.
Variable l: StringLang A.
(* Imagine the omega of the two 00, but I cannot use letters, otherwise coq doc pretty printing
does not like the ^ in front !*)
The second definition is weaker. If the string language is extensional, both definitions are
equivalent.
Lemma lang_o_iter_extract w : (exists f, s_monotone f /\ (f 0 = 0) /\ (forall n,l (extract (f n) (f (S n)) w) )) -> l^00 w.
Proof.
intros [f [Inc [B L]]].
pose (f' := fun n => (extract (f n) (f (S n)) w)).
exists f'. split.
- apply L.
- intros n. unfold concat_inf. destruct concat_inf_indices as [i j] eqn:H. cbn.
destruct (concat_inf_index_to_begin H) as [H1 H2].
rewrite H1. rewrite drop_correct. f_equal. f_equal. clear H1 H2 H.
induction i; cbn; auto.
rewrite IHi. specialize (Inc i). omega.
Qed.
Lemma string_omega_omega_iteration v: l v -> l^00 (v to_omega).
Proof.
intros EL. now exists (fun _ => v).
Qed.
Lemma lang_omega_iteration_extensional: StringLang_Extensional l -> SeqLang_Extensional (l^00).
Proof.
intros EL. intros w w' [f [P Q]] Ew.
exists f. split; auto. now rewrite <-Ew, Q.
Qed.
End LanguageOmegaIteration.
Instance lang_omega_iteration_proper A: Proper (@language_eq (String A) ==> @language_eq (Seq A)) (@lang_o_iter A).
Proof.
intros L1 L2 E. intros w. split; firstorder.
Qed.
Definition lang_prepend (X:Type) (lf : StringLang X) (ls: SeqLang X) : (SeqLang X) :=
fun w => exists v w', w === v +++ w' /\ lf v /\ ls w'.
Notation "l1 'o' l2" := (lang_prepend l1 l2) (at level 50).
Lemma in_lang_prepend (X:Type) (L_1: StringLang X) (L_2: SeqLang X) v w: L_1 v -> L_2 w -> (L_1 o L_2) (v +++ w).
Proof.
intros L1 L2. exists v, w. repeat split; auto.
Qed.
Global Instance lang_prepend_proper X: Proper (@language_eq (String X) ==> @language_eq (Seq X) ==> @language_eq (Seq X)) (@lang_prepend X).
Proof.
intros LS1 LS2 ES L1 L2 E. intros w. split; firstorder.
Qed.
Lemma split_position_lang_prepend X lf ls (w: Seq X):
(exists n, lf (mkstring w n) /\ ls (drop (S n) w)) -> (lf o ls) w.
Proof.
intros [n [P R]].
exists (mkstring w n), (drop (S n) w). repeat split; auto.
now rewrite revert_drop.
Qed.
Lemma prepend_on_omega_iteration (A:Type) (l_1 l_2 : StringLang A) w : (l_1 o l_2^00) w
-> exists v f_w, l_1 v /\ (forall k, l_2 (f_w k)) /\ w === (v +++ (concat_inf f_w )) .
Proof.
intros [v [w' [E [P [f [Q R]]]]]].
exists v, f. repeat split; auto. now rewrite E, R.
Qed.