如何在精益中证明 r → (∃ x : α, r)

Question

我正在尝试证明逻辑命题 r → (∃ x : α, r)，其中 r 是 Prop（命题或命题），α 是 Type.通过书中的练习，我已经在精益中证明了一些事情，但我仍然坚持这一点。

我真的不确定我什至不明白为什么这是真的。由于 α 类型的 x 不存在，α 无人居住不会使这成为一个错误的陈述吗？

我最好的 "attempts" 是 1) 希望 lean 的阐述者能填写我需要的内容，

theorem t5_2: r → (∃ x : α, r) :=
  assume rx: r,
    ⟨_, rx⟩

但它不能推断出 α 类型的东西，这是有道理的。并且 2) 我还认为这可能是一个非构造性证明，所以我正在考虑通过反证法进行证明。然而，我在纸上得到的最远的是

  ¬ (∃ x : α, r) → (∀ x : α, ¬ r) → ??

我不确定如何在精益中执行第一个暗示，即使我这样做了，我仍然需要一个 α 类型的 x 来消除 ∀ .

如有任何提示，我们将不胜感激。

Answer 1

一般来说，这种说法是不正确的。 α 可以是 empty:

example : ¬ ∀ (α : Type) (r : Prop), r → (∃ x : α, r) :=
begin
  intro h,
  cases h empty _ true.intro with w,
  cases w
end

如果你假设 [inhabited α]

，你可以证明原来的陈述

example (α : Type) [inhabited α] (r : Prop) : r → (∃ x : α, r) :=
λ h, ⟨inhabited.default α, h⟩

How to prove r → (∃ x : α, r) in Lean