пример: (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r)

Раздел 3.6 доказательства теорем в 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)

Есть ли подход, исключающий такое дублирование?

Есть ли более идиоматический подход?


lean
person dharmatech    schedule 16.10.2019    source источник
comment
Последний блок кода, вероятно, можно сократить до or.inl. Если вы хотите использовать тактику, все доказательство, скорее всего, может быть уменьшено до by tauto (я не проверял это).   -  person jmc    schedule 16.10.2019

Ответы (1)


arrow_upward
3
arrow_downward

Ваш подход, основанный на использовании первого метода, описанного в доказательстве теорем в 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 может быть доказано двумя способами, отличными от гипотезы, вам понадобится где-то дублирование, потому что вы находитесь в двух разных «нитях» аргументации. Подобные термины нетрудно составить, если вы поймете всю мощь функциональности Lean _ отверстий. Например, на полпути к построению этого лямбда-члена мой сеанс выглядел так:

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 (из которой происходит весь импорт) - это не просто математическая библиотека, математики создают там математику, но компьютерные ученые также создают мощные тактики, которые улучшают жизнь всех (не только математиков).

Если у вас есть еще вопросы, гораздо более эффективный способ получить ответ - просто задать их в чате Lean в Zulip, возможно, в потоке #new members. Команда людей там обычно очень эффективно справляется с делами.

person Kevin Buzzard    schedule 16.10.2019