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

Question

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

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

有没有更地道的方法？

Answer 1

使用精益定理的证明中教授的第一种方法的方法并不是真正的惯用，因为精益的数学库中的代码要么是以战术模式编写的(在本书后面讨论过)，要么是以完整的方式编写的。这里有一个战术模式证明：

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!

注意这里的进口。精益的数学库mathlib不仅仅是一个数学库，数学家在那里创造了数学，计算机科学家也制定了强有力的策略，这使得每个人(不仅仅是数学家)的生活变得更好。

如果您还有更多的问题，获得答案的一个更有效的方法就是在在祖利普的精益聊天上提问，也许是在#新成员流中。那里的一组人通常处理事情的效率很高。