Update

src/subsequences2.v

@@ -0,0 +1,950 @@
+Require Import Nat.
+Require Import PeanoNat.
+Require Import List.
+Import ListNotations.
+
+
+Fixpoint Subsequence {X: Type} (l s : list X) : Prop :=
+  match s with
+  | nil    => True
+  | hd::tl => exists l1 l2, l = l1 ++ (hd::l2) /\ Subsequence l2 tl
+  end.
+
+
+
+Theorem Subsequence_nil_r {X: Type} : forall (l : list X), Subsequence l nil.
+Proof.
+  intro l. reflexivity.
+Qed.
+
+
+Theorem Subsequence_nil_cons_r {X: Type}: forall (l: list X) (a:X),
+  ~ Subsequence nil (a::l).
+Proof.
+  intros l a. intro H. destruct H. destruct H. destruct H.
+  destruct x; apply nil_cons in H; contradiction H.
+Qed.
+
+
+Theorem Subsequence_cons_l {X: Type} : forall (l s: list X) (a: X),
+  Subsequence l s -> Subsequence (a::l) s.
+Proof.
+  intros l s a. intro H. destruct s. apply Subsequence_nil_r.
+  destruct H. destruct H. destruct H. exists (a::x0). exists x1. rewrite H.
+  split; easy.
+Qed.
+
+
+Theorem Subsequence_cons_r {X: Type} : forall (l s: list X) (a: X),
+  Subsequence l (a::s) -> Subsequence l s.
+Proof.
+  intros l s a. intro H. simpl in H. destruct H. destruct H.
+  destruct s. apply Subsequence_nil_r. destruct H. simpl in H0.
+  destruct H0. destruct H0. destruct H0.
+  exists (x ++ a::x2). exists x3.
+  rewrite H. rewrite H0. split. rewrite <- app_assoc.
+  rewrite app_comm_cons. reflexivity. assumption.
+Qed.
+
+
+Theorem Subsequence_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
+  Subsequence (a::l1) (a::l2) <-> Subsequence l1 l2.
+Proof.
+  intros l s a. split; intro H.
+  destruct H. destruct H. destruct H.
+  destruct x. inversion H. assumption.
+  destruct s. apply Subsequence_nil_r.
+  destruct H0. destruct H0. destruct H0.
+  exists (x1 ++ (a::x3)). exists x4.
+  inversion H. rewrite H0. rewrite <- app_assoc.
+  rewrite app_comm_cons. split; easy.
+  exists nil. exists l. split; easy.
+Qed.
+
+
+Lemma subsequence_alt_defs {X: Type} :
+  forall l s : list X,
+  (exists (l1: list X) (l2 : list (list X)),
+    length s = length l2
+    /\ l = l1 ++ flat_map (fun e => (fst e) :: (snd e)) (combine s l2))
+    ->
+  (exists (t: list bool),
+    length t = length l /\ s = map snd (filter fst (combine t l))).
+Proof.
+  intros l s. intro H. destruct H. destruct H. destruct H.
+
+  exists (
+    (repeat false (length x)) ++
+    (flat_map (fun e => true :: (repeat false (length e))) x0)).
+  split.
+  rewrite H0. rewrite app_length. rewrite app_length. rewrite repeat_length.
+  rewrite Nat.add_cancel_l. rewrite flat_map_length. rewrite flat_map_length.
+
+  assert (forall v (u: list X),
+    length u = length v
+    -> map (fun e => length (fst e :: snd e)) (combine u v)
+       = map (fun e => length (true :: repeat false (length e))) v).
+  intro v. induction v; intro u; intro I.
+  apply length_zero_iff_nil in I. rewrite I. reflexivity.
+  destruct u. apply O_S in I. contradiction I.
+  simpl. rewrite IHv. rewrite repeat_length. reflexivity.
+  inversion I. reflexivity.
+
+  rewrite H1; inversion H; reflexivity. rewrite H0.
+  assert (forall (u: list X) v w,
+    filter fst (combine (repeat false (length u) ++ v) (u ++ w))
+      = filter fst (combine v w)).
+  intro u. induction u; intros v w. reflexivity. simpl. apply IHu.
+
+  assert (forall (v: list (list X)) (u : list X),
+    length u = length v
+    -> u = map snd (filter fst (combine
+         (flat_map (fun e => true:: repeat false (length e)) v)
+         (flat_map (fun e => fst e :: snd e) (combine u v))))).
+  intro v. induction v; intro u; intro I.
+  apply length_zero_iff_nil in I. rewrite I. reflexivity.
+  destruct u. apply O_S in I. contradiction I.
+  simpl. rewrite H1. rewrite <- IHv; inversion I; reflexivity.
+  rewrite H1. rewrite <- H2; inversion H; reflexivity.
+Qed.
+
+
+Lemma subsequence_alt_defs2 {X: Type} :
+  forall l s : list X,
+  (exists (t: list bool),
+    length t = length l /\ s = map snd (filter fst (combine t l)))
+  -> Subsequence l s.
+Proof.
+  intros l s. intro H. destruct H. destruct H.
+
+  assert (I: forall u (v w: list X),
+    length u = length w
+    -> v = map snd (filter fst (combine u w))
+    -> Subsequence w v).
+  intro u. induction u; intros v w; intros I J.
+  rewrite J. apply Subsequence_nil_r.
+  destruct v. apply Subsequence_nil_r.
+  destruct w. apply Nat.neq_succ_0 in I. contradiction I.
+  destruct a. exists nil. exists w. inversion J.
+  apply IHu in H3. split; inversion J; try rewrite <- H5; easy.
+  inversion I. reflexivity.
+  assert (Subsequence w (x0::v)). apply IHu; inversion I; easy.
+  apply Subsequence_cons_l; assumption.
+  apply I with (u := x); assumption.
+Qed.
+
+
+Theorem subsequence_flat_map {X: Type} :
+  forall l s : list X, Subsequence l s
+  <-> exists (l1: list X) (l2 : list (list X)),
+    length s = length l2
+    /\ l = l1 ++ flat_map (fun e => (fst e) :: (snd e)) (combine s l2).
+Proof.
+  intros l s. split. generalize l. induction s; intro l0; intro H.
+  exists l0. exists nil. split. reflexivity. rewrite app_nil_r.
+  reflexivity. destruct H. destruct H. destruct H. apply IHs in H0.
+  destruct H0. destruct H0. destruct H0. exists x. exists (x1::x2).
+  split; simpl; [rewrite H0 | rewrite <- H1]; easy.
+  intro. apply subsequence_alt_defs in H. apply subsequence_alt_defs2.
+  assumption.
+Qed.
+
+
+Theorem subsequence_bools {X: Type} :
+  forall l s : list X, Subsequence l s
+  <-> (exists (t: list bool),
+    length t = length l /\ s = map snd (filter fst (combine t l))).
+Proof.
+  intros l s. split; intro. apply subsequence_alt_defs.
+  apply subsequence_flat_map. assumption.
+
+
+(** * Various definitions
+
+   Different definitions of a subsequence are given; they are proved
+   below to be equivalent, allowing to choose the most convenient at
+   any step of a proof.
+*)
+    
+Definition subsequence {X: Type} (l s : list X) :=
+  exists (l1: list X) (l2 : list (list X)),
+    length s = length l2
+    /\ l = l1 ++ flat_map (fun e => (fst e) :: (snd e)) (combine s l2).
+
+Definition subsequence2 {X: Type} (l s : list X) :=
+  exists (t: list bool),
+    length t = length l /\ s = map snd (filter fst (combine t l)).
+
+
+
+(** * Elementary properties
+*)
+
+Theorem subsequence_nil_r {X: Type}: forall (l : list X), subsequence l nil.
+Proof.
+  intro l. exists l. exists nil. rewrite app_nil_r. split; easy.
+Qed.
+
+
+Theorem subsequence2_nil_r {X: Type} : forall (l : list X), subsequence2 l nil.
+Proof.
+  intro l. 
+  exists (repeat false (length l)). rewrite repeat_length.
+  split; try induction l; easy.
+Qed.
+
+
+
+Theorem subsequence_nil_cons_r {X: Type}: forall (l: list X) (a:X),
+  ~ subsequence nil (a::l).
+Proof.
+  intros l a. intro H.
+  destruct H. destruct H. destruct H.
+  destruct x. rewrite app_nil_l in H0.
+  destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
+  apply nil_cons in H0. contradiction H0.
+  apply nil_cons in H0. contradiction H0.
+Qed.
+
+
+Theorem subsequence2_nil_cons_r {X: Type}: forall (l: list X) (a:X),
+  ~ subsequence2 nil (a::l).
+Proof.
+  intros l a. intro H. destruct H.
+  destruct H. assert (x = nil). destruct x. reflexivity.
+  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
+  rewrite H1 in H0. symmetry in H0. apply nil_cons in H0. contradiction H0.
+Qed.
+
+
+
+
+Theorem subsequence_cons_l {X: Type}: forall (l s: list X) (a: X),
+  subsequence l s -> subsequence (a::l) s.
+Proof.
+  intros l s a. intro H. destruct H. destruct H. destruct H.
+  exists (a::x). exists x0. split. assumption. rewrite H0. reflexivity.
+Qed.
+
+
+Theorem subsequence2_cons_l {X: Type} : forall (l s: list X) (a: X),
+  subsequence2 l s -> subsequence2 (a::l) s.
+Proof.
+  intros l s a. intro H. destruct H. destruct H. exists (false::x).
+  split; try apply eq_S; assumption.
+Qed.
+
+
+
+Theorem subsequence_cons_r {X: Type} : forall (l s: list X) (a: X),
+  subsequence l (a::s) -> subsequence l s.
+Proof.
+  intros l s a. intro H. destruct H. destruct H. destruct H.
+  destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
+  exists (x++a::l0). exists x0. split. inversion H. reflexivity. rewrite H0.
+  rewrite <- app_assoc. apply app_inv_head_iff. reflexivity.
+Qed.
+
+
+Theorem subsequence2_cons_r {X: Type} : forall (l s: list X) (a: X),
+  subsequence2 l (a::s) -> subsequence2 l s.
+Proof.
+  intro l. induction l. intros. apply subsequence2_nil_cons_r in H.
+  contradiction H. intros s a0 . intro H. destruct H. destruct H. destruct x.
+  symmetry in H0. apply nil_cons in H0. contradiction H0.
+  destruct b. simpl in H0. inversion H0.
+  exists (false::x). split; try rewrite <- H; reflexivity.
+  apply subsequence2_cons_l. apply IHl with (a := a0).
+  exists x. split; inversion H; easy.
+Qed.
+
+
+Theorem subsequence_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
+  subsequence (a::l1) (a::l2) <-> subsequence l1 l2.
+Proof.
+  intros l s a. split; intro H; destruct H; destruct H; destruct H.
+  destruct x. destruct x0.
+  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
+  inversion H0. exists l0. exists x0.
+  inversion H. rewrite H3. split; reflexivity.
+  destruct x0. 
+  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
+  exists (x1 ++ (a::l0)). exists x0. inversion H. rewrite H2.
+  split. reflexivity. inversion H0. rewrite <- app_assoc.
+  apply app_inv_head_iff. rewrite app_comm_cons. reflexivity.
+  exists nil. exists (x::x0). simpl.
+  split; [ rewrite H | rewrite H0 ]; reflexivity.
+Qed.
+
+
+Theorem subsequence2_cons_eq {X: Type}: forall (l1 l2: list X) (a: X),
+  subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
+Proof.
+  intros l s a. split; intro H; destruct H; destruct H.
+  destruct x. inversion H0. destruct b. exists (x).
+  split; inversion H; try rewrite H2; inversion H0; reflexivity.
+  inversion H. assert (subsequence2 l (a::s)).
+  exists x. split; assumption.
+  apply subsequence2_cons_r with (a := a). assumption.
+  exists (true :: x). split. apply eq_S. assumption. rewrite H0. reflexivity.
+Qed.
+
+
+
+(** * Equivalence of all definitions
+
+   The following three implications are proved:
+
+   - subsequence l s -> subsequence2 l s
+   - subsequence2 l s -> subsequence3 l s
+   - subsequence3 l s -> subsequence l s
+*)
+
+Theorem subsequence_eq_def_1 {X: Type} :
+  forall l s : list X, subsequence l s -> subsequence2 l s.
+Proof.
+  intros l s. intro H. destruct H. destruct H. destruct H.
+
+  exists (
+    (repeat false (length x)) ++
+    (flat_map (fun e => true :: (repeat false (length e))) x0)).
+  split.
+  rewrite H0. rewrite app_length. rewrite app_length. rewrite repeat_length.
+  rewrite Nat.add_cancel_l. rewrite flat_map_length. rewrite flat_map_length.
+
+  assert (forall v (u: list X),
+    length u = length v
+    -> map (fun e => length (fst e :: snd e)) (combine u v)
+       = map (fun e => length (true :: repeat false (length e))) v).
+  intro v. induction v; intro u; intro I.
+  apply length_zero_iff_nil in I. rewrite I. reflexivity.
+  destruct u. apply O_S in I. contradiction I.
+  simpl. rewrite IHv. rewrite repeat_length. reflexivity.
+  inversion I. reflexivity.
+
+  rewrite H1; inversion H; reflexivity. rewrite H0.
+  assert (forall (u: list X) v w,
+    filter fst (combine (repeat false (length u) ++ v) (u ++ w))
+      = filter fst (combine v w)).
+  intro u. induction u; intros v w. reflexivity. simpl. apply IHu.
+
+  assert (forall (v: list (list X)) (u : list X),
+    length u = length v
+    -> u = map snd (filter fst (combine
+         (flat_map (fun e => true:: repeat false (length e)) v)
+         (flat_map (fun e => fst e :: snd e) (combine u v))))).
+  intro v. induction v; intro u; intro I.
+  apply length_zero_iff_nil in I. rewrite I. reflexivity.
+  destruct u. apply O_S in I. contradiction I.
+  simpl. rewrite H1. rewrite <- IHv; inversion I; reflexivity.
+  rewrite H1. rewrite <- H2; inversion H; reflexivity.
+Qed.
+
+
+Theorem subsequence_eq_def_2 {X: Type} :
+  forall l s : list X, subsequence2 l s -> subsequence3 l s.
+Proof.
+  intros l s. intro H. destruct H. destruct H.
+
+  assert (I: forall u (v w: list X),
+    length u = length w
+    -> v = map snd (filter fst (combine u w))
+    -> subsequence3 w v).
+  intro u. induction u; intros v w; intros I J.
+  rewrite J. apply subsequence3_nil_r.
+  destruct v. apply subsequence3_nil_r.
+  destruct w. apply Nat.neq_succ_0 in I. contradiction I.
+  destruct a. exists nil. exists w. inversion J.
+  apply IHu in H3. split; inversion J; try rewrite <- H5; easy.
+  inversion I. reflexivity.
+  assert (subsequence3 w (x0::v)). apply IHu; inversion I; easy.
+  apply subsequence3_cons_l; assumption.
+  apply I with (u := x); assumption.
+Qed.
+
+
+
+(** * Decidability of all definitions
+*)
+
+Theorem subsequence2_dec {X: Type}:
+  (forall x y : X, {x = y} + {x <> y})
+  -> forall (l s : list X), { subsequence2 l s } + { ~ subsequence2 l s }.
+Proof.
+  intro H.
+  intro l. induction l; intro s. destruct s. left. apply subsequence2_nil_r.
+  right. apply subsequence2_nil_cons_r.
+
+  assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl. destruct H0.
+
+  rewrite <- subsequence2_cons_eq with (a := a) in s0.
+  apply subsequence2_cons_r in s0. left; assumption.
+
+  destruct s. left. apply subsequence2_nil_r.
+  assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
+  destruct IHl with (s := s); [ left | right ];
+  rewrite subsequence2_cons_eq; assumption.
+
+  right. intro I.
+  destruct I. destruct H0. destruct x0.
+  symmetry in H1. apply nil_cons in H1. contradiction H1.
+  destruct b.
+  inversion H1. rewrite H3 in n0. easy.
+  apply n. exists x0; split; inversion H0; easy.
+Qed.
+
+
+Theorem subsequence3_dec {X: Type}:
+  (forall x y : X, {x = y} + {x <> y})
+  -> forall (l s : list X), { subsequence3 l s } + { ~ subsequence3 l s }.
+Proof.
+  intro H. intros l s.
+  assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
+  apply subsequence2_dec. assumption. destruct H0.
+  apply subsequence_eq_def_2 in s0. left. assumption.
+  right. intro I.
+  apply subsequence_eq_def_3 in I.
+  apply subsequence_eq_def_1 in I.
+  apply n in I. contradiction I.
+Qed.
+
+
+Theorem subsequence_dec {X: Type}:
+  (forall x y : X, {x = y} + {x <> y})
+  -> forall (l s : list X), { subsequence l s } + { ~ subsequence l s }.
+Proof.
+  intro H. intros l s.
+  assert ({ subsequence3 l s } + { ~ subsequence3 l s }).
+  apply subsequence3_dec. assumption. destruct H0.
+  apply subsequence_eq_def_3 in s0. left. assumption.
+  right. intro I.
+  apply subsequence_eq_def_1 in I.
+  apply subsequence_eq_def_2 in I.
+  apply n in I. contradiction I.
+Qed.
+
+
+(** * Various general properties
+*)
+
+Theorem subsequence_id {X: Type} :
+  forall u : list X, subsequence u u.
+Proof.
+  intro u. apply subsequence_eq_def_3.
+  induction u. easy. exists nil. exists u.
+  split; easy.
+Qed.
+
+Theorem subsequence_app {X: Type} :
+  forall l1 s1 l2 s2 : list X,
+  subsequence l1 s1 -> subsequence l2 s2 -> subsequence (l1++l2) (s1++s2).
+Proof.
+  intros l1 s1 l2 s2. intros H I.
+  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
+  apply subsequence_eq_def_1 in H.
+  apply subsequence_eq_def_1 in 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. apply PeanoNat.Nat.neq_succ_0 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 -> subsequence l2 l3 -> subsequence l1 l3.
+Proof.
+  intros l1 l2 l3. intros H I.
+  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
+  apply subsequence_eq_def_1 in 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. apply O_S 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.
+  apply O_S 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. reflexivity.
+  destruct u0. reflexivity. destruct v0.
+  apply PeanoNat.Nat.neq_succ_0 in J; contradiction J.
+  destruct b; simpl; rewrite K; rewrite IHw;
+  inversion I; inversion J; reflexivity.
+  rewrite H4; try rewrite H1; try rewrite H; reflexivity.
+Qed.
+
+
+Lemma subsequence_length {X: Type} :
+  forall (u v: list X), subsequence u v -> length v <= length u.
+Proof.
+  intros u v. generalize u. induction v; intro u0; intro H. apply Nat.le_0_l.
+  apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
+  destruct H. destruct H. destruct H. apply subsequence_eq_def_3 in H0.
+  apply IHv in H0. simpl. apply Nat.le_succ_l. rewrite H.
+  rewrite app_length. apply Nat.lt_lt_add_l.
+  rewrite <- Nat.le_succ_l. simpl. rewrite <- Nat.succ_le_mono.
+  assumption.
+Qed.
+
+
+Theorem subsequence_eq {X: Type} :
+  forall (u v: list X),
+  subsequence u v -> subsequence v u -> u = v.
+Proof.
+  intro u. induction u; intro v; intros H I;
+  apply subsequence_eq_def_1 in H; apply subsequence_eq_def_1 in I.
+
+  destruct v. reflexivity.
+  apply subsequence2_nil_cons_r in H. contradiction H.
+  destruct v. apply subsequence2_nil_cons_r in I. contradiction I.
+
+  destruct H. destruct H. destruct I. destruct H1.
+  destruct x0. apply O_S in H. contradiction H.
+  destruct x1. apply O_S in H1. contradiction H1.
+  destruct b; destruct b0.
+
+  assert (subsequence2 u v). exists x0.
+  split; inversion H; inversion H0; reflexivity.
+  assert (subsequence2 v u). exists x1.
+  split; inversion H1; inversion H2; reflexivity.
+  apply subsequence_eq_def_2 in H3; apply subsequence_eq_def_3 in H3.
+  apply subsequence_eq_def_2 in H4; apply subsequence_eq_def_3 in H4.
+  apply IHu in H4. rewrite H4. inversion H0. reflexivity. assumption.
+
+  assert (subsequence2 u v). exists x0.
+  split; inversion H; inversion H0; reflexivity.
+  assert (subsequence2 v (a::u)). exists x1.
+  split; inversion H1; inversion H2; reflexivity.
+  assert (subsequence u (a::u)). apply subsequence_trans with (l2 := v);
+  apply subsequence_eq_def_3; apply subsequence_eq_def_2; assumption.
+  apply subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
+  contradiction H5.
+
+  assert (subsequence2 u (x::v)). exists x0.
+  split; inversion H; inversion H0; reflexivity.
+  assert (subsequence2 v u). exists x1.
+  split; inversion H1; inversion H2; reflexivity.
+  assert (subsequence v (x::v)). apply subsequence_trans with (l2 := u);
+  apply subsequence_eq_def_3; apply subsequence_eq_def_2; assumption.
+  apply subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
+  contradiction H5.
+
+  assert (subsequence2 u (x::v)). exists x0.
+  split; inversion H; inversion H0; reflexivity.
+  assert (subsequence2 v (a::u)). exists x1.
+  split; inversion H1; inversion H2; reflexivity.
+  apply subsequence2_cons_r in H3. apply subsequence2_cons_r in H4.
+  apply subsequence_eq_def_2 in H3. apply subsequence_eq_def_2 in H4.
+  apply subsequence_eq_def_3 in H3. apply subsequence_eq_def_3 in H4.
+  apply IHu in H4. rewrite H4 in H0. rewrite H4 in H.
+  simpl in H0. assert (subsequence2 v (x::v)). exists x0.
+  split. inversion H. reflexivity. assumption.
+  apply subsequence_eq_def_2 in H5. apply subsequence_eq_def_3 in H5.
+  apply subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
+  contradiction H5. assumption.
+Qed.
+
+
+Theorem subsequence_length_eq {X: Type} :
+  forall (u v: list X),
+  subsequence u v -> length u = length v -> u = v.
+Proof.
+  intros u v. intros H I. apply subsequence_eq_def_1 in H.
+  destruct H. destruct H. rewrite H0 in I.
+  rewrite map_length in I.
+  replace (length u) with (length (combine x u)) in I.
+  symmetry in I. apply filter_length_forallb in I.
+  apply forallb_filter_id in I. rewrite I in H0.
+
+  assert (J: forall (a: list bool) (b: list X),
+    length a = length b -> b = map snd (combine a b)).
+  intro a. induction a; intro b; intro J.
+  symmetry in J. apply length_zero_iff_nil in J. rewrite J. reflexivity.
+  destruct b. inversion J. simpl. rewrite <- IHa. reflexivity.
+  inversion J. reflexivity. rewrite H0. apply J. assumption.
+
+  rewrite combine_length. rewrite H. apply PeanoNat.Nat.min_id.
+Qed.
+
+
+ Theorem subsequence_in {X: Type} :
+   forall (u: list X) a, In a u <-> subsequence u [a].
+ Proof.
+   intros u a. split.
+   induction u; intro H. apply in_nil in H. contradiction.
+   destruct H. rewrite H. exists nil. exists [u]. split. reflexivity.
+   simpl. rewrite app_nil_r. reflexivity. apply subsequence_cons_l.
+   apply IHu. assumption.
+   intro H. destruct H. destruct H. destruct H. rewrite H0. apply in_or_app.
+   right. destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
+   left. reflexivity.
+Qed.
+
+
+Theorem subsequence_rev {X: Type} :
+  forall (u v: list X), subsequence u v <-> subsequence (rev u) (rev v).
+Proof.
+  assert (MAIN: forall (u v: list X),
+      subsequence u v -> subsequence (rev u) (rev v)).
+  intros u v. intro H.
+  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
+  apply subsequence_eq_def_1 in H. destruct H. destruct H.
+  exists (rev x). split. rewrite rev_length. rewrite rev_length.
+  assumption. rewrite H0.
+
+  assert (LEMMA : forall (l1: list bool) (l2: list X),
+    length l1 = length l2
+    -> combine (rev l1) (rev l2) = rev (combine l1 l2)).
+  intro l1. induction l1; intro l2; intro I. reflexivity.
+  destruct l2. inversion I. inversion I. apply IHl1 in H2.
+  simpl.
+  assert (LEMMA2 : forall (u w : list bool) (v x : list X),
+    length u = length v
+    -> combine (u ++ w) (v ++ x) = (combine u v) ++ (combine w x)).
+  intro u0. induction u0; intros w v0 x1; intro J.
+  symmetry in J. apply length_zero_iff_nil in J. rewrite J.
+  reflexivity. destruct v0. inversion J. inversion J.
+  apply IHu0 with (w := w) (x := x1) in H3. simpl. rewrite H3.
+  reflexivity. rewrite LEMMA2. rewrite IHl1. reflexivity.
+  inversion I. reflexivity. rewrite rev_length. rewrite rev_length.
+  inversion I. reflexivity. rewrite LEMMA. rewrite <- map_rev.
+  assert (LEMMA3: forall v (w: list (bool * X)),
+    rev (filter v w) = filter v (rev w)).
+  intros v0 w. induction w. reflexivity. simpl. rewrite filter_app.
+  simpl. destruct (v0 a). simpl. rewrite IHw. reflexivity.
+  rewrite IHw. symmetry. apply app_nil_r. rewrite LEMMA3.
+  reflexivity. assumption.
+  split. apply MAIN. intro H. apply MAIN in H.
+  rewrite rev_involutive in H. rewrite rev_involutive in H.
+  assumption.
+Qed.
+
+
+Theorem subsequence_map {X Y: Type} :
+  forall (u v: list X) (f: X -> Y),
+    subsequence u v -> subsequence (map f u) (map f v).
+Proof.
+  intros u v. generalize u. induction v; intros u0 f; intro H.
+  apply subsequence_nil_r. apply subsequence_eq_def_3.
+  apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
+  destruct H. destruct H. destruct H.
+  exists (map f x). exists (map f x0). split.
+  rewrite <- map_cons. rewrite <- map_app. rewrite H. reflexivity.
+  apply subsequence_eq_def_2. apply subsequence_eq_def_1.
+  apply IHv. apply subsequence_eq_def_3. assumption.
+Qed.
+
+
+Theorem subsequence_double_cons {X: Type} :
+  forall (u v: list X) a, subsequence (a::u) (a::v) <-> subsequence u v.
+Proof.
+  intros u v a. split; intro H. destruct H. destruct H. destruct H.
+  destruct x; destruct x0. symmetry in H0. apply nil_cons in H0.
+  contradiction. inversion H0.
+  exists l. exists x0. split. inversion H. reflexivity. reflexivity.
+  apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
+  inversion H0. exists (x1++x::l). exists x0. split. inversion H.
+  reflexivity. rewrite <- app_assoc. reflexivity.
+  apply subsequence_eq_def_3. exists nil. exists u.
+  split. reflexivity. apply subsequence_eq_def_2. apply subsequence_eq_def_1.
+  assumption.
+Qed.
+
+
+Theorem subsequence_filter {X: Type} :
+  forall (u v: list X) f, subsequence (filter f u) v -> subsequence u v.
+Proof.
+  intro u. induction u; intros v f; intro H. assumption.
+  simpl in H. destruct (f a). assert (K := H).
+  apply subsequence_eq_def_1 in H. destruct H. destruct H.
+  destruct x. apply O_S in H. contradiction. destruct b.
+  destruct v. apply subsequence_nil_r. assert (x0 = a). inversion H0.
+  reflexivity. rewrite H1.
+  apply subsequence_eq_def_3. exists nil. exists u. split. reflexivity.
+  apply subsequence_eq_def_2. apply subsequence_eq_def_1.
+  apply IHu with (f := f). rewrite H1 in K.
+  apply subsequence_double_cons in K. assumption.
+  apply subsequence_cons_l. apply IHu with (f := f).
+  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
+  exists x. split. inversion H. reflexivity. apply H0.
+  apply subsequence_cons_l. apply IHu with (f := f). assumption.
+Qed.
+
+
+Theorem subsequence_incl {X: Type} :
+  forall (u v: list X), subsequence u v -> incl v u.
+Proof.
+  intros u v. intro H. intro a. intro I.
+  generalize I. generalize H. generalize u.
+  induction v; intros u0; intros J K. inversion K.
+  destruct K. rewrite H0 in J.
+  apply subsequence_eq_def_1 in J.
+  apply subsequence_eq_def_2 in J.
+  destruct J. destruct H1. destruct H1. rewrite H1.
+
+  assert (J: forall (u v : list X) w, In w (u++w::v)).
+  intro  u1. induction u1; intros v0 w. left. reflexivity.
+  right. apply IHu1. apply J. apply IHv.
+
+  apply subsequence_cons_r in H. assumption. assumption.
+  apply subsequence_cons_r in J. assumption. assumption.
+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 | exists x1]; split; try assumption; reflexivity.
+
+  assumption.
+Qed.
+
+
+Theorem subsequence_split_2 {X: Type} :
+  forall (u v w: list X),
+    subsequence u (v++w) 
+    -> (exists a b, u = a++b /\ (subsequence a v) /\ subsequence b w).
+Proof.
+  intros u v w. intro H. destruct H. destruct H. destruct H.
+  exists (x ++
+     flat_map (fun e : X * list X => fst e :: snd e) (combine v x0)).
+  exists (
+     flat_map (fun e : X * list X => fst e :: snd e)
+     (combine w (skipn (length v) x0))).
+   split. rewrite H0. rewrite <- app_assoc. apply app_inv_head_iff.
+   rewrite <- flat_map_app.
+
+   assert (L: forall (w y: list X) (z : list (list X)),
+     length z = length w + length y ->
+     combine (w ++ y) z = combine w z ++ combine y (skipn (length w) z)).
+   intros w0. induction w0; intros y z; intro I. reflexivity.
+   destruct z. simpl. rewrite combine_nil. reflexivity.
+   simpl. rewrite IHw0. reflexivity. inversion I. reflexivity.
+   rewrite L. reflexivity. rewrite app_length in H. rewrite H.
+   reflexivity. split.
+   exists x. exists (firstn (length v) x0). split.
+   rewrite firstn_length. rewrite <- H. rewrite app_length.
+   rewrite min_l. reflexivity. apply PeanoNat.Nat.le_add_r.
+   rewrite combine_firstn_l. reflexivity.
+
+   exists nil. exists (skipn (length v) x0). split.
+   rewrite app_length in H. rewrite skipn_length. rewrite <- H.
+   rewrite PeanoNat.Nat.add_sub_swap. rewrite PeanoNat.Nat.sub_diag.
+   reflexivity. reflexivity. reflexivity.
+ Qed.
+
+
+Theorem subsequence_filter_2 {X: Type} :
+  forall (u v: list X) f,
+    subsequence u v -> subsequence (filter f u) (filter f v).
+Proof.
+  intros u v. generalize u. induction v; intros u0 f; intro H.
+  apply subsequence_nil_r.
+
+  assert (f a = true \/ f a = false).
+  destruct (f a); [ left | right ]; reflexivity. destruct H0.
+  simpl. rewrite H0.
+  replace (a::v) with ([a] ++ v) in H. apply subsequence_split_2 in H.
+  destruct H. destruct H. destruct H. destruct H1.
+
+  assert (subsequence ((filter f x) ++ (filter f x0))
+                      ((filter f [a]) ++ (filter f v))).
+  apply subsequence_app. simpl. rewrite H0.
+  apply subsequence_incl in H1. apply incl_cons_inv in H1. destruct H1.
+  assert (In a (filter f x)). apply filter_In. split; assumption.
+  apply subsequence_in. assumption. apply IHv. assumption.
+  rewrite <- filter_app in H3. rewrite <- H in H3. simpl in H3.
+  rewrite H0 in H3. assumption. reflexivity.
+  simpl. rewrite H0. apply IHv. apply subsequence_cons_r in H.
+  assumption.
+Qed.
+
+
+Theorem subsequence_add {X: Type} :
+  forall (u v w: list X) x, subsequence u v -> Add x u w -> subsequence w v.
+Proof.
+  intros u v w. generalize u v.
+  induction w; intros u0 v0 x; intros H I; inversion I.
+  rewrite <- H2. apply subsequence_cons_l. rewrite <- H3. assumption.
+
+  assert (J := H). apply subsequence_eq_def_1 in H. rewrite <- H1 in H.
+  rewrite H0 in H. destruct H. destruct H.
+  destruct x1. apply O_S in H. contradiction. destruct b.
+  rewrite H4. simpl. apply subsequence_double_cons.
+  apply IHw with (u := l) (x := x).
+  apply subsequence_eq_def_3. apply subsequence_eq_def_2. exists x1.
+  inversion H. split; reflexivity. assumption.
+  apply subsequence_cons_r with (a:=a).
+  rewrite H4. simpl. apply subsequence_double_cons.
+  apply IHw with (u := l) (x := x).
+  apply subsequence_eq_def_3. apply subsequence_eq_def_2. exists x1.
+  inversion H. split; reflexivity. assumption.
+Qed.
+
+
+Theorem subsequence_nodup {X: Type} :
+  forall (u v: list X), subsequence u v -> NoDup u -> NoDup v.
+Proof.
+  intros u v. intros H I. apply subsequence_eq_def_1 in H.
+  destruct H. destruct H. rewrite H0.
+
+  assert (J: forall z (q: list X),
+    NoDup q -> NoDup (map snd (filter fst (combine z q)))).
+  intro z. induction z; intro q; intro J. apply NoDup_nil.
+  destruct q. rewrite combine_nil. apply NoDup_nil.
+  destruct a. simpl. rewrite NoDup_cons_iff in J. destruct J.
+  apply IHz in H2. apply NoDup_cons.
+
+  assert (K: forall (q: list X) g h,
+    ~ In g q -> ~ In g (map snd (filter fst (combine h q)))).
+  intro q0. induction q0; intros g h; intro J.
+  rewrite combine_nil. easy. destruct h. easy. destruct b.
+  replace (map snd (filter fst (combine (true :: h) (a :: q0))))
+    with (a::(map snd (filter fst (combine h q0)))).
+  rewrite not_in_cons. split;
+  rewrite not_in_cons in J; destruct J. assumption. apply IHq0.
+  assumption. reflexivity. apply IHq0.
+  rewrite not_in_cons in J; destruct J. assumption. apply K. assumption.
+  assumption. simpl. apply IHz.
+  rewrite NoDup_cons_iff in J. destruct J. assumption. apply J.
+  assumption.
+Qed.
+
+
+Theorem subsequence_in_2 {X: Type} :
+  forall (u v: list X) a, subsequence u v -> In a v -> In a u.
+Proof.
+  intros u v. generalize u. induction v; intros u0 a0; intros H I.
+  contradiction I. destruct I.
+  apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
+  destruct H. destruct H. destruct H. rewrite H. rewrite H0.
+  apply in_elt. apply IHv. apply subsequence_cons_r in H.
+  assumption. assumption.
+Qed.
+
+
+Theorem subsequence_not_in {X: Type} :
+  forall (u v: list X) a, subsequence u v -> ~ In a u -> ~ In a v.
+Proof.
+  intros u v. generalize u. induction v; intros u0 a0; intros H I.
+  easy. apply not_in_cons. split. apply subsequence_incl in H.
+  apply incl_cons_inv in H. destruct H.
+
+  assert (forall z (x y: X), In x z -> ~ In y z -> x <> y).
+  intro z. induction z; intros x y; intros J K. inversion J.
+  apply in_inv in J. destruct J. rewrite <- H1.
+  apply not_in_cons in K. destruct K. apply not_eq_sym. assumption.
+  apply IHz. assumption.
+  apply not_in_cons in K. destruct K. assumption. apply not_eq_sym.
+  generalize I. generalize H. apply H1. generalize I. apply IHv.
+  apply subsequence_cons_r in H. assumption.
+Qed.
+
+
+Theorem subsequence_as_filter {X: Type} :
+  forall (u: list X) f, subsequence u (filter f u).
+Proof.
+  intros u f. apply subsequence_eq_def_3. apply subsequence_eq_def_2.
+  exists (map f u). split. apply map_length.
+  induction u. reflexivity. simpl. destruct (f a).
+  simpl. rewrite IHu. reflexivity. assumption.
+Qed.
+
+
+Theorem subsequence_as_partition {X: Type} :
+  forall (u v w: list X) f,
+    (v, w) = partition f u -> (subsequence u v) /\ (subsequence u w).
+Proof.
+  intros u v w f. intro H. rewrite partition_as_filter in H. split.
+  replace v with (fst (v, w)). rewrite H. simpl.
+  apply subsequence_as_filter. reflexivity.
+  replace w with (snd (v, w)). rewrite H. simpl.
+  apply subsequence_as_filter. reflexivity.
+Qed.