Lean Prover中存在量词∃ x, f x的证明方法咨询

你的思路完全正确——构造满足f y的具体y，再用这个y完成存在性证明，是这类存在性目标的标准构造性证明路径。

核心实现步骤 #

• 先确定一个具体的y，使得f y成立（这一步需要结合f的定义来选，比如如果f是判断自然数是否为偶数，就选y=2）
• 用Lean的存在性引入规则，把这个y和f y的证明结合起来，完成目标

代码示例（以Lean 4为例） #

假设我们有一个已定义的函数f：

def f (n : Nat) : Bool := n > 0

基础写法（用let绑定变量）

example : ∃ x, f x := by
  let y := 1  -- 构造满足条件的y
  exists y    -- 将目标转化为证明f y成立
  simp [f]    -- 展开f的定义，验证f y为真

简洁写法（直接指定y）

不需要let也能完成，直接在exists里给出构造的y：

example : ∃ x, f x := by
  exists 1
  simp [f]

复杂场景（依赖引理证明f y）

如果f y的证明需要更多步骤，可以先单独证好引理再用：

-- 先证明y=1满足f y
lemma f_1_valid : f 1 := by simp [f]

example : ∃ x, f x := by
  exists 1
  exact f_1_valid  -- 直接调用已证引理完成证明

Lean 3的对应写法 #

语法略有差异，但逻辑一致：

def f (n : nat) : bool := n > 0

example : ∃ x, f x :=
begin
  existsi 1,
  simp [f],
end

关键说明 #

let只是用来给构造的y起个名字，真正完成存在性证明的是exists（Lean 4）或existsi（Lean 3）——这个指令会把原目标∃ x, f x转化为f y，你只需要补上f y的证明即可。

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