Update

src/subsequences.v

@@ -604,6 +604,52 @@ Proof.
 Qed.
 
 
+Theorem subsequence_split {X: Type} :
+  forall (u v w: list X),
+    subsequence (u++v) w 
+    -> (exists a b, w = a++b /\ (subsequence u a) /\ subsequence v b).
+Proof.
+  intros u v w. intro H.
+  apply subsequence_eq_def_1 in H.
+  destruct H. destruct H.
+
+  assert (forall (b: list bool) (u v: list X),
+    length b = length (u++v)
+    -> exists x y, b = x++y /\ length x = length u /\ length y = length v).
+  intros b u0 v0. intro I.
+  rewrite app_length in I.
+  exists (firstn (length u0) b). exists (skipn (length u0) b).
+  split. symmetry. apply firstn_skipn. split.
+  rewrite firstn_length_le. reflexivity. rewrite I.
+  apply PeanoNat.Nat.le_add_r. rewrite skipn_length.
+  rewrite I. rewrite Nat.add_sub_swap. rewrite PeanoNat.Nat.sub_diag.
+  reflexivity. apply le_n.
+  apply H1 in H. destruct H. destruct H. destruct H. destruct H2.
+
+  exists (map snd (filter fst (combine x0 u))).
+  exists (map snd (filter fst (combine x1 v))).
+  rewrite <- map_app. rewrite <- filter_app.
+
+  assert (L: forall (g i: list bool) (h j: list X), length g = length h
+    -> (combine g h) ++ (combine i j) = combine (g++i) (h++j)).
+  intro g. induction g; intros i h j; intro I.
+  symmetry in I. apply length_zero_iff_nil in I. rewrite I.
+  reflexivity.
+  destruct h. apply PeanoNat.Nat.neq_succ_0 in I. contradiction.
+  simpl. rewrite IHg. reflexivity. inversion I. reflexivity.
+  rewrite L. rewrite <- H. split. assumption. split.
+
+  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
+  exists x0. split. assumption. reflexivity.
+  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
+  exists x1. split. assumption. reflexivity.
+
+  assumption.
+Qed.
+
+
+
+
 (** * Tests
 *)