类型论中的零除：常见问题解答

不是的。它只是意味着精益/符号并不意味着数学除法。让我们表示实数。让我们用if和来定义一个函数。给出这样的定义会给我们带来数学上的矛盾吗？不，当然不是！这只是一个定义。LEAN使用符号/来表示意思。顺便说一句，就像Coq、AGDA等一样，Lean称它为real.div，而不是。

这似乎肯定会导致推特上的混乱。但在定理证明器中进行数学运算时，这并不会导致混淆。数学家不会被0除以，因此在实践中他们从来没有注意到real.div和数学除法(1/0没有定义)之间的区别。事实上，如果一个数学家问Lean认为1/0是什么，人们可能会问数学家为什么要问这个问题，因为我们都知道，数学中不允许除以0，因此这与他们的工作不相关。实际上，知道real.div与知道数学除法是一样的；任何关于一个定理的定理都会转化为关于另一个定理的定理，所以拥有real.div等同于拥有数学除法。

情况变得更糟了。在自然数上定义了一个减法自然数，记号为x-y，它吃掉两个自然数，然后吐出另一个自然数。如果x和y是ℕ和x<；y类型的项，则x-y将为0。有一个名为real.sqrt的函数，它接受一个实数作为输入，然后输出一个实数。如果你给它，它就会输出。除了保证输出实数之外，我不知道如果给它输入会发生什么。也许是0。可能是1。也许是37。我不在乎。我是一个数学家，如果我想取负实数的平方根，我不会使用real.sqrt，因为我不想要实数形式的答案，而real.sqrt的类型是ℝ→ℝ。

问得好！我在2017年就试过了！事实证明，在定理证明器中这真的很不方便！

以下是我学习精益的方法。我是以“普通数学家”的身份来到这里的，当时我正在考虑将精益融入他们本科的“证明导论”课程。我以前没有使用定理证明器的经验，也没有正式的编程背景。作为一项可行性研究，我试着用精益来做我计划给本科生做的所有问题单。这要追溯到2017年，当时Lean的数学库要小得多，real.sqrt还不存在。然而，SUPS和INFS的基本理论已经形式化，所以我定义了real.sqrt x，对于x非负，是，并证明了人们在平方根函数的接口中想要的基本定理，例如AND等等(这里是非负实数，我的函数将接受的唯一实数)。

然后，我开始证明，这是我课程中一张习题纸上的一个问题。学生们被告知不要使用计算器，并被要求找到一个只使用代数操作的证明，即real.sqrt的接口。当然，按照我设置的方式，每次使用符号时，我都必须提供一个证明，证明我所取的平方根是非负的。每次符号出现在我的证据里。即使我已经在前一行证明了2&>0，我也必须在这一行再次证明，因为这行也有一个入口。当然，证明只是通过Normnum，但是我很快就厌倦了输入10个字符。

然后我在精益聊天中抱怨这一点，被嘲笑我愚蠢的数学家惯例，并展示了惯用的精益方法。惯用的方法是允许像负数这样的垃圾输入到平方根函数中，然后返回垃圾输出。人们把非负性假设放在定理中。例如，定理的陈述有这样的假设。请注意，它也没有假设，因为人们可以在证明中推导出这一点，而不会用它来打扰用户。这与数学家的方法相反，在数学家的方法中，证明也需要提供，因为在某种意义上，它是符号的一部分。

不，不太喜欢。我的意思是，它(A)在数学上等同于我们数学家目前所做的，(B)只是在用依赖类型理论形式化数学时更方便。

究竟什么是田野呢？对于数学家来说，域是一个集合，其中逆函数仅定义为非零。字段的非零元素形成一个组，因此我们有诸如for之类的公理(这对它甚至没有意义)。比方说，我们遇到了一个外星人物种，他们也发现了领域，但他们的设置涉及到一个功能，而不是我们的。它们是使用我们的符号、for和定义的。他们的公理当然和我们的是一样的，比如他们有。他们有一个额外的公理，但这没什么大不了的。它是摆动和环形交叉口-他们定义了，他们的定理不需要，而我们的则需要。它们只是使用略微不同的符号来表达相同的概念。它们是不连续的。我们的并不是到处都有定义。但是，在我们的字段类别和他们的字段类别之间存在典型的类别同构。这两种设置在数学上没有区别。

利恩使用的是外星物种公约。外星人‘是Lean的field.inv，Lean的field.div x y被定义为field.mul(x，field.inv y)。

好的，所以我可以看到它是可以工作的。为什么我对这一切仍然感到有点不舒服？

这可能是出于以下原因。您正在想象一个计算机校对人员将检查您的工作，特别是检查您是否被零除过，如果您除过零，那么您预计它会抛出一个错误，说明您的证明是无效的。您需要内化的是，Lean只是在使用上面由for和定义的函数。特别是，你不能通过应用形式的输入来证明错误的东西，因为通过除以零然后继续来获得矛盾的方法将涉及到引用对于数学除法为真但对于数学除法不为真的定理。例如，也许一位数学家会说，这对所有人都是正确的，隐含的假设是，这可以从符号中推断出来。Lean定理real.div a=1只有在假设的情况下才能证明，所以该定理不能在。换句话说，这个问题只是在争论的另一个点上出现了。Lean不会接受您在第8行偷偷地除以0的证明，但是失败将发生在参数的不同点。然而，失败仍然是断言你有一个分母，但你没有证明它是非零的。它不会发生在你做除法的时候，它会发生在你调用定理的时候，而这个定理对real.div是不成立的。

感谢吉姆·普罗普和亚历克斯·康托洛维奇在推特上提出这一问题。我希望这能澄清一些事情。

这篇文章发表在“学习精益”、“M1F”、“M40001”、“类型论”、“本科生数学和标记除法”、“除以零”上。为固定链接添加书签。