1

精益定理证明的第 3.6 节显示以下内容：

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)

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

有没有更惯用的方法？

4

1 回答 1

3

你的方法，使用Theorem Proving In Lean中讲授的第一种方法，在 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⟩

or.inl现在的“重复”只是函数出现两次的事实。我的感觉是，因为p可以从假设以两种不同的方式证明，所以你需要在某个地方重复，因为你处于论证的两个不同“线程”中。_一旦您了解了精益的空洞功能的强大功能，这样的术语就不难建立。例如，在构建这个 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（所有导入的来源）不仅仅是一个数学库，数学家在那里制作数学，但计算机科学家也制定了强大的策略，这让每个人（不仅仅是数学家）的生活都更好。

如果您还有其他问题，获得答案的一种更有效的方法是在 Zulip 的 Lean 聊天中提问，也许是在 #new members 流中。那里的一群人通常非常有效地处理事情。

于 2019-10-16T07:53:29.147 回答