MoreCoq.v

Fixpoint split
           {X Y : Type} (l : list (X*Y))
           : (list X) * (list Y) :=
  match l with
    | nil => (nil, nil)
    | (x,y) :: t =>
      let (r,s) := split t in
      (x :: r, y :: s)
  end.

Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
  split l = (l1, l2) ->
  combine l1 l2 = l.
Proof.
  intros until l1; revert l;
  induction l1 as [|x xs]; destruct l2 as [|y ys]; destruct l as [|p ps]; intro S;
  try (destruct p; simpl in *; case_eq (split ps); intros xs' ys' H; rewrite H in S);
  inversion S;
  try rewrite IHxs with (l := ps); subst; auto.
Qed.