如何证明精益中的分布性(命题有效性属性6)？
如何证明精益中的分布性(命题有效性属性6)？
提问于 2020-01-16 02:57:42
在经历了大多数练习，并在精益手册第3章末尾的精益中解决/证明了前五个命题有效性/性质之后，我仍然无法理解以下含义(证明性质6所需的含义之一)：
theorem Distr_or_L (p q r : Prop) : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
begin
intros pqpr,
have porq : p ∨ q, from pqpr.left,
have porr : p ∨ r, from pqpr.right,
sorry
end我面临的困难主要是因为当p不是真的时，因为我不知道如何使用精益工具将假设中and的两个方面结合起来，以获得在该场景下q和r都必须成立的事实。我非常感谢这里的任何帮助；请帮助我理解如何在上面的设置中构造这个证明，而不引入除标准精益之外的任何其他策略。为了完整性，这里是我对另一个方向的证明：
theorem Distr_or_R (p q r : Prop) : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) :=
begin
intros pqr,
exact or.elim pqr
( assume hp: p, show (p ∨ q) ∧ (p ∨ r), from
and.intro (or.intro_left q hp) (or.intro_left r hp) )
( assume hqr : (q ∧ r), show (p ∨ q) ∧ (p ∨ r), from
and.intro (or.intro_right p hqr.left) (or.intro_right p hqr.right) )
end回答 1
Stack Overflow用户
回答已采纳
发布于 2020-01-16 03:22:45
提示。在porq和porr上尝试大小写拆分。
这里有一个解决方案
theorem Distr_or_L (p q r : Prop) : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
begin
intros pqpr,
have porq : p ∨ q, from pqpr.left,
have porr : p ∨ r, from pqpr.right,
{ cases porq with hp hq,
{ exact or.inl hp },
{ cases porr with hp hr,
{ exact or.inl hp },
{ exact or.inr ⟨hq, hr⟩ } } }
end页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/59757965
复制相关文章
相似问题
腾讯云开发者
