如何在Lean的证明块内部正确定义自定义函数？

Lean 证明块内定义函数的方法 #

可以在战术模式的证明块内定义函数，核心是使用let战术而非have：

• let会完整保留项的定义内容，适合定义需要用到具体实现的函数
• have仅保留项的类型，适合证明命题，无法调用定义的具体实现

正确示例

针对你提到的依赖证明内变量x的函数场景，有两种常用写法：

1. lambda表达式写法

theorem exmpl (x : ℕ) : false :=
begin
  let f : ℕ → ℕ := λ n, n + x,
  -- 后续可直接调用f，定义可被rfl识别
  have h : f 3 = 3 + x := rfl,
end

2. 直接带参数的定义写法

theorem exmpl (x : ℕ) : false :=
begin
  let f (n : ℕ) : ℕ := n + x,
  -- 效果和lambda写法完全一致
  have h : f 0 = x := rfl,
end

之前写法失败的原因

• 第一种写法have f (n : ℕ) : n := n + 1存在语法错误：冒号后应填写返回值类型，你填写的n是自然数变量而非类型
• 第二种用have定义函数的写法逻辑错误：have定义的项仅保留类型，系统不会记录它的具体实现，后续无法验证函数的定义性质

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