Coq QArith 除以零就是零，为什么？

我注意到在 Coq 的有理数定义中，零的倒数被定义为零。 （通常，除以零是没有明确定义/合法/允许的。）

Require Import QArith.
Lemma inv_zero_is_zero: (/ 0) == 0. 
Proof. unfold Qeq. reflexivity. Qed.

为什么会这样呢？

它会导致有理数计算出现问题吗？或者安全吗？

简短的回答是：是的，绝对安全。

当我们说除以零没有明确定义时，我们实际上的意思是零没有乘法逆元。特别是，我们不能有一个函数来计算零的乘法逆元。然而，它is可以编写一个函数来计算所有其他元素的乘法逆元，并在这样的逆元不存在时返回某个任意值（例如零）。这正是这个函数正在做的事情。

在任何地方都定义这个逆运算符意味着我们将能够定义用它进行计算的其他函数，而不必明确争论它的参数不为零，从而使其使用起来更方便。事实上，想象一下如果我们让这个函数返回一个option相反，当我们将其传递为零时就会失败：我们必须使整个代码成为一元代码，从而使其更难以理解和推理。如果编写一个需要证明其参数非零的函数，我们也会遇到类似的问题。

那么，有什么问题呢？好吧，当尝试prove关于使用逆运算符的函数的任何内容，我们都必须添加明确的假设，表明我们向它传递了一个不同于零的参数，或者认为它的参数可以never为零。关于这个函数的引理然后得到额外的前提条件，例如

forall q, q <> 0 -> q * (/ q) = 1

许多其他库的结构也是如此，参见。例如定义场公理 http://ssr.msr-inria.inria.fr/~jenkins/current/Ssreflect.ssralg.html在 MathComp 的代数库中。

There are在某些情况下，我们希望将某些函数所需的附加前提条件内化为类型级约束。例如，当我们使用时，这就是我们所做的长度索引向量和一个保险箱get只能对范围内的数字调用的函数。那么，在设计库时，我们如何决定选择哪一个，即是使用具有大量额外信息的丰富类型并防止对某些函数的虚假调用（如长度索引的情况），还是忽略此信息并要求它作为显式引理（如乘法逆情况）？好吧，这里没有明确的答案，人们确实需要单独分析每种情况，并决定哪种替代方案更适合该特定情况。