如何证明r→（∃x：α，r）在精益中

Question

我正在尝试证明逻辑语句r → (∃ x : α, r)，其中r是Prop（命题或陈述），α是Type。通过本书的练习，我已经在“精益”中证明了一些东西，但是我仍然坚持这一观点。

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

我最好的“尝试”是1）希望精益细化者能满足我的需求，

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⟩