coq - coq 中自然数的欧几里德划分

Question

Coq 标准库中是否有对自然数进行欧几里德除法的函数？我一直无法找到一个。如果没有，那么从数学上讲，是否有理由不应该有一个？

我想要这个的原因是因为我试图将一个列表分成两个较小的列表。我希望一个列表的大小大约是另一个列表的一半，所以我正在计算 (length xs)/2。

Answer 1

这可能是您正在寻找的:

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