1

在经历了大多数练习并在 LEAN 手册第 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
4

1 回答 1

1

暗示。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
于 2020-01-15T19:22:44.820 回答