ヘルパー関数を使用しない定義関数

Question

私はSoftware Foundationsを読み、その問題を解決しています。これは私が定義しようとしている定義のいずれかです。

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

基本的にはハスケルの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 ([],[]). 

I持っている二つの質問：

• それはsplit2このようなヘルパー関数を使用せずにsplitを定義することは可能ですか？
• Coqにはwhere節（Haskellのような）がありますか？

Answer 1

Coqにletがあります。あなたは、標準のハスケル定義を翻訳することができます。++の二次的な性能を避けてください：

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.