coq - Coq QArith 除以零是零，为什么？

Question

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

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

为什么会这样？

它会导致有理数计算出现问题，还是安全？

Answer 1

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

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

在任何地方都定义这个逆运算符意味着我们将能够定义用它计算的其他函数，而不必明确地争论它的参数不是零，这使得它更方便使用。确实，想象一下如果我们让这个函数返回一个option而不是当我们将它传递为零时会失败：我们将不得不使我们的整个代码单子化，使其更难理解和推理。如果编写一个需要证明其参数不为零的函数，我们将遇到类似的问题。

那么，有什么问题呢？好吧，当试图证明关于使用逆运算符的函数的任何事情时，我们将不得不添加明确的假设，即我们正在向它传递一个不同于零的参数，或者认为它的参数永远不会为零。然后关于这个函数的引理得到额外的先决条件，例如

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

许多其他库的结构都是这样的，参见。例如MathComp 代数库中域公理的定义。

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