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

Question

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

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

由于涉及到iff，先演示一个方向，从左到右：

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

    (assume h : p ∨ (q ∧ r),

        or.elim h

            (assume hp : p, 

                show (p ∨ q) ∧ (p ∨ r), from ⟨or.inl hp, or.inl hp⟩)

            (assume hqr : q ∧ r,

                have hq : q, from hqr.left,
                have hr : r, from hqr.right,

                show (p ∨ q) ∧ (p ∨ r), from  ⟨or.inr hq, or.inr hr⟩))

要转到另一个方向，我们必须证明：

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

根据本书目前为止所展示的示例，这一示例的不同之处在于左侧涉及两个 or 表达式...所以它好像我必须使用 or.elim 两次...

我弄乱了一些方法。这是将一个 or.elim 嵌套在另一个中的一个：

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

    (assume h : (p ∨ q) ∧ (p ∨ r),

        have hpq : p ∨ q, from h.left,
        have hpr : p ∨ r, from h.right,

        or.elim hpq

            (assume hp : p,

                show p ∨ (q ∧ r), from or.inl hp)

            (assume hq : q, 

                or.elim hpr

                    (assume hp : p,

                        show p ∨ (q ∧ r), from or.inl hp)

                    (assume hr : r,

                        show p ∨ (q ∧ r), from or.inr ⟨hq, hr⟩)))

这里让我感到奇怪的一件事是以下表达式出现了两次：

(assume hp : p,

    show p ∨ (q ∧ r), from or.inl hp)

有没有不涉及这种重复的方法？

是否有更惯用的方法？

Answer 1

你的方法，使用 Theorem Proving In Lean 中教授的第一种方法，在精益数学库中的代码是以战术模式（本书稍后介绍）或以全学期模式。这是一个战术模式证明：

import tactic.rcases -- advanced mathlib tactics, to speed things up a bit
variables (p q r : Prop)

example : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
begin
  rintro ⟨hpq,hpr⟩,
  cases hpq, -- this is or.elim
    left, assumption, -- first show
  cases hpr, -- second or.elim
    left, assumption, -- second show
  right, exact ⟨hpq, hpr⟩
end

我在这里也看不出如何避免重复代码——left, assumption 扮演着 assume, show 的角色。如果您想避免导入，可以将 rintro 行更改为 intro h, cases h with hpq hpr,.

虽然这种逻辑证明可以很容易地写成直接项模式：

example (p q r : Prop) : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
λ ⟨hpq, hpr⟩, or.elim hpq or.inl $ λ hq, or.elim hpr or.inl $ λ hr, or.inr ⟨hq, hr⟩

现在的"duplication"只是函数or.inl出现了两次。我的感觉是，因为 p 可以从假设中以两种不同的方式得到证明，所以你需要在某处重复，因为你处于两个不同的 "threads" 论证中。一旦您理解了 Lean 的 _ 孔功能的强大功能，建立这样的术语就不难了。例如，在构建此 lambda 项的过程中，我的会话如下所示：

example (p q r : Prop) : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
λ ⟨hpq, hpr⟩, or.elim hpq or.inl $ _

洞口的错误准确地告诉我需要构建哪个术语来填充它。

最后，正如@jmc 所说，像这样的事情只能用战术来解决，这实际上可能是解决这个目标的惯用方法：

import tactic.tauto

example (p q r : Prop): (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
by tauto!

注意这里的导入。 Lean 的数学库 mathlib（所有导入均来自该库）不仅仅是一个数学库，数学家在那里创造数学，但计算机科学家也制定强大的策略，这让每个人（不仅仅是数学家）的生活变得更好。

如果您还有其他问题，获得答案的更有效方法是在 the Lean chat at Zulip 上提问，也许在#new members stream 中提问。那里的一个团队通常可以非常有效地处理事情。

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

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

lean