如何在精益学习中证明r→(∃x:α，r)
如何在精益学习中证明r→(∃x:α，r)
提问于 2019-11-25 04:43:56
我试图证明逻辑语句r → (∃ x : α, r)，其中r是Prop (命题或语句)，α是Type。我已经通过书中的练习证明了精益中的一些东西，但我被困在了这一点上。
我真的不确定我甚至不明白为什么会这样。由于不存在类型为α的x，无人居住的α不会使这句话成为一种错误的陈述吗？
我最大的“尝试”是希望精益的讲述者能填上我需要的东西，
theorem t5_2: r → (∃ x : α, r) :=
assume rx: r,
⟨_, rx⟩但是它不能推导出α类型的东西，这是有意义的。2)我也认为这可能是一个非建设性的证明，所以我想做一个矛盾的证明。然而，我在纸上得到的最多的是
¬ (∃ x : α, r) → (∀ x : α, ¬ r) → ??我不确定如何在lean中执行第一个隐含，即使我执行了，我仍然需要一个α类型的x来消除∀。
如有任何提示，我们将不胜感激。
回答 1
Stack Overflow用户
回答已采纳
发布于 2019-12-30 05:08:08
这句话通常是不正确的。α可以是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⟩页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/59022225
复制相关文章
相似问题
腾讯云开发者
