如何在定理证明中展开let表达式？解决unknown constant报错

问题根源 #

你用let在证明块内定义的F是局部绑定变量，并非全局命名空间下的常量。而delta和unfold这两个tactic的核心作用是展开全局定义的常量（比如用def在定理外声明的函数），它们会去_root_根命名空间查找对应的常量，但局部let的F根本没被注册到这里，所以会报unknown constant '_root_.F'的错误。

正确的处理方式 #

对于局部let绑定的变量，需要用能处理局部绑定的tactic来展开定义，常用的有：

• dsimp [F]：简化局部绑定的表达式，直接展开F的定义
• change 0 ≤ 1：手动替换F n为它的定义值（适合简单场景）
• simp [F]：自动展开并完成后续简单证明

修正后的代码示例：

example : True := by
  let F : ℕ→ℕ := λ _ => 0
  have F_le_1 : ∀(n:ℕ), F n ≤ 1 := by
    intro n
    dsimp [F] -- 展开局部定义的F
    trivial -- 此时目标变为0 ≤ 1，直接完成证明
  trivial

补充差异说明 #

如果在定理外用def F : ℕ→ℕ := λ _ => 0定义，F会被注册为_root_.F全局常量，此时delta F就能正常找到并展开——这就是为什么全局定义不会报错的原因。

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