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> : "→"

Например, ∃ вводится нажатием клавиши 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 pones, позволяет из того, что если из 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 pones это просто применение функции, когда же введение предположения это лямбда-абстракция.

Смотря шире, 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, P x
• ∃x, 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))

Арифметика