Definition function without using a helper function

Question

I have been reading through Software Foundations and solving the problems in it. This is one of the definition I'm trying to define:

Fixpoint split {X Y : Type} (l : list (X*Y)) : (list X) * (list Y)

Basically it's a unzip version of haskell.

I implemented it like this:

Fixpoint split2 {X Y : Type} (l : list (X*Y)) (g :(list X) * (list Y))
               : (list X) * (list Y) :=
  match l with
    | [] => g
    | (x,y)::xs => split2 xs ((fst g) ++ [x],(snd g) ++ [y])
  end.

Fixpoint split {X Y : Type} (l : list (X*Y))
               : (list X) * (list Y) :=
split2 l ([],[]).

I have two questions:

• Is it possible to define split without using a helper function like split2 this ?
• Is there a equivalent of where clause (like in Haskell) in Coq ?

Answer 1

There is let in Coq. You can and should just translate the standard Haskell definition, avoiding the quadratic performance with ++:

Fixpoint split {A B} (l : list (A * B)) : list A * list B :=
  match l with
    [] => ([], [])
  | (x, y) :: xs => let (xs2, ys2) := split xs in (x::xs2, y::ys2)
  end.