Lean 4递归定义pop的自然数下溢疑问：为何通过类型检查？

你困惑的核心在于对Lean 4中自然数（Nat）减法的特性不熟悉，以及没注意到类型约束已经帮你规避了潜在的逻辑问题：

• Lean的Nat减法是截断式的：和常规编程语言里的整数减法不同，Lean中Nat类型的减法不会出现“下溢报错”。当被减数小于减数时，结果直接返回0，比如0 - 1在Lean里的值就是0，不会触发任何错误。
• 类型约束保证递归合法性：你的代码里有前置条件r:n <= st.length，当匹配到h::t分支时，st.length等于t.length + 1（由len_succ定理证明），结合r可得n <= t.length + 1。通过Nat.sub_le_iff_le_add定理，这个条件等价于n - 1 <= t.length——这正好是递归调用pop t (n-1)所需的前置条件。哪怕n=0，n-1=0，此时0 <= t.length也天然成立（因为列表长度是非负自然数），所以递归调用的类型检查完全合法。

简单说，Lean的Nat减法本身不会报错，再加上类型约束的保障，你的代码才能顺利通过类型检查。

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