精益证明:通过举例证明存在量词

Question

我是一个精益证明器的初学者，我在下面的例子中遇到了一点困难:

我需要证明下面的

∃x, f x

其中f是精益文件前面定义的函数。这看起来很简单，我可以很容易地用英语提供证明(至少我认为这是正确的):

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

然而，把它翻译成精益给了我一些问题。我试过使用"让"关键字来构造任意的y, f成立，但我不确定如何使用这个y来证明我的目标

∃x, f x

我的想法正确吗?我该如何解决这个问题?

Answer 1

在Lean中，类型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