lean - 从 Lean 中的正整数中恢复 nat

Question

鉴于(a : Z)和(a >= 0)，我想有(n : N)这样的n = a。这当然有点麻烦，因为n = a是异构平等。

我发现nat_abswhich 做了类似的事情，除了当我有一个负整数时它也处理这种情况，我知道我没有。

在精益中如何处理这种情况？

Answer 1

n = a不是异质平等，因为您（希望）无法证明N = Z. 你所能期望的最好的就是int.of_nat n = a，你应该能够证明a >= 0这一点int.of_nat (nat_abs a) = a。

请注意，您可以编写 a = n，它会输入 check ，因为 Lean 会强制n转换为int.of_nat n. 这不是异质相等，而是Z.