CODEWITHSUNDEEP
coq
Sibi
Sibi

Reputation: 48644

Definition function without using a helper function

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:

Upvotes: 1

Views: 103

Answers (1)

András Kovács
András Kovács

Reputation: 30103

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.

Upvotes: 1

Related Questions