在精益证明中定义一个函数

Question

在精益中，我们可以这样定义一个函数

def f (n : ℕ) : ℕ := n + 1

然而，在证明中这不再可能。以下代码无效：

theorem exmpl (x : ℕ) : false :=
begin
  def f (n : ℕ) : ℕ := n + 1,
end

我假设可以用 have 来代替，但尝试像

theorem exmpl (x : ℕ) : false :=
begin
  have f (n : ℕ) : n := n + 1,
  have f : ℕ → ℕ := --some definition,
end

对我不起作用。是否可以在精益证明中定义一个函数，您将如何实现？

（在上面的例子中，可以在证明之前定义它，但你也可以想象像f (n : ℕ) : ℕ := n + x这样的函数，它只能在引入x之后定义）

Answer 1

在策略证明中，您有 have and let 新定义的策略。 have 策略会立即忘记除新定义类型之外的所有内容，它通常只用于命题。相比之下，let 策略会记住定义的值。

这些策略没有在冒号左侧包含参数的语法，但您可以使用 lambda 表达式：

theorem exmpl (x : ℕ) : false :=
begin
  let f : ℕ → ℕ := λ n, n + 1,
end

（尝试将 let 更改为 have 以查看上下文如何变化。）

另一种方法是在策略证明之外使用 let 表达式。这些表达式在冒号之前确实有参数语法。例如，

theorem exmpl (x : ℕ) : false :=
let f (n : ℕ) : ℕ := n + x
in begin
  
end

Define a function inside of a proof in Lean