不使用辅助函数的定义函数

Question

我一直在阅读软件基础并解决其中的问题。这是我要定义的定义之一：

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

基本上它是 haskell 的 unzip 版本。

我是这样实现的：

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 ([],[]).

我有两个问题：

是否可以在不使用像 split2 这样的辅助函数的情况下定义 split？
在 Coq 中是否有等同于 where 子句（如 Haskell 中的）？

Answer 1

Coq 中有 let。您可以而且应该只翻译标准 Haskell 定义，避免 ++:

的二次性能

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.

不使用辅助函数的定义函数

Definition function without using a helper function

coq