proofs.md

Упражнения по формальным доказательствам

Нет времени объяснять, переходим сразу к делу.

Инструменты

Доказывать теоремы мы будем, используя интерактивные пруверы Isabelle или Lean 3. Примеры приводятся для каждого прувера, для решения задач же можно использовать любой из них.

Эти пруверы поддерживают юникод, и мы будем использовать юникодные символы. Для ввода юникода в Windows и Linux существуют WinCompose и XCompose соответственно. Следующая конфигурация позволяет вводить основные логические символы:

<Multi_key> <f> <i> : "∈"
<Multi_key> <f> <a> : "∀"
<Multi_key> <f> <e> : "∃"
<Multi_key> <f> <t> : "∧"
<Multi_key> <f> <v> : "∨"
<Multi_key> <f> <asciitilde> : "¬"
<Multi_key> <f> <u> : "∪"
<Multi_key> <f> <n> : "∩"
<Multi_key> <f> <s> : "⊆"
<Multi_key> <f> <S> : "⊇"
<Multi_key> <f> <l> : "λ"
<Multi_key> <f> <bracketleft> : "⟨"
<Multi_key> <f> <bracketright> : "⟩"
<Multi_key> <f> <braceleft> : "←"
<Multi_key> <f> <braceright> : "→"
<Multi_key> <f> <slash> : "≠"
<Multi_key> <f> <less> : "≤"
<Multi_key> <f> <greater> : "≥"

Например, ∃ вводится нажатием клавиши Compose, затем клавиши f и затем клавиши e.

Объяснять, как установить пруверы в систему мы не будем. Скажем лишь, что в случае Isabelle следует использовать поставляемый с ним редактор JEdit, когда же для Lean есть расширение к Visual Studio Code.

Если используется Visual Studio Code, то нужно убедиться, что используемый шрифт полноценно поддерживает математические символы. Одним из таких шрифтов является Iosevka.

Правила игры

Формальное доказательство это вывод некоторого заключения из данных предположений, используя логические правила вывода, аксиомы и утверждения уже доказанных теорем. Мы сначала рассмотрим правила вывода для пропозиционной логики используя Isabelle.

Создайте файл Logic.thy в Isabelle/JEdit со следующим содержанием:

theory Logic
  imports Main
begin

end

Между begin и end мы и будем писать утверждения лемм и их доказательства. Но сначала — правила.

Пропозиционная логика

Синтаксис:

• Метапеременные: P, Q, Foo, …
• ¬P читается как «не P»
• P ∧ Q читается как «P и Q»
• P ∨ Q читается как «P или Q»
• P ⟶ Q читается как «из P следует Q»
• P ⟷ Q читается как «P тогда и только тогда, когда Q»

Стрелка в Isabelle/JEdit пишется как -->. Кроме того, в Isabelle есть ещё одна стрелка:

• P ⟹ Q (пишется ==>): предположив P, можно доказать Q

Эта стрелка является частью металогики Isabelle, и нужна лишь там, где явно требуется именно доказательство. Кроме того, с её помощью мы будем писать правила вывода.

Стрелки правоассоциативны: P ⟶ Q ⟶ R это то же, что P ⟶ (Q ⟶ R).

Правила имеют следующий вид: ⟦P1; ...; Pn⟧ ⟹ Q. Здесь P1, ..., Pn это предположения, когда же Q это выводимое из предположений заключение. В случае, когда предположение только одно, мы пишем просто P ⟹ Q.

Правила для ⟶ выглядят следующим образом:

impI: "(P ⟹ Q) ⟹ P ⟶ Q"
mp:   "⟦P ⟶ Q; P⟧ ⟹ Q"

Первое правило говорит о том, что если предположив P можно доказать Q, то из P следует Q. Второе, с латинским названием modus ponens, позволяет из того, что если из P следует Q, и того, что P истинно, вывести Q.

Теперь правила для ∧:

conjI: "⟦P; Q⟧ ⟹ P ∧ Q"
conjunct1: "(P ∧ Q) ⟹ P"
conjunct2: "(P ∧ Q) ⟹ Q"

conjI позволяет вывести истинность P ∧ Q из того, что P истинно и Q истинно. Остальные два позволяют вывести, соответственно, P и Q из P ∧ Q.

Интереснее выглядят правила для ∨:

disjI1: "P ⟹ P ∨ Q"
disjI2: "Q ⟹ P ∨ Q"
disjE:  "⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R"

Естественно спросить: а какое же Q появляется в выводе disjI1? Ответ: можно выбрать совершенно любое Q. Правило disjE же говорит, что если P ∨ Q, и из P, и из Q можно доказать R, то выбора нет: R истинно.

Ещё интереснее правила для отрицания:

FalseE: "False ⟹ P"
notI: "(P ⟹ False) ⟹ ¬P"
notE: "⟦¬P; P⟧ ⟹ R"

False означает ложь или абсурд. Из абстурда следует что угодно, и если из P следует абсурд, то должно быть верно, что не P. notE же позволяет вывести что угодно из того, что одновременно и P, и не P.

Наконец, правила для ⟷:

iffI: "⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P ⟷ Q"
iffD1: "⟦P ⟷ Q; P⟧ ⟹ Q"
iffD2: "⟦P ⟷ Q; Q⟧ ⟹ P"

Их мы обсуждать не будем.

С помощью всех этих правил мы можем доказывать различные утверждения. В Isabelle они имеют вид:

lemma foo:
  assumes P1 and P2 ... and Pn
  shows Q

Сразу же после леммы должно идти её доказательство. Доказательство имеет вид:

proof -
  assume ⟨label⟩: A1
  have ⟨label⟩: C1 using ⟨assums⟩ ⟨proof⟩
  have ⟨label⟩: C2 using ⟨assums⟩ ⟨proof⟩
  ...
  show Q using assums ⟨proof⟩
qed

Здесь ⟨label⟩ это имя промеждуточного утверждения, ⟨assums⟩ — факты, требуемые методу для доказательства утверждения, а ⟨proof⟩ это его доказательство. Доказательство может использовать какое-то из правил или метод, а может в свою очередь быть блоком proof ... qed. Кроме того, в качестве заглушки для доказательства можно использовать sorry.

Примеры доказательств

Сформулируем и докажем следующее утверждение:

1. Солнце или дождь
2. Однако, не солнце
3. Значит, дождь

lemma sunny_rainy:
  assumes sr: "Sunny ∨ Rainy" and ns: "¬Sunny"
  shows "Rainy"
proof -
  have 1: "Sunny ⟹ Rainy"
  proof -
    assume s: Sunny
    show "Rainy" using ns s by (rule notE)
  qed
  
  have 2: "Rainy ⟹ Rainy"
  proof -
    assume r: Rainy
    show Rainy using r by assumption
  qed

  show "Rainy" using sr 1 2 by (rule disjE)
qed

Что здесь можно увидеть:

1. Мы применяем правило следующим образом: (rule name). При этом мы должны перечислить необходимые предпосылки используя using
2. by assumption использует предположение напрямую

Это достаточно громоздкое доказательство даже по меркам формальных доказательств с полным отсутствием какой-либо автоматизации. Мы можем его сократить.

1. Не обязательно явно вводить предположение с помощью assume
2. Если блок доказательства содержит только show R by .., то весь блок можно заменить на by ..

Применяя эти соображения, получаем:

lemma sunny_rainy:
  assumes sr: "Sunny ∨ Rainy" and ns: "¬Sunny"
  shows "Rainy"
proof -
  have 1: "Sunny ⟹ Rainy" using ns by (rule notE)
  have 2: "Rainy ⟹ Rainy" by assumption

  show "Rainy" using sr 1 2 by (rule disjE)
qed

Однако, это доказательство можно ещё сократить. Если мы применим правило disjE в обратную сторону, то общая цель доказательства распадётся на две, которые можно доказать по отдельности.

Конкретно, это делается так:

lemma sunny_rainy:
  assumes sr: "Sunny ∨ Rainy" and ns: "¬Sunny"
  shows "Rainy"
proof (rule disjE[OF sr])
  show "Sunny ⟹ Rainy" using ns by (rule notE)
  show "Rainy ⟹ Rainy" by assumption
qed

Здесь мы с помощью OF указываем sr в качестве предположения для disjE.

Вообще, даже самая слабая автоматизация может доказать подобное утвеждение без явного использования правил:

lemma sunny_rainy:
  assumes sr: "Sunny ∨ Rainy" and ns: "¬Sunny"
  shows "Rainy"
  using sr ns by clarify

И мы будем её использовать. Но потом, когда перейдём от голой логики к арифметике.

А сейчас рассмотрим ещё одно утверждение и его доказательство:

lemma or_distr:
  assumes pqr: "P ∧ (Q ∨ R)"
  shows "(P ∧ Q) ∨ (P ∧ R)" (is ?th)
proof -
  have p: P using pqr by (rule conjunct1)
  have qr: "Q ∨ R" using pqr by (rule conjunct2)

  show ?th
  proof (rule disjE[OF qr])
    show ?th if q: Q
      apply(rule disjI1)
      using p q by (rule conjI)
    show ?th if r: R
      apply(rule disjI2)
      using p r by (rule conjI)
  qed
qed

Здесь мы дали цели доказательства имя с помощью (is ?th). Кроме того, мы использовали if, чтобы ввести предположение перед тем, как доказывать утверждение.

Ещё мы использовали apply, чтобы преобразовать цель перед тем, как её доказывать. apply(...) действует аналогично proof (...), но при этом не требует введение нового блока. Кроме того, apply позволяет применять правила друг за другом: apply(rule foo) apply(rule bar).

Доказательства в Lean

Если Isabelle основан на естественном выводе в логике высшего порядка, то Lean использует совсем другое основание: зависимые типы. Тем не менее, формальные доказательства в Lean весьма схожи с доказательствами в Isabelle.

Главное отличие между Isabelle и Lean заключается в стрелке: она только одна, и означает тип функций из значений одного типа в значения другого типа. Modus ponens это просто применение функции, когда же введение предположения это лямбда-абстракция.

Смотря шире, Lean пологается на соответствие Карри-Говарда: высказывание это тип, доказательство это выражение имеющее этот тип.

Следующие функции являются аналогом правил вывода в Isabelle:

and.intro      : P → Q → P ∧ Q
and.elim_left  : P ∧ Q → P
and.elim_right : P ∧ Q → Q

or.inl      : P → P ∨ Q
or.inr      : Q → P ∨ Q
or.cases_on : P ∨ Q → (P → R) → (Q → R) → R

false.elim : false → P

iff.intro : (P → Q) → (Q → P) → (P ↔ Q)
iff.mp    : (P ↔ Q) → P → Q
iff.mpr   : (P ↔ Q) → Q → P

ВАЖНО: → это короткая стрелка. Она отличается от длинной стрелки ⟶, которая используется в Isabelle.

Вместо and.intro p q можно писать просто ⟨p, q⟩, а вместо and.elim_left h можно писать h.1. ¬P на самом деле является сахаром для P → false.

Доказательства будем писать в файл logic.lean. В отличие от Isabelle, он шапки не требует.

Формулировка теоремы в Lean выглядит следующим образом:

lemma sunny_rainy {sunny rainy : Prop}
  (sr : sunny ∨ rainy) (ns : ¬sunny) : rainy :=

В отличие от Isabelle, мы должны указать, что sunny и rainy являются утверждениями.

Мы могли бы написать доказательство так, как пишут программы:

let
  if_sunny (s : sunny) : rainy := false.elim (ns s),
  if_rainy (r : rainy) : rainy := r
in
  or.cases_on sr if_sunny if_rainy

Но мы так делать не будем. Вместо этого мы будем использовать тактики:

lemma sunny_rainy {sunny rainy : Prop}
  (sr : sunny ∨ rainy) (ns : ¬sunny) : rainy :=
begin
  cases sr with s r,
  show rainy, from false.elim (ns s),
  show rainy, from r
end

Тактика cases sr действует аналогично rule disjE[OF sr] и расскладывает исходную цель на две новые. with s r вводит соответствующие предположения для каждой из целей.

show указывает текущую цель, когда же from предоставляет выражение в качестве доказательства цели.

Теперь доказательство or_dirsr:

lemma or_distr {P Q R : Prop}
  (pqr : P ∧ (Q ∨ R)) : (P ∧ Q) ∨ (P ∧ R) :=
begin
  let th := (P ∧ Q) ∨ (P ∧ R),
  have p : P, from pqr.1,
  have qr : Q ∨ R, from pqr.2,

  cases qr with q r,
    show th, { apply or.inl, from ⟨p, q⟩ },
    show th, { apply or.inr, from ⟨p, r⟩ }
end

let определяет значение в блоке. Чтобы ввести промежуточные факты, используется have. Фигурные скобки же аналогичны блоку proof и позволяют ограничить доказательство единственной целью. apply действует так же, как apply в Isabelle, который мы применяли перед доказательством. В Lean apply можно применять в любой части доказательства.

Выразительность Lean позволяет записать это доказательство ещё короче:

lemma or_distr {P Q R : Prop}
  (pqr : P ∧ (Q ∨ R)) : (P ∧ Q) ∨ (P ∧ R) :=
begin
  let th := (P ∧ Q) ∨ (P ∧ R),
  cases pqr.2 with q r,
    show th, from or.inl ⟨pqr.1, q⟩,
    show th, from or.inr ⟨pqr.1, r⟩
end

Ещё одна важная тактика это assume. Она позволяет вводить предположения, требуемые для доказательства цели. Например:

lemma pq_nq {P Q : Prop}
  (pq : P → Q) (nq : ¬Q) : ¬P :=
begin
  assume p : P,
  have q : Q, from pq p,
  show false, from nq q,
end

Двойное отрицание

Рассмотренные нами правила составляют конструктивную логику. В классической логике же существует ещё так называемый закон двойного отрицания:

notnotD: "¬¬P ⟹ P"

Доказательство называется конструктивным, если оно использует только правила конструктивной логики и другие конструктивные доказательства.

По ряду причин, конструктивные доказательства являются предпочтительными. Поэтому в Lean нужно явно добавлять open classical в начало файла, чтобы закон двойного отрицания стал доступен. Соответствующая функция называется by_contradiction.

Правилом, равносильным двойному отрицанию, является закон исключения третьего:

excluded_middle: "¬P ∨ P"

В Lean соответствующая функция называется em, и используется так: em P.

Упражнения

Все упражнения имеют вид Q, ⟦P1; ...; Pn⟧ ⟹ Q или P ⟹ Q, что означает, что предполагая P1, ..., Pn нужно доказать Q.

Для доказательства следует использовать Isabelle или Lean 3. Решать все упражнения не обязательно. Важно лишь понимать, как они в принципе могут быть решены

Простые:

• P ∧ Q ⟹ Q ∧ P
• P ∧ (Q ∧ R) ⟹ (P ∧ Q) ∧ R

---

• P ⟹ (Q ⟶ P)
• P ⟶ Q ⟶ R ⟹ (P ∧ Q) ⟶ R
• ⟦(P ⟶ Q); (Q ⟶ R)⟧ ⟹ (P ⟶ R)
• ⟦(P ⟶ Q ⟶ R); (P ⟶ Q)⟧ ⟹ (P ⟶ R)

---

• ¬(P ∨ Q) ⟹ ¬P ∧ ¬Q
• ¬P ∨ Q ⟹ P ⟶ Q

---

• P ⟶ (Q ∧ R) ⟹ (P ⟶ Q) ∧ (P ⟶ R)
• (P ∨ Q) ⟶ R ⟹ (P ⟶ R) ∧ (Q ⟶ R)

Сложнее:

• (P ∨ Q) ∨ R ⟹ P ∨ (Q ∨ R)
• (P ∧ Q) ∨ (P ∧ R) ⟹ P ∧ (Q ∨ R)
• P ∨ (Q ∧ R) ⟹ (P ∨ Q) ∧ (P ∨ R)

Требующие двойного отрицания или исключения третьего:

• P ⟶ Q ⟹ ¬P ∨ Q
• ¬(P ∧ Q) ⟹ ¬P ∨ ¬Q
• ¬P ⟶ Q ⟹ ¬Q ⟶ P
• ((P ⟶ Q) ⟶ P) ⟹ P (⋆)

(⋆: при доказательстве полезно использовать утверждения других упражнений)

Предикаты и кванторы

Пропозициональная логика невыразительна: в ней нельзя даже выразить нечто столь простое, как «существует число больше нуля». Чтобы формулировать подобные высказывания, нужны кванторы.

Но сначала нам нужны предикаты. Предикат это по-сути функция из некоторого набора значений в логическое значение. Например, в Isabelle мы можем определить предикат, истинный для положительных чисел следующим образом:

definition positive :: "nat ⇒ bool" where
  "positive n ⟷ n > 0"

Но мы этого делать не будем. Вместо этого, мы будем рассматривать утверждения, включающие произвольные предикаты.

В синтаксисе появляются два новых символа:

• ∀x. P x, читается как «для всех x (верно) P x»
• ∃x. P x, читается как «существует такое х, что (верно) P x»

Кроме того, есть мета-символ ⋀x. P(x), означающий, что P(x) можно доказать для любого x.

Эти символы захватывают всё, что справа, то есть, например, ∀x. P x ⟶ Q x это то же, что и ∀x. (P x ⟶ Q x).

Вместо P x под этими символами могут быть любые логические выражения, которые используют или не используют x. Переменные работают те же, как и в программировании, и мы их обсуждать не будем.

Правила вывода для ∀:

allI: "(⋀x. P x) ⟹ (∀x. P x)"
spec: "(∀x. P x) ⟹ P y"

Если можно доказать P x для любого x, то для всех x верно P x. Кроме того, если P x для всех x, то верно утверждение, где на место x подставленно некоторое конкретное y.

Правила вывода для ∃:

exI: "P y ⟹ ∃x. P x"
exE: "⟦(∃x. P x); (⋀y. P y ⟹ Q)⟧ ⟹ Q

Если P y для некотого конкретного y, то существует такое x, что P x. И если существует такое x, что P x, и для любого y можно доказать, что из P y следует Q, то тогда Q.

Перейдём к примерам. Следующий пример показывает, как работать с ∀:

lemma all_and:
  assumes apq: "∀y. P y ∧ Q y"
  shows "(∀x. P x) ∧ (∀x. Q x)" (is "?ap ∧ ?aq")
proof (rule conjI)
  show ?ap
  proof (rule allI)
    fix x
    have pq: "P x ∧ Q x" using apq by (rule spec)
    show "P x" using pq by (rule conjunct1)
  qed

  show ?aq
  proof (rule allI)
    fix x
    have pq: "P x ∧ Q x" using apq by (rule spec)
    show "Q x" using pq by (rule conjunct2)
  qed
qed

Здесь мы обозначили ∀x. P x как ?ap и ∀x. Q x как ?aq. Применение conjI позволяет разложить цель на две, а применение allI позволяет перейти сразу к доказательству ⋀x. P x.

Чтобы доказать ⋀x. P x, мы фиксируем произвольное x, и затем доказываем утверждения, используя это x как конкретное значение.

Теперь пример для ∃:

lemma ea_swap:
  assumes eap: "∃x. ∀y. P x y"
  shows "∀b. ∃a. P a b" (is ?th)
proof (rule exE[OF eap])
  fix x
  assume ay_p: "∀y. P x y"

  show ?th
  proof (rule allI)
    fix b
    have pxb: "P x b" using ay_p by (rule spec)
    show "∃a. P a b" using pxb by (rule exI)
  qed
qed

rule exE[OF eap] позволяет заполучить x, но в последующем доказательстве он должен быть произволен.

В доказательстве мы могли бы всюду использовать x и y, вместо того, чтобы вводить переменные a и b. Причина, почему мы так не делаем проста: нет смысла путаться в буквах и натыкаться на непонятные ошибки, когда есть возможность этого не делать.

В Isabelle есть специальная конструкция, позволяющая использовать exE не создавая дополнительный блок:

lemma ea_swap:
  assumes eap: "∃x. ∀y. P x y"
  shows "∀b. ∃a. P a b" (is ?th)
proof (rule allI)
  obtain x where ay_p: "∀y. P x y"
    using eap by (rule exE)
  fix b

  have pxb: "P x b" using ay_p by (rule spec)
  show "∃a. P a b" using pxb by (rule exI)
qed

Все переменные в Isabelle имеют тип, и мы можем указать конкретный тип у переменной следующим образом: x :: type. Это позволяет доказать следующее утверждение:

lemma all_exists:
  assumes ap: "∀x :: nat. P x"
  shows "∃x. P x" (is ?th)
proof -
  have 0: "P 0" using ap by (rule spec)
  show ?th using 0 by (rule exI)
qed

У Isabelle есть ещё одна особенность, которой нет у пруверов, использующих зависимые типы: любой тип в Isabelle населён. И для любого типа 'a, undefined является некоторым конкретным произвольным значением этого типа.

То есть лемму выше можно обобщить:

lemma all_exists:
  assumes ap: "∀x. P x"
  shows "∃x. P x" (is ?th)
proof -
  have 0: "P undefined" using ap by (rule spec)
  show ?th using 0 by (rule exI)
qed

Мы эту особенность Isabelle использовать не будем. В Lean типы могут быть пусты, и потому в нём это утверждение является ложным.

Равенство

В Isabelle/HOL для любого типа 'a определён бинарный предикат = типа 'a ⇒ 'a ⇒ Bool со следующими аксиомами:

refl: "t = t"
subst: "s = t ⟹ P s ⟹ P t"

Первая говорит, что любое значение t равно самому себе. Второе же говорит, что если s и t равны, и верно, что P s, то тогда и P t.

С помощью этих двух свойств можно доказать остальные свойства равенства. Например:

lemma eq_sym:
  assumes st: "s = t"
  shows "t = s" (is ?th)
proof (rule subst[OF st])
  show "s = s" by (rule refl)
qed

lemma eq_trans:
  assumes rs: "r = s" and st: "s = t"
  shows "r = t"
proof (rule subst[where ?P="λx. r = x"])
  show "s = t" using st by assumption
  show "r = s" using rs by assumption
qed

В случае eq_sym, мы передали равенство правилу, и Isabelle сам догадался, что в качестве предиката P следует использовать λt. t = s. В случае же eq_trans, мы явно указали предикат, и затем использовали show чтобы показать истинность соответствующих предпосылок subst.

Мы не будем уделять много внимания равенству, вместо этого просто перечислим полезные леммы в стандартной библиотеке:

lemma sym:       "s = t ⟹ t = s"
lemma ssubst:    "t = s ⟹ P s ⟹ P t"
lemma trans:     "⟦r = s; s = t⟧ ⟹ r = t"
lemma trans_sym: "r = s ⟹ t = s ⟹ r = t"

Предикаты и кванторы в Lean

Синтаксис (указание типа обычно можно опустить):

• ∀x : T, P x
• ∃x : T, P x

В Lean ∀ это просто тип функций. И вместо allI и spec используются просто лямбда-абстракция и применение функции.

Вся соль заключается в типах. Что такое доказательство P → Q? Это всего лишь значение соответствущего типа: функция, которая берёт свидетельство того, что P истинно (значение типа P) и возвращает свидетельство того, что Q истинно (значение типа Q).

Аналогично, функция типа ∀x : A, P x берёт на вход некоторое значение x типа A, и возвращает значение типа P x. Но при этом тип возвращаемого значения зависит от значения, переданного в функцию! Например, если мы передали функции типа ∀x : nat, P x число 42, то в результате получаем значение типа P 42.

{P Q : Prop} что вы видели в сигнатурах функциях это тоже аргументы, только неявные.

Тип ∃ в Lean же определён следующим образом:

inductive Exists {α : Sort u} (p : α → Prop) : Prop
| intro (w : α) (h : p w) : Exists

Это зависимая пара: значение w типа α вместе со значением типа p w. То есть, это значение вместе со свидетельством того, что значение удволетворяет предикату.

Для ∃ определены функции, аналогичные соотвествующим правилам вывода:

exists.intro : ∀ (w : A), P w → (∃ (x : A), P x)
exists.elim  : (∃ (x : A), P x) → (∀ (a : A), P a → Q) → Q

Вместо exists.intro w pw можно просто писать ⟨w, pw⟩.

all_and доказывается следующим образом в Lean:

lemma all_and {A : Type*} {P Q : A → Prop}
  (apq : ∀x, P x ∧ Q x) : (∀x, P x) ∧ (∀x, Q x) :=
begin
  apply and.intro,
  show (∀x, P x),
    { assume x, from (apq x).1 },
  show (∀x, Q x),
    { assume x, from (apq x).2 }
end

Мы дожны указать, что A являтся типом, и что P и Q это предикаты.

Фиксирование переменной никак не отличается от введения предположения. И в самом деле, используя лямбда-абстракцию, мы можем записать это доказательство короче:

lemma all_and {A : Type*} {P Q : A → Prop}
  (apq : ∀x, P x ∧ Q x) : (∀x, P x) ∧ (∀x, Q x) :=
begin
  apply and.intro,
  show (∀x, P x), from (λ x, (apq x).1),
  show (∀x, Q x), from (λ x, (apq x).2),
end

Теперь доказательство ea_swap:

lemma ea_swap {A B : Type*} {P: A → B → Prop}
  (eap : ∃x, ∀y, P x y) : ∀b, ∃a, P a b :=
begin
  cases eap with x ay_p,
  assume b,

  have pxb: P x b, from ay_p b,
  show (∃a, P a b), from ⟨x, pxb⟩
end

Тактика cases позволяет достать значение вместе со свидетельством того, что оно соответствует предикату. Затем мы собираем значение типа ∃a, P a b из значения x и свидетельства pxb.

Теперь перечислим некоторые функции для равенства:

eq.refl  : ∀(a : A), a = a
eq.subst : (s = t) → P s → P t

eq.symm  : (s = t) → (t = s)
eq.trans : (r = s) → (s = t) → (r = t)

Упражнения

В том же формате, что и раньше.

Простые:

• (∀x. ∀y P x y) ⟹ (∀y. ∀x. P x y)
• (∃x. ∃y P x y) ⟹ (∃y. ∃x. P x y)
• (¬∃x. P x) ⟹ (∀x. ¬(P x))
• ((∃x. P x) ⟶ Q) ⟹ (∀x. P x ⟶ Q) (⋆)
• ((∀x. P x ⟶ Q) ⟹ (∃x. P x) ⟶ Q)

Сложнее:

• (∃x. P x) ∨ (∃x. Q x) ⟹ (∃x. P x ∨ Q x)
• (∀x. P x) ∨ (∀x. Q x) ⟹ (∀x. P x ∨ Q x)

Требующие исключения третьего:

• (¬∀x. P x) ⟹ (∃x. ¬(P x))(⋆⋆)

(⋆: шапка в lean имеет вид {A : Type*} {P : A → Prop} {Q : Prop})

(⋆⋆: полезно использовать результаты других упражнений)

Арифметика

Логическая часть кончилась, и теперь мы можем позволить себе использовать автоматизацию! В Isabelle/HOL её много разной, но важнейшими методами являются simp и auto.

Читатель, который радовался удобству и изяществу Lean, может перестать это делать: в этом интерактивном прувере метода, аналогичного auto нет. К счастью, мы сможем обойтись одним лишь simp.

Мы создадим простую теорию для арифметики. Создайте файл arith.lean со следующим содержанием:

inductive nah
| zero : nah
| suc : nah → nah

open nah

instance : has_zero nah := ⟨zero⟩
instance : has_one nah := ⟨suc zero⟩

def add : nah → nah → nah
| n 0 := n
| n (suc k) := suc (add n k)

instance : has_add nah := ⟨add⟩

Мы определили новый тип! Он называется nah и представляет собой натуральное число. Вместе с типом, одновременно определены и следующие функции:

nah      : Type
nah.zero : nah
nah.suc  : nah → nah

nah.rec {T : nah → Sort l} : T zero → (∀k : nah, T k → T k.suc) → (∀n : nah, T n)

Первые три это конструктор типа и конструкторы значения типа. При этом suc n можно также писать как n.suc.

Последняя функция намного интереснее: она определяет одновременно и индукцию, и рекурсию для типа nah. Здесь T это отображение значения типа nah в тип уровня l. Утверждения в Lean (Prop) являются типами нулевого уровня, большинство типов (Type) же являются типами первого уровня.

Если мы определим def f : (∀n : nah, T n) := nah.rec base next, то функции base и next имеют следующий смысл:

• base вычисляет значение f zero
• Для любого k, next вычисляет значение f (suc k), используя значение f k

Всё вместе позволяет вычислять f для любого значения типа nah. Если T является предикатом, то это соответствует индукции над типом nah. В общем случае же, это просто примитивно рекурсивная функция.

open nah позволяет писать просто zero и suc вместо nah.zero и nah.suc. instance : has_zero nah и instance : has_one nah позволяют же писать 0 вместо zero и 1 вместо suc zero.

Дальше мы рекурсивно определяем сложение двух чисел. В более привычной записи оно выглядит как n + (k + 1) := (n + k) + 1.

Мы могли бы определить add с помощью nah.rec:

def add (n : nah) : nah → nah :=
  @nah.rec (λ _, nah) n (λ k add_n_k, suc add_n_k)

@ перед nah.rec позволяет указать неявный аргумент этой функции.

Наконец, instance : has_add nah позволяет писать n + k вместо add n k.

Теперь мы готовы доказывать теоремы. Сначала докажем результат, которому была посвящена значительная часть Principia Mathematica Рассела:

lemma one_add_one : 1 + 1 = suc 1 :=
by exact eq.refl (suc 1)

Как любой порядочный язык программирования, Lean умеет вычислять выражения. Причём эти выражения могут содержать переменные:

lemma add_zero {n : nah} : n + 0 = n     := by refl  -- то же, что и `exact eq.refl n`
lemma add_one  {n : nah} : n + 1 = suc n := by refl

Одной лишь β-редукции, однако, недостаточно, чтобы доказать 0 + n = n. Но мы можем доказать это индуктивно:

lemma zero_add {n : nah} : 0 + n = n :=
begin
  induction n with n ih,
  show zero + zero = zero, refl,
  show 0 + n.suc = n.suc,
    have s: 0 + n.suc = (0 + n) + 1, refl,
    rw [s, ih], refl
end

Тактика induction позволяет не использовать nat.rec явно. Для второй цели она вводит следующие предположения: n : nah и ih: 0 + n = n.

Тактика rw позволяет переписывать части цели с помощью равенства. В данном примере, она сначала преобразует цель 0 + n.suc = n.suc в (0 + n) + 1 = n.suc, используя s. Затем, она преобразует (0 + n) + 1 = n.suc в n + 1 = n.suc, используя ih. Затем refl завершает доказателство цели.

Эта тактика понимает выражения буквально, и считает 0 и zero разными выражениями. Поэтому могут быть полезны тривиальные леммы вроде add_zero.

rw это достаточно императивный способ манипулировать равенством. calc позволяет записать то же доказательство более декларативно:

lemma zero_add {n : nah} : zero + n = n :=
begin
  induction n with n ih,
  show zero + zero = zero, refl,
  calc
    zero + n.suc = (zero + n) + 1 : by refl
             ... = n + 1          : by rw ih
end

Упражнение: доказать следующую лемму с помощью индукции по k:

lemma suc_add {n k : nah} : n.suc + k = suc (n + k) :=
sorry

Замечание: упражнения и примеры являются частью теории. Не забываем пополнять arith.lean.

Теперь докажем ассоциативность сложения:

lemma add_assoc {n k p : nah} : (n + k) + p = n + (k + p) :=
begin
  induction p with p ih,
  show (n + k) + 0 = n + (k + 0), refl,
  calc
    (n + k) + p.suc = suc ((n + k) + p) : by refl
    ... = suc (n + (k + p)) : by rw ih
    ... = n + (k + p.suc) : by refl
end

Простое, очевидное доказательство. Однако, его можно сократить:

lemma add_suc {n k : nah} : n + k.suc = suc (n + k) := by refl

lemma add_assoc {n k p : nah} : (n + k) + p = n + (k + p) :=
begin
  induction p with p ih,
  show (n + k) + 0 = n + (k + 0), refl,
  show (n + k) + p.suc = n + (k + p.suc), simp [add_suc, ih]
end

simp это автоматизированная версия rw: она итеративно применяет сразу набор равенств. Кроме равенств она ещё может применять и функции.

Если rw или simp дано равенство eq: a = b, то в цели a заменяется на b. Если наоборот, нужно заменить b на a, то вместо eq в тактику следует передавать ←eq.

simp может автоматически применять леммы, помеченные как @[simp]. Здесь есть определённые тонкости, так что мы будем указывать все необходимые леммы явно.

Упражнение: используя simp, доказать add_comm:

lemma add_comm {n k : nah} : n + k = k + n :=
sorry

Теперь докажем add_left_comm:

lemma add_left_comm {n k p : nah} : n + (k + p) = k + (n + p) :=
calc
  n + (k + p) = (n + k) + p : by rw ←add_assoc
          ... = (k + n) + p : by rw @add_comm k
          ... = k + (n + p) : by rw add_assoc

Доказав всего три леммы, мы можем автоматически доказывать утверждения вроде следующего:

example (a b c d e : nah) : (((a + b) + c) + d) + e = (c + ((b + e) + a)) + d :=
by simp [add_assoc, add_comm, add_left_comm]

Умножение

Как и сложение, умножение определим рекурсивно:

def mul : nah → nah → nah
| n 0 := 0
| n (suc k) := mul n k + n

instance : has_mul nah := ⟨mul⟩

И сразу же докажем несколько лемм:

lemma mul_zero {n : nah}  : n * 0 = 0             := by refl
lemma mul_suc {n k : nah} : n * k.suc = n * k + n := by refl
lemma mul_one {n : nah}   : n * 1 = n             :=
by { unfold has_one.one, rw [mul_suc, add_comm], refl }

lemma zero_mul {n : nah} : 0 * n = 0 :=
sorry

lemma suc_mul {n k : nah} : n.suc * k = n * k + k :=
sorry

lemma one_mul {n : nah} : 1 * n = n :=
begin
  unfold has_one.one, rw [suc_mul],
  show 0 * n + n = n, rw [zero_mul, zero_add],
end

Упражнение: доказать zero_mul и suc_mul.

Замечание: suc_mul доказывается сложнее, чем леммы, что мы видели ранее. Однако, используя calc и simp, доказательство второй цели можно записать в четыре строчки. Заклинание simp [add_assoc, add_comm, add_left_comm, add_suc] позволяет не возиться со свойствами сложения.

В mul_one мы прямо сталкиваемся с тем, что для тактики rw 1 это не то же самое, что и zero.suc. Поэтому мы применяем тактику unfold, чтобы развернуть определение 1. Аналогично мы действуем в one_mul, но там мы кроме того используем show, чтобы превратить zero * n + n = n в 0 * n + n = n.

Теперь докажем дистрибутивность и леммы, аналогичные леммам для сложения:

lemma mul_left_distr {n k p : nah} : n * (k + p) = n * k + n * p :=
sorry

lemma mul_assoc {n k p : nah} : (n * k) * p = n * (k * p) :=
sorry

lemma mul_comm {n k : nah} : n * k = k * n :=
sorry

lemma mul_left_comm {n k p : nah} : n * (k * p) = k * (n * p) :=
sorry

lemma mul_right_distr {n k p : nah} : (n + k) * p = n * p + k * p :=
by simp [mul_comm, mul_left_distr]

Упражнение: доказать леммы.

Замечание: эти леммы не независимы: порядок доказательства важен.

Как и в случае сложения, эти леммы позволяют доказывать вещи вроде

example (a b c d e : nah) : (((a * b) * c) * d) * e = (c * ((b * e) * a)) * d :=
by simp [mul_assoc, mul_comm, mul_left_comm]

Больше сложения и умножения

Нам потребуются следующие леммы:

lemma suc_inj {n k : nah} (eq : n.suc = k.suc) : n = k := by { cases eq, refl }
lemma suc_ne_zero {n : nah} : n.suc ≠ 0 := (λ e, by cases e)
lemma zero_ne_suc {n : nah} : 0 ≠ n.suc := (λ e, by cases e)

a ≠ b это синоним a = b → false.

Lean знает, что индуктивные типы свободно порождены своими конструкторами, и n.suc = k.suc может быть истинно только в том случае, когда истино n = k. Аналогично, Lean знает, что n.suc не может быть равен нулю.

Теперь докажем следующие леммы:

lemma suc_ne {n : nah} : n.suc ≠ n :=
sorry

lemma add_right_cancel {n k p : nah} (eq : n + p = k + p) : n = k :=
sorry

lemma add_left_cancel {n k p : nah} (eq : p + n = p + k) : n = k :=
begin
  rw [@add_comm p n, @add_comm p k] at eq,
  from add_right_cancel eq
end

lemma add_eq_zero_left {n k: nah} (eq: n + k = 0) : n = 0 :=
begin
  cases k,
  from eq,
  from false.elim (suc_ne_zero eq)
end

lemma add_eq_zero_right {n k: nah} (eq: n + k = 0) : k = 0 :=
sorry

Упражнение: доказать леммы

rw ... at assum позволяет применить rw к предположению. cases это более слабый аналог induction, не вводящий индуктивных предположений.

В Lean есть дополнительные тактики, которые действуют как применение правил вывода:

• left как apply or.inl
• right как apply or.inr
• split как apply and.intro или apply iff.intro
• exfalso как apply false.elim

Кроме того, вместо have ..., from ..., можно писать просто have ... := ...,. А запись foo ; bar, позволяет применить тактику bar ко всем целям, порождённым тактикой foo.

Применяя всё вместе, докажем:

lemma mul_eq_zero {n k : nah} (eq : n * k = 0) : n = 0 ∨ k = 0 :=
begin
  cases n ; cases k,
  show zero  = 0 ∨ zero  = 0, left,  refl,
  show zero  = 0 ∨ k.suc = 0, left,  refl,
  show n.suc = 0 ∨ zero  = 0, right, refl,
  exfalso, {
    have nsz: n.suc = 0 := add_eq_zero_right eq,
    from suc_ne_zero nsz,
  }
end

Наконец, мы готовы разобрать доказательство, которое значительно сложнее всего того, что мы видели ранее:

lemma mul_left_cancel {n k p : nah} (pn : n ≠ 0) (eq : n * k = n * p) : k = p :=
begin
  induction p with p ih generalizing k,
  show k = 0, {
    cases mul_eq_zero eq with nz kz,
    from false.elim (pn nz),
    from kz
  },
  show k = p.suc, {
    cases k,
    exfalso, {
      have npz: n * p = 0 := add_eq_zero_left eq.symm,

      cases mul_eq_zero npz with nz pz,
      from pn nz,
      {
        have nz: n * 0 = n * 1, { rw pz at eq, from eq },
        rw mul_one at nz,
        from pn nz.symm,
      }
    },
    show k.suc = p.suc, {
      have nknp: n * k = n * p := @add_right_cancel _ _ n eq,
      have kp: k = p := ih nknp,
      from congr_arg (λ x, x.suc) kp
    },
  }
end

Здесь много тонкостей. В первую очередь, мы применяем индукцию с обобщением по k. Это значительно усиливает индуктивную гипотезу: если без обобщения контекст второй цели содержит ih: n * k = n * p → k = p, то с обобщением он содержит ih: ∀ {k : nah}, n * k = n * p → k = p вместе с k: nah.

Далее, во второй цели мы делаем cases k. Случай, когда k = 0 невозможен, и мы применяем exfalso, чтобы затем доказать false.

В выражении @add_right_cancel _ _ n eq, подчёркивания это значения, которые Lean выводит автоматически.

Наконец, congr_arg это функция с сигнатурой ∀f : A → B, a = b → f a = f b. Она позволяет получить k.suc = p.suc из k = p.

Неравенства

Определим n ≤ k:

inductive less_or_eq (n : nah) : nah → Prop
| refl : less_or_eq n
| step : (∀{k}, less_or_eq k → less_or_eq k.suc)

instance : has_le nah := ⟨less_or_eq⟩

Это индуктивно определённый предикат со следующими конструкторами:

less_or_eq.refl : ∀{n}, less_or_eq n n
less_or_eq.step : ∀{n k}, less_or_eq n k → less_or_eq n k.suc

Теперь леммы:

lemma leq_suc {n k : nah} (q : n ≤ k) : n ≤ k.suc := sorry

lemma zero_leq {n : nah} : 0 ≤ n :=
sorry

lemma suc_leq {n k : nah} (le : n.suc ≤ k) : n ≤ k :=
begin
  induction le with k prev next,
  show n ≤ n.suc, from leq_suc less_or_eq.refl,
  show n ≤ k.suc, from leq_suc next
end

lemma leq_zero {n : nah} (le: n ≤ 0) : n = 0 :=
begin
  cases n,
  show zero = 0, refl,
  exfalso, { cases le },
end

Упражнение доказать.

С индуктивным определением не всегда удобно работать, поэтому докажем следующие леммы:

lemma leq_exists {n k : nah} (le : n ≤ k) : ∃p, n + p = k :=
sorry

lemma exists_leq {n k : nah} (ex : ∃p, n + p = k) : n ≤ k :=
sorry

Упражнение доказать леммы.

Замечание: в одной из лемм может быть полезна обобщённая индукция.

Тактика existsi y превращает цель ∃x, P x в P y:

example {n : nah} : n ≤ n.suc :=
begin
  apply exists_leq,
  existsi (1 : nah),
  refl
end

Теперь докажем следующие леммы:

lemma suc_leq_suc {n k : nah} : n ≤ k ↔ n.suc ≤ k.suc :=
sorry

lemma right_add_leq_add {n k p : nah} : n ≤ k ↔ n + p ≤ k + p :=
sorry

Упражнение: доказать.

Замечение: suc_le_suc.1 использует лемму слева направо, а suc_le_suc.2, соответственно, справа налево.

Наконец, туториал завершает доказательства основных свойств неравенства:

lemma leq_trans {n k p : nah} (nk : n ≤ k) (kp: k ≤ p) : n ≤ p :=
sorry

lemma leq_antisym {n k : nah} (nk: n ≤ k) (kn : k ≤ n) : n = k :=
sorry

lemma leq_total (n k : nah) : n ≤ k ∨ k ≤ n :=
sorry

Упражнение: доказать.

Замечение: не следует забывать про обобщённую индукцию.

Ссылки

• The Natural Number Game, основной источник идей для этого туториала
• Курс Automated Reasoning
• Logic and Proof

Ну и, конечно же, документация к Isabelle/HOL и Lean.

Формальное доказательство это

Есть же формальное определение формального доказательства. 🙂 Кроме того, забыли про аксиомы, а это может сильно пригодиться в дальнейшем.

Синтаксис:

Сами пропозициональные переменные забыли! 😃 Сходу не очевидно, что можно использовать произвольные идентификаторы вместо P и Q.

Первое правило говорит о том, что если предположив P можно доказать Q, то из P следует Q. Второе, с латинским названием modus pones, говорит, что если из P следует Q и P истино, то и Q должно быть истино.

Ох, ё... Вы же здесь с ходу смешали в кучу выводимость и истинность, не объяснив ни что такое первое, ни второе. Может, не надо так?

Ещё интереснее правила для отрицания:

notE никак не прокомментировали.

Lean использует совсем другое основание: зависимые типы

Но ведь зав. типы эквивалентны (интуиционистской) логике высшего порядка, а лямбда-термы кодируют (изоморфны) деревьям естественного вывода! 😄

соответствие Карри-Ховарда

Карри-Говарда... 😒

iff.mpr : (P ↔ Q) → ?M_2 → P

Что, прям так и без пояснений? 😃

Пруф-ассистенты, строго говоря. "Пруверы" обычно подразумеваются автоматические (ATP) — Z3, Vampire, вот это всё.

«Интерактивный прувер» — норм?

Есть же формальное определение формального доказательства. Кроме того, забыли про аксиомы, а это может сильно пригодиться в дальнейшем.

Ох, ё... Вы же здесь с ходу смешали в кучу выводимость и истинность, не объяснив ни что такое первое, ни второе. Может, не надо так?

Тут есть проблема: сколь-либо полноценный обзор логики вываливается далеко за пределы этого текста. И под истинностью понимается именно выводимость.

Но я попробую сформулировать иначе, и заодно упомянуть аксиомы.

Но ведь зав. типы эквивалентны (интуиционистской) логике высшего порядка, а лямбда-термы кодируют (изоморфны) деревьям естественного вывода!

Да, но машинерия другая. Никаких тебе proof objects в Isabelle, и стрелок целых две.

Тут есть проблема: сколь-либо полноценный обзор логики вываливается далеко за пределы этого текста.

Согласен. Поэтому предлагаю интерпретации и, соответственно, истинность вообще не упоминать, ограничившисть только выводимостью.

Никаких тебе proof objects в Isabelle, и стрелок целых две.

На самом деле, proof objects в Isabelle, конечно, есть. И стрелок существенно больше... 😄

Переменные: P, Q, R

Я бы добавил как минимум Sunny чтобы не было большого сюрприза потом.

Ну и обычное нытьё, что правила вывода и правила формирования синтаксиса используют _мета_переменные...

если из P следует Q, и того, что P истино, вывести Q.
P истино

Опечатка, должно быть "истинно".

Хотя я бы по-прежнему настаивал на том чтобы вообще выпилить упоминание "истинности" и оставить только "выводимость". 🙂

Может быть и стоит выпилить, но я не знаю как сформулировать текст так, чтобы читалось легко и естественно.

Так что пока будет так. Опечатку поправю.

@suhr я поправил несколько опечаток в форке: https://gist.github.com/gabriel-fallen/14772db4315375a9f6f309a9b3e2043f
Но не вижу как сделать PR.

Предикаты и кванторы в Lean

Синтаксис:

∀x, P x
∃x, P x

А следом идёт формат ∀x : A, P x — может, лучше сразу дать с типами, и дописать, что типы часто можно не указывать, потому что Lean сам догадывается во многих случаях по контексту?

Спасибо, обновил гист. Вообще, наверное стоит всё-таки перенести текст в отдельный репозиторий.

@suhr в копилку. Видел забавную простенькую задачку из какого-то тьюториала:

theorem andb_true_elim2 (a b : bool) : a && b = true -> b = true := sorry

Правда, в текущий набор задач она "не лезет", потому что там нет про булы и их разницу с Prop. Вероятно, про это стоит написать, иначе у большинства возникнет сильное недоумение в какой-то момент. 🙂

Этим каким-то туториалом был Software Foundations. Да, и булевы значения в Lean пишутся как ff и tt.

Principia Mathematica Рассела

Так-то она Рассела и Уайтхеда. 😉

@suhr

n.suc = k.suc может быть истино только в том случае, когда истино n = n

n = k 🙂

Хорошо бы пояснить, чем

inductive less_or_eq (n : nah) : nah → Prop

отличается от
inductive less_or_eq : (n : nah) → nah → Prop