Lean定理证明：((p∨q)→r)→(p→r)∧(q→r)证明结构咨询

左→右方向的证明思路与实现 #

要搞定 ((p ∨ q) → r) → (p → r) ∧ (q → r) 这个证明，核心是把大目标拆成小任务：先接收前提 (p ∨ q) → r，再分别证出 p → r 和 q → r，最后用合取引入规则把它们拼起来就行。

具体拆解步骤：

• 先假设前提 hpqr : (p ∨ q) → r
• 证 p → r：先假设 hp : p，用 or.inl hp 把单个 p 包装成 p ∨ q，再传给前提 hpqr 就能得到 r
• 证 q → r：逻辑类似，假设 hq : q，用 or.inr hq 生成 p ∨ q，再通过前提推导 r
• 最后用 and.intro 把两个蕴含式合并成合取式

对应的Lean代码实现：

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

完整双向等价式的证明 #

如果要完成整个等价式 ((p ∨ q) → r) ↔ (p → r) ∧ (q → r)，需要用 iff.intro 同时处理左→右和右→左两个方向：

• 右→左方向：先假设合取式 hprqr : (p → r) ∧ (q → r)，然后假设 p ∨ q，用 or.elim 分情况讨论：如果是 p 就用合取的左部分 hprqr.left 推 r，如果是 q 就用右部分 hprqr.right 推 r

完整代码：

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

其实这个证明的关键就是熟练用Lean里的基础逻辑规则：合取的and.intro/访问左右项、析取的or.inl/or.inr/or.elim，还有蕴含式的假设引入规则，把大目标拆成一个个小问题逐步解决就清晰多了。

内容的提问来源于stack exchange，提问作者dharmatech