在Lean中定义证明中的函数

Question

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

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

对我不起作用。在lean中定义证明中的函数是可能的吗?您将如何实现？

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

Answer 1

在一个策略证明中，您有用于新定义的have和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