示例：((p ∨ q) → r) → (p → r) ∧ (q → r)

Question

Section 3.6 of Theorem Proving in Lean 显示如下：

example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := sorry

让我们关注从左到右的方向：

example : ((p ∨ q) → r) → (p → r) ∧ (q → r) := sorry

构建此示例的好方法是什么？

如果我采用这样的方式（使用下划线以便我们可以指明整体方法）：

example : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
    (assume hpqr : (p ∨ q) → r,
        (assume hpq : p ∨ q,
            or.elim hpq 
                (assume hp : p,
                    show (p → r) ∧ (q → r), from and.intro _ _)
                (assume hq : q,
                    show (p → r) ∧ (q → r), from and.intro _ _)))

我们得到：

如果我们将其重组为：

example (hpqr : ((p ∨ q) → r)) : (p → r) ∧ (q → r) := 
    (assume hpq : p ∨ q,
        or.elim hpq 
            (assume hp : p,
                show (p → r) ∧ (q → r), from and.intro _ _)
            (assume hq : q,
                show (p → r) ∧ (q → r), from and.intro _ _))

我们似乎离得更近了一点：

第 3 章似乎没有涉及左侧 ∧ 和 → 的其他有效示例。

欢迎就如何解决这个问题提出任何建议！

更新

下面是基于 Yury 推荐的方法：

example : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
    (assume hpqr : (p ∨ q) → r,
        (and.intro
            (assume hp : p, hpqr (or.inl hp))
            (assume hq : q, hpqr (or.inr hq))))

原来很简单。 :-)

更新

这是一个处理双向的 iff 版本：

example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=

    iff.intro

        (assume hpqr : (p ∨ q) → r,
            show (p → r) ∧ (q → r), from
                (and.intro
                    (assume hp : p, hpqr (or.inl hp))
                    (assume hq : q, hpqr (or.inr hq))))

        (assume hprqr : (p → r) ∧ (q → r),
            show ((p ∨ q) → r), from
                (assume hqr : p ∨ q,
                    or.elim hqr
                        (assume hp : p, hprqr.left hp)
                        (assume hq : q, hprqr.right hq)))

Answer 1

您在本示例的假设中没有 p ∨ q。因此，您必须从 (assume hpqr, _) 直接转到 and_intro。我的意思是，类似

example (p q r : Prop) : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
assume hpqr,
and.intro (assume p, _) (assume q, _)

示例：((p ∨ q) → r) → (p → r) ∧ (q → r)

example : ((p ∨ q) → r) → (p → r) ∧ (q → r)

lean