精益证明者：通过提供示例证明存在量词

Question

我是 lean prover 的初学者，我在下面的例子中遇到了一些困难：

我需要证明以下内容

∃ x, f x

其中 f 是先前在 lean 文件中定义的函数。这看起来很简单，我可以轻松地提供英文证明（至少我认为这是正确的）：

1. 构造一个任意的 y 使得 f y 成立。
2. 通过构造一个 f y 成立的任意 y，我们已经证明了目标 ∃ x, f x

然而，将其转化为精益给我带来了一些问题。我尝试使用“let”关键字构造一些 f 成立的任意 y，但我不确定如何使用这个 y 来证明我的目标

∃ x, f x

我的想法对吗？我该如何解决这个问题？

Answer 1

在精益中，类型

Exists

被定义为归纳类型，如下所示：

inductive Exists {α : Sort u} (p : α → Prop) : Prop
| intro (w : α) (h : p w) : Exists

所以尝试写

refine Exists.intro y _,

（如果在战术模式下）或

let y := ... in Exists.intro _

（如果在术语模式下）并查看

_

需要什么。

Answer 2

使用战术模式：

lemma testproof : ∃ x : nat, x > 5 :=
begin
  apply exists.intro 6,
  dec_trivial,
end

#check testproof  -- testproof : ∃ (x : ℕ), x > 5

直接使用 Exists（使用

@

传递否则会被推断的参数）：

def testproof' := @Exists.intro nat (λ x, x > 5) 6 dec_trivial

#check testproof'  -- testproof' : ∃ (x : ℕ), x > 5