我想对一个整数变量使用归纳法,在正负方向上做一个归纳步骤。
考虑以下定理(为了演示,不管它是否有意义):
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,现在正在尝试使用整数。