Lean中如何将非负整数Z转换为自然数N（处理异质等式）

好问题！既然你已经明确知道输入的整数a : Int是非负的，完全可以利用这个前提来简化转换，不用依赖nat_abs（毕竟它还要额外处理负数分支）。在Lean里有几种优雅且高效的方式来实现：

1. 直接使用Int.toNat（推荐） #

Int.toNat是Lean专门为非负整数转自然数设计的函数，它的类型签名是(a : Int) → a ≥ 0 → Nat——正好要求你传入非负性的证明，完美匹配你的场景。

示例代码：

-- 封装成可复用的函数
def nonneg_z_to_nat (a : Int) (h : a ≥ 0) : Nat :=
  Int.toNat a h

-- 使用示例：当你有非负假设时直接调用
example (a : Int) (h : a ≥ 0) : Nat := nonneg_z_to_nat a h

这个方法的优势在于：

• 完全利用了你已知的a ≥ 0前提，避免了不必要的分支判断
• Lean会在编译时确保你确实满足非负条件，类型安全有保障

2. 在已有假设的上下文中直接内联使用 #

如果你的代码上下文（比如定理证明、局部作用域）里已经存在a ≥ 0的假设h，可以直接内联调用Int.toNat，不用额外封装函数：

example (a : Int) (h : a ≥ 0) : Nat :=
  let n := Int.toNat a h
  -- 在这里可以直接使用n进行后续操作
  n

3. 利用have生成临时证明（如果需要） #

如果你的非负条件不是直接作为参数传入，而是可以通过其他前提推导出来，还可以用have临时生成非负性证明：

example (a : Int) (h : a = 5) : Nat :=
  have h_nonneg : a ≥ 0 := by rw [h]; norm_num
  Int.toNat a h_nonneg

为什么不用nat_abs？ #

nat_abs的实现是分情况处理的（判断整数正负），当你已经明确a ≥ 0时，Int.toNat是更直接、更高效的选择——Lean的编译器会优化这个路径，不会产生多余的分支逻辑。

内容的提问来源于stack exchange，提问作者ScarletAmaranth