Coq 標準ライブラリに自然体のユークリッド除算を実行する関数はありますか? 私はそれを見つけることができませんでした。存在しない場合、数学的に、存在してはならない理由はありますか?
これが必要な理由は、リストを 2 つの小さなリストに分割しようとしているからです。1 つのリストをもう 1 つのリストの約半分のサイズにしたいので、(長さ xs) / 2 を計算しています。
Coq 標準ライブラリに自然体のユークリッド除算を実行する関数はありますか? 私はそれを見つけることができませんでした。存在しない場合、数学的に、存在してはならない理由はありますか?
これが必要な理由は、リストを 2 つの小さなリストに分割しようとしているからです。1 つのリストをもう 1 つのリストの約半分のサイズにしたいので、(長さ xs) / 2 を計算しています。
これはあなたが探しているものかもしれません:
http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Numbers.Natural.Abstract.NDiv.html
その他のユークリッドの事柄:
http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Arith.Euclid.html
http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Numbers.NatInt.NZDiv.html
http://coq.inria.fr/distrib/V8.4/stdlib/Coq.ZArith.Zdiv.html
http://coq.inria.fr/distrib/V8.4/stdlib/Coq.ZArith.Zeuclid.html