精益中整数的归纳创建非整数类型

如何解决精益中整数的归纳创建非整数类型

我想对一个整数变量使用归纳法，在正负方向上做一个归纳步骤。

考虑以下定理（为了演示，不管它是否有意义）：

theorem exmpl (x : ℤ) : (x = 5):=
begin
  induction x,-- inductive steps
end

在精益策略状态下产生：

case int.of_nat
x: ℕ
⊢ int.of_nat x = 5

case int.neg_succ_of_nat
x: ℕ
⊢ -[1+ x] = 5

合理地，归纳产生两种情况，一种为正方向，一种为负方​​向。但同时发生的情况是 x 现在变成了一个自然数，并且在目标中它变成了 int.of_nat x 和 -[1+ x]。

由于我的归纳在整数内部运行，我会假设这些类型是它们的某种“子集”，大概比整数具有更多有用的属性。 Lean Reference 声明第二个似乎是“应该由类型类解析推断的隐式参数”，但没有进一步解释这意味着什么。

虽然这种转换对于某些应用程序可能是必要的，但在我的用例中，我只想继续使用整数，并且还没有找到将目标转换回使用整数的好方法。

所以我的问题是：

• 这些新类型 x 被转换成什么类型​​，它们的含义是什么以及转换为什么有意义？
• 而且，更重要的是：如何将目标改回可以再次使用整数的情况？

提供更多背景信息： 我是一名具有一些编程和数学知识但没有使用证明助手的背景的学生。我最近通过 Natural Number Game 发现了 Lean，现在正在尝试使用整数。

解决方法

精益中的归纳策略使用基于类型定义的归纳原则。对于自然数，这种归纳原理是众所周知的。对于整数，定义有点不直观，并给出了一个不太有用的归纳原理。

在精益中，整数被定义为自然数的两个副本的不相交并集。这为您提供了从 nat 到 int 的两个函数，将 n 发送到 n 的规范嵌入，以及将 n 发送到 -(n + 1) 的另一个映射。每个整数都是唯一的形式 n 或 -(n + 1) 对于 n 自然数，整数归纳原理基本上考虑了这两种情况，这不是那么有用。在精益中，这两个从 nat 到 int 的映射称为 int.of_nat 和 int.neg_succ_of_nat，而 -[1+ x] 是 int.neg_succ_of_nat 的表示法。

所以尽管 induction 将 x 变成了自然数，但 int.of_nat x 和 -[1+ x] 仍然都是整数。

如果您想要一种更有用的整数归纳方法，您可以使用 mathlib int.induction_on 中定义的定理 data.int.basic https://leanprover-community.github.io/mathlib_docs/data/int/basic.html 您可以通过导入此文件来使用它（在 mathlib 网站上有关于安装和导入 mathlib 文件的文档）和使用 induction x using int.induction_on（此方法并不总是有效）或诸如 apply int.induction_on x 或 refine int.induction_on x _ _ _ 之类的东西也可能有效。>

还值得一提的是，在精益中处理整数时很少使用归纳法，而且大多数情况下您只是使用库定理来证明您想要的大部分内容。

,

为了补充 Christopher Hughes 的回答，int 类型在 Lean 3 核心中定义为：

inductive int : Type
| of_nat : nat → int
| neg_succ_of_nat : nat → int

见here。

当所讨论的 induction 类型不是递归时，induction x 策略（即 cases x）的工作原理与 inductive 相同，而 int 不是-- 它的构造函数（例如 of_nat 和 neg_succ_of_nat）都没有将 int 作为参数（该类型仅作为输出出现）。因此，为了证明精益中的 int 成立，您需要证明这些情况中的每一个都成立（没有额外的归纳假设）。然而，正如 Christopher Hughes 所指出的，关于 int 的许多常见属性和定理已经得到证明，并且可以在 Lean 3 核心库本身或 mathlib 中使用。然后，您可以使用这些定理作为构建块来证明更复杂的概念。