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

【问题标题】：Induction on integers in Lean creates non-int types精益中整数的归纳创建非整数类型
【发布时间】：2021-10-06 21:34:13
【问题描述】：

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

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

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 发现了精益，现在正在尝试使用整数。

【问题讨论】：

标签： types type-conversion induction lean

【解决方案1】：

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

在精益中，整数被定义为两个自然数副本的不相交并集。这为您提供了从 nat 到 int 的两个函数，规范嵌入将 n 发送到 n，另一个映射将 n 发送到 -(n + 1)。每个整数都是唯一的 n 或 -(n + 1) 的形式，对于 n 是自然数，整数的归纳原理基本上考虑了这两种情况，这不是那么有用。在 Lean 中，这两个从 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 data.int.basic 中定义的定理 int.induction_on https://leanprover-community.github.io/mathlib_docs/data/int/basic.html 您可以通过导入此文件来使用它（有关于 imstalling 和在 mathlib 网站上导入 mathlib 文件）并使用 induction x using int.induction_on（这种方法并不总是有效）或类似 apply int.induction_on x 或 refine int.induction_on x _ _ _ 的东西也可能有效。

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

【讨论】：

【解决方案2】：

补充一点 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 不是——它的构造函数都不是（例如@ 987654329@ 和 neg_succ_of_nat) 将 int 作为参数（该类型仅作为输出出现）。因此，要证明精益中的int 成立，您需要证明这些情况中的每一个都成立（没有额外的归纳假设）。然而，正如 Christopher Hughes 所指出的，许多关于 int 的常见属性和定理已经被证明，并且可以在 Lean 3 核心库本身或 mathlib 中使用。然后，您可以使用这些定理作为构建块来证明更复杂的概念。

【讨论】：