Update

src/subsequences.v

@@ -358,7 +358,103 @@ Proof.
 Qed.
 
 
+Theorem subsequence2_app {X: Type} :
+  forall l1 s1 l2 s2 : list X,
+  subsequence2 l1 s1 -> subsequence2 l2 s2 -> subsequence2 (l1++l2) (s1++s2).
+Proof.
+  intros l1 s1 l2 s2. intros H I.
+  destruct H. destruct I. exists (x++x0). destruct H. destruct H0.
+  split. rewrite app_length. rewrite app_length.
+  rewrite H. rewrite H0. reflexivity.
+  rewrite H1. rewrite H2.
 
+  assert (J: forall (t : list bool) (u : list X) (v: list bool) (w : list X),
+    length t = length u
+    -> combine (t++v) (u++w) = (combine t u) ++ (combine v w)).
+  intros t u v w. generalize u. induction t; intro u0; intro K.
+  replace u0 with (nil : list X). reflexivity.
+  destruct u0. reflexivity. apply O_S in K. contradiction K.
+  destruct u0. symmetry in K. apply O_S in K. contradiction K.
+  simpl. rewrite IHt. reflexivity. inversion K. reflexivity.
+
+  rewrite J. rewrite filter_app. rewrite map_app. reflexivity.
+  assumption.
+Qed.
+
+
+Theorem subsequence_trans {X: Type} :
+  forall (l1 l2 l3: list X),
+  subsequence l1 l2 -> subsequence2 l2 l3 -> subsequence2 l1 l3.
+Proof.
+  intros l1 l2 l3. intros H I.
+  destruct H. destruct H. destruct H. destruct I. destruct H1.
+  exists (
+    (repeat false (length x)) ++
+    (flat_map (fun e => (fst e) :: (repeat false (length (snd e))))
+              (combine x1 x0))).
+  split.
+
+  rewrite app_length. rewrite repeat_length.
+  rewrite H0. rewrite app_length. rewrite Nat.add_cancel_l.
+  rewrite flat_map_length. rewrite flat_map_length.
+  assert (forall (u: list X) (v: list (list X)),
+    length u = length v
+    -> list_sum (map (fun z => length (fst z :: snd z))
+                     (combine u v))
+       = list_sum (map (fun z => S (length z)) v)).
+  intros u v. generalize u. induction v; intro u0; intro I.
+  apply length_zero_iff_nil in I. rewrite I. reflexivity.
+  destruct u0.
+  symmetry in I. apply PeanoNat.Nat.neq_succ_0 in I. contradiction I.
+  simpl. rewrite IHv. reflexivity. inversion I. reflexivity.
+  rewrite H3.
+  assert (forall (u: list bool) (v: list (list X)),
+    length u = length v
+    -> list_sum (map (fun z => length (fst z :: repeat false (length (snd z))))
+                     (combine u v))
+       = list_sum (map (fun z => S (length z)) v)).
+  intros u v. generalize u.
+  induction v; intro u0; intro I; destruct u0. reflexivity.
+  apply PeanoNat.Nat.neq_succ_0 in I. contradiction I.
+  symmetry in I. apply PeanoNat.Nat.neq_succ_0 in I. contradiction I.
+  simpl. rewrite IHv. rewrite repeat_length. reflexivity.
+  inversion I. reflexivity. rewrite H4. reflexivity.
+  rewrite H1. rewrite H. reflexivity. assumption.
+
+  assert (K: forall (w v: list X) u,
+    filter fst (combine ((repeat false (length w)) ++ u)
+                        (w ++ v)) = filter fst (combine u v)).
+  intro w0. induction w0. reflexivity. apply IHw0.
+  rewrite H2. rewrite H0.
+  assert (forall (u v: list X) (w: list bool),
+    map snd (filter fst (combine ((repeat false (length u)) ++ w) (u ++ v)))
+      = map snd (filter fst (combine w v))).
+  intro u. induction u; intros v w. reflexivity.
+  apply IHu. rewrite H3.
+  assert (forall (u: list bool) (v: list X) (w: list (list X)),
+    length u = length w
+    -> length u = length v
+    -> filter fst (combine
+                      (flat_map
+                         (fun e => fst e:: (repeat false (length (snd e))))
+                         (combine u w))
+                      (flat_map (fun e => fst e :: snd e) (combine v w)))
+         = filter fst (combine u v)).
+  intros u v w. generalize u. generalize v.
+  induction w; intros v0 u0; intros I J.
+  apply length_zero_iff_nil in I. rewrite I in J. rewrite I.
+  symmetry in J. apply length_zero_iff_nil in J. rewrite J.
+  reflexivity.
+  destruct u0. reflexivity. destruct v0.
+  apply PeanoNat.Nat.neq_succ_0 in J. contradiction J.
+  destruct b; simpl; rewrite K; rewrite IHw.
+  reflexivity. inversion I. reflexivity. inversion J. reflexivity.
+  reflexivity. inversion I. reflexivity. inversion J. reflexivity.
+  rewrite H4. reflexivity.
+  rewrite H1. rewrite H. reflexivity.
+  rewrite H1. reflexivity.
+Qed.
+ 
 
 
 Example test1: subsequence [1;2;3;4;5] [1;3;5].