Require Import Nat.
Require Import PeanoNat.
Require Import List.
Import ListNotations.


(** * Various definitions of a subsequences

   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)).

Fixpoint subsequence3 {X: Type} (l s : list X) : Prop :=
  match s with
  | nil    => True
  | hd::tl => exists l1 l2, l = l1 ++ (hd::l2) /\ subsequence3 l2 tl
  end.


(**
   Identical elementary properties of all definitions of a subsequence.
*)

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 subsequence3_nil_r {X: Type} : forall (l : list X), subsequence3 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. 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 subsequence3_nil_cons_r {X: Type}: forall (l: list X) (a:X),
  ~ subsequence3 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 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 subsequence3_cons_l {X: Type} : forall (l s: list X) (a: X),
  subsequence3 l s -> subsequence3 (a::l) s.
Proof.
  intros l s a. intro H. destruct s. apply subsequence3_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. 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 subsequence3_cons_r {X: Type} : forall (l s: list X) (a: X),
  subsequence3 l (a::s) -> subsequence3 l s.
Proof.
  intros l s a. intro H. simpl in H. destruct H. destruct H.
  destruct s. apply subsequence3_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. 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.


Theorem subsequence3_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
  subsequence3 (a::l1) (a::l2) <-> subsequence3 l1 l2.
Proof.
  intros l s a. split; intro H.
  destruct H. destruct H. destruct H.
  destruct x. inversion H. assumption.
  destruct s. apply subsequence3_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.


(**
   Decidability and equivalence of all definitions of a subsequence.
*)

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. contradiction n0. reflexivity.

  assert (subsequence2 l (x::s)). exists x0. split; inversion H0; easy.
  apply n in H2. contradiction H2.
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. intro l. induction l. intro s. destruct s. left. reflexivity.
  right. apply subsequence3_nil_cons_r.

  intro s. assert({subsequence3 l s} + {~ subsequence3 l s}). apply IHl.
  destruct H0.

  rewrite <- subsequence3_cons_eq with (a := a) in s0.
  apply subsequence3_cons_r in s0. left. assumption.

  destruct s. left. apply subsequence3_nil_r.
  assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
  destruct IHl with (s := s); [ left | right ];
  rewrite subsequence3_cons_eq; assumption.

  right. intro I.
  destruct I. destruct H0. destruct H0. destruct x0.
  inversion H0. rewrite H3 in n0. contradiction n0. reflexivity.

  assert (subsequence3 l (x::s)). exists x2. exists x1.
  inversion H0. split. reflexivity. assumption.
  apply n in H2. contradiction H2.
Qed.


Theorem subsequence_eq_def_2 {X: Type} :
  (forall (x y : X), {x = y} + {x <> y})
  -> (forall l s : list X, subsequence l s <-> subsequence2 l s).
Proof.
  intro I. intro l. induction l.
  intro s. split; intro H. destruct s. apply subsequence2_nil_r.
  apply subsequence_nil_cons_r in H. contradiction H.
  destruct s. apply subsequence_nil_r.
  apply subsequence2_nil_cons_r in H. contradiction H.

  intro s. destruct s. split; intro H. apply subsequence2_nil_r.
  apply subsequence_nil_r.

  assert ({a=x} + {a<>x}). apply I. destruct H.
  rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl.
  rewrite subsequence_cons_eq. split; intro; assumption.

  split; intro H. apply subsequence2_cons_l. apply IHl.
  destruct H. destruct H. destruct H.
  destruct x0. destruct x1.
  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
  simpl in H0. inversion H0. rewrite H2 in n. contradiction n.
  reflexivity. inversion H0.
  exists x2. exists x1. split. assumption.
  reflexivity.

  apply subsequence_cons_l. apply IHl.
  destruct H. destruct H.
  destruct x0. simpl in H0.
  symmetry in H0. apply nil_cons in H0. contradiction H0.
  destruct b. simpl in H0. inversion H0. rewrite H2 in n.
  contradiction n. reflexivity.
  exists x0. inversion H. inversion H0.
  split; reflexivity.
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 ({ subsequence2 l s } + { ~ subsequence2 l s }).
  apply subsequence2_dec. assumption. destruct H0.
  rewrite <- subsequence_eq_def_2 in s0. left. assumption.
  assumption. rewrite <- subsequence_eq_def_2 in n. right. assumption.
  assumption.
Qed.


Theorem subsequence_eq_def_3 {X: Type} :
  (forall (x y : X), {x = y} + {x <> y})
  -> (forall l s : list X, subsequence l s <-> subsequence3 l s).
Proof.
  intro I. intro l. induction l.
  intro s. split; intro H. destruct s. apply subsequence3_nil_r.
  apply subsequence_nil_cons_r in H. contradiction H.
  destruct s. apply subsequence_nil_r.
  apply subsequence3_nil_cons_r in H. contradiction H.

  intro s. destruct s. split; intro H. apply subsequence3_nil_r.
  apply subsequence_nil_r.

  assert ({a=x} + {a<>x}). apply I. destruct H.
  rewrite e. rewrite subsequence3_cons_eq. rewrite <- IHl.
  rewrite subsequence_cons_eq. split; intro; assumption.

  split; intro H. apply subsequence3_cons_l. apply IHl.
  destruct H. destruct H. destruct H.
  destruct x0. destruct x1.
  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
  simpl in H0. inversion H0. rewrite H2 in n. contradiction n.
  reflexivity. inversion H0.
  exists x2. exists x1. split. assumption.
  reflexivity.

  apply subsequence_cons_l. apply IHl.
  destruct H. destruct H. destruct H.

  destruct x0. inversion H. rewrite H2 in n. contradiction n. reflexivity.
  exists x2. exists x1. split. inversion H. reflexivity. assumption.
Qed.


(**
   Various general properties of a subsequence.
*)

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. 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 -> 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. 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.
  reflexivity. inversion I; reflexivity. inversion J; reflexivity.
  reflexivity. inversion I; reflexivity. inversion J; reflexivity.
  rewrite H4; try rewrite H1; try rewrite H; reflexivity.
Qed.
 


Example test1: subsequence [1;2;3;4;5] [1;3;5].
Proof.
  unfold subsequence.
  exists [].
  exists [[2];[4];[]]. simpl. easy.
Qed.

Example test2: subsequence [1;2;3;4;5] [2;4].
Proof.
  unfold subsequence.
  exists [1].
  exists [[3];[5]]. simpl. easy.
Qed.

Example test3: subsequence [1;2;3;4;5] [1;3;5].
Proof.
  rewrite subsequence_eq_def_2.
  exists [true; false; true; false; true].
  split; reflexivity.
  apply Nat.eq_dec.
Qed.





Theorem subsequence0_eq_def_2 {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. reflexivity. 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. reflexivity. inversion I.
  reflexivity. rewrite H1. rewrite <- H2. reflexivity.
  inversion H. reflexivity.
Qed.


Theorem subsequence0_eq_def_3 {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. reflexivity. inversion J. rewrite <- H5. assumption.
  inversion I. reflexivity. simpl in J.

  assert (subsequence3 w (x0::v)). apply IHu.
  inversion I. reflexivity. assumption.
  apply subsequence3_cons_l. assumption.

  apply I with (u := x); assumption.
Qed.


Theorem subsequence0_eq_def_1 {X: Type} :
  forall l s : list X, subsequence3 l s -> subsequence l s.
Proof.
  intros l s. generalize l. induction s; intro l0; intro H.
  apply subsequence_nil_r. 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.
  reflexivity. rewrite H. rewrite H1. reflexivity.
Qed.





(*
  destruct H. destruct H.

  (* z contient la position des booléens dans x *)
  pose (z := map snd (filter fst (combine x (seq 0 (length x))))).
  destruct s. exists l. exists nil. rewrite app_nil_r. split; easy.

  assert (0 < length z). unfold z. rewrite map_length.
  assert (forall v (u: list X) (w: list nat),
  length u = length v -> length u = length w
    -> length (filter fst (combine v w))
        = length (map snd (filter fst (combine v u)))).
  intro v. induction v; intros u w; intros I J. reflexivity.
  destruct w. apply length_zero_iff_nil in J. rewrite J in I.
  apply O_S in I. contradiction I.
  destruct u. apply O_S in J. contradiction J.
  destruct a; simpl. apply eq_S. apply IHv.
  inversion I. reflexivity. inversion J. reflexivity.
  apply IHv.
  inversion I. reflexivity. inversion J. reflexivity.
  assert (length (x0::s) = length (map snd (filter fst (combine x l)))).
  rewrite H0. reflexivity. rewrite <- H1 with (w := seq 0 (length x)) in H2.
  rewrite <- H2. apply Nat.lt_0_succ. inversion H. reflexivity.
  rewrite H. rewrite seq_length. reflexivity.
  exists (firstn (hd 0 z) l).

  (* z2 contient la position du true suivant *)
  pose (z2 := (skipn 1 z) ++ [ length l ]).

  (* z3 contient la longueur de chaque bloc  true; false; false; ... *)
  pose (z3 := map (fun e => (snd e) - (fst e)) (combine z z2)).

  exists (map (fun e => firstn ((snd e) -1) (skipn (S (fst e)) l))
            (combine z z3)).

  assert (length (x0::s) = length z). unfold z. rewrite H0.
  rewrite map_length. rewrite map_length. rewrite H.
  assert (forall u (v: list X) (w: list nat),
    length v = length w
    -> length (filter fst (combine u v))
       = length (filter fst (combine u w))).
  intro u. induction u; intros v w; intro I. reflexivity.
  destruct v. symmetry in I. apply length_zero_iff_nil in I.
  rewrite I. reflexivity. destruct w. apply Nat.neq_succ_0 in I.
  contradiction I. destruct a; simpl; rewrite IHu with (w := w).
  inversion I; reflexivity. inversion I; reflexivity. reflexivity.
  inversion I; reflexivity. rewrite H2 with (w := seq 0 (length l)).
  reflexivity. rewrite seq_length. reflexivity.

  unfold z3. unfold z2. split. destruct z. apply Nat.nlt_0_r in H1.
  contradiction H1.
  rewrite map_length. rewrite combine_length. rewrite map_length.
  rewrite combine_length. rewrite app_length. rewrite Nat.add_1_r.
  simpl. apply eq_S. rewrite Nat.min_id. rewrite Nat.min_id.
  inversion H2. reflexivity. unfold z. rewrite H0.

  assert (forall (u: list bool) (v: list X),
    length u = length v
    -> v =
    firstn (hd 0 (map snd (filter fst (combine u (seq 0 (length u)))))) v ++
    flat_map (fun e : X * list X => fst e :: snd e)
      (combine (map snd (filter fst (combine u v)))
         (map (fun e : nat * nat => firstn (snd e - 1) (skipn (S (fst e)) v))
            (combine (map snd (filter fst (combine u (seq 0 (length u)))))
               (map (fun e : nat * nat => snd e - fst e)
                  (combine (map snd (filter fst (combine u (seq 0 (length u)))))
                     (skipn 1
                        (map snd (filter fst (combine u (seq 0 (length u))))) ++
                      [length v]))))))).
  intro u. induction u; intro v; intro I.
  symmetry in I. apply length_zero_iff_nil in I. assumption.
  destruct v. rewrite app_nil_r. rewrite firstn_nil. reflexivity.
  destruct a. 

  replace
     (map snd (filter fst (combine (true :: u) (seq 0 (length (true :: u))))))
  with 
 *)