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

Question

第3.6节定理证明在精益说明如下：

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, _)