6
私はCoqに騙されています。具体的には、私はmergesortを実装しようとしているし、それが動作することを証明しようとしています。CoqのFixpointの制限？
実装での私の試みがされた：私はこの結果として取得
Fixpoint sort ls :=
match ls with
| nil => nil
| cons x nil => cons x nil
| xs =>
let (left, right) := split xs nil nil
in merge (sort left) (sort right)
end.
エラーは以下のとおりです。これらのエラーの
Error:
Recursive definition of sort is ill-formed.
In environment
sort : list nat -> list nat
ls : list nat
x : nat
l : list nat
y : nat
l0 : list nat
left : list nat
right : list nat
Recursive call to sort has principal argument equal to "left" instead of
one of the following variables: "l" "l0".
Recursive definition is:
"fun ls : list nat =>
match ls with
| nil => nil
| x :: nil => x :: nil
| x :: _ :: _ =>
let (left, right) := split ls nil nil in merge (sort left) (sort right)
end".
私の解釈では、LとL0はなしLSであるということですその頭、x、lsとxの後ろの要素（これはyと呼ぶことにしたと思います）。私がこれらのリストの1つで再帰しなかったのは悲しいことであり、代わりにローカルで定義されたリストに再帰しました。
私はパターンマッチから直接来たものだけを再帰させることができますか？はいの場合、これは厳しい制限のようです。その周りに道がありますか？私は、Coqが関数が終了することを伝えることができないと推測しています。左と右がxよりも小さいことを証明する方法はありますか？
http://adam.chlipala.net/cpdt/html/GeneralRec.html
よく設立再帰と呼ばれるセクションを読んで、それをソートするために十分な根拠再帰を使用してマージを実装しています