Lean#

Lean это система интерактивного доказательства теорем, основанная на исчислении индуктивных построений. Она станет нашим основным инструментом.

Установка#

Для работы с Lean нам потребуется система управления версиями Git и редактор исходного кода Visual Studio Code.

Переходим по ссылкам и скачиваем оба приложения, после чего устанавливаем сначала Git, а затем Visual Studio Code. Открываем Visual Studio Code. На панели слева щёлкаем по иконке с четырьмя квадратами — откроется панель расширений. Вводим lean4 в строку поиска и устанавливаем расширение.

Нам осталось лишь открыть проект. Используем Git, чтобы скачать и открыть заготовленный проект. Для этого нажимаем клавишу F1 и в появившейся строке поиска вводим git clone и нажимаем Enter. Visual Studio Code попросит URL репозитория, вставляем в поле ввода https://github.com/suhr/polygon.git и снова нажимаем Enter. Выбираем директорию, в которую будет скачана директория с проектом.

На панели слева выбираем иконку с двумя листами бумаги. Откроется панель файлов. Щёлкаем по файлу Basics.lean чтобы открыть его.

Основы Lean#

Начнём с синтаксиса примеров и определений.

Определение name как значения expr типа type записывается в Lean следующим образом:

def name: type := expr

Когда определение представляет собой доказательство некоторого высказывания, вместо слова def принято писать слово theorem:

theorem name: type := expr

Декларация, что выражение expr является примером значения типа type, записывается как

example: type := expr

Выражение expr может быть перенесено на следующую строку, а также может быть разбито на несколько строк. В таком случае каждая строка выражения должна начинаться с отступа. Отступ вводится с помощью клавиши Tab.

Рассмотрим теперь синтаксис выражений в Lean:

Лямбда-абстракция \(λx:τ.\; e\) записывается в Lean как λx:τ => e или как fun x: τ => e. Вместо λx:α => λy:β => e можно просто писать λ(x:α)(y:β) => e
Применение \(e_1\ e_2\) записывается как e1 e2. Важно: применение в выражении всегда пишется через пробел. Запись вроде f(x) или (f a)b синтаксически некорректна
Тип функций \(∀x:σ.\; τ\) записывается как ∀x:σ, τ. Можно также писать (x:σ) → τ
Запись let x := v; e означает выражение e, в котором x определено как v. Точку с запятой можно опустить, если e начинается с новой строки
(e : τ) представляет собой выражение e вместе с явным указанием того, что оно имеет тип τ

Lean широко использует символы Unicode, отсутствующие на стандартной клавиатуре. Расширение Lean в Visual Studio Code предоставляет метод ввода математических символов.

Ввод символа начинается с ввода обратной косой черты, после которой следует имя символа. Если введённое имя однозначно определяет требуемый символ и не является префиксом имени какого-то другого символа, метод ввода немедленно заменяет введённое имя на требуемый символ. В противном случае, ввод символа можно завершить, нажав клавишу Tab или пробел.

Имена греческих букв совпадает с их именами на английском языке. Так, например, \lambda вводит λ, а \sigma и \tau вводят σ и τ. Если первая буква имени является заглавной, то и вводимая буква тоже будет заглавной. Например, \Gamma превращается в Γ.

Символы → (стрелка), ∧ (конъюнкция), ∨ (дизъюнкция) и ¬ (отрицание) вводятся, соответственно, как \to, \and, \or и \not. Кванторы всеобщности и существования записываются как \forall и \exists.

Вселенные типов в Lean называются сортами, и записываются как Sort 0, Sort 1 и так далее. Вселенная Sort 0 является вселенной высказываний, и потому обозначается как Prop. Вселенные типов Sort 1, Sort 2 и так далее обозначаются также как Type 0, Type 1 и так далее. Вместо Type 0 можно писать просто Type.

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

\[(λα\,β:\mathcal U_1.\; λx:α.\; λy:β.\; x) : ∀α\,β: \mathcal U_1.\; (x:α) → (y:β) → α\]

В Lean этот пример примет следующий вид:

example: ∀α β: Type, α → β → α :=
  λ(α β: Type)(x:α)(y:β) => x

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

example (α β: Type)(x:α)(y:β): α := x

Сокращённую запись можно воспринимать следующим образом: пример является функцией, которая, будучи применена к α и β типа Type, x типа α и y типа β, становится выражением x типа α.

Превратим теперь наш пример в определение:

def f1 (α β: Type)(x:α)(_:β): α := x

Подчёркивание вместо имени связывающей переменной означает, что связываемое значение не используется в определении.

Lean это интерактивное средство доказательства теорем. Панель Lean Infoview в правой половине экрана показывает различную полезную информацию. Одной из вещей, которую показывает эта панель, является контекст и ожидаемый тип в том месте, куда установлен курсор редактора.

Поставим курсор непосредственно перед выражением x в определении f1. Lean Infoview покажет следующую информацию:

α β : Type
x : α
x✝ : β
⊢ α

Список до символа турникета представляет собой контекст выражения, а тип после турникета является ожидаемым типом выражения.

С Lean можно взаимодействовать посредством команд, которые вводятся прямо в редактор. Рассмотрим некоторые из этих команд.

Команда #check проверяет, что выражение корректно типизированно, и выводит его тип. Поставив курсор на #check f1 Nat Nat 3 5 можно узнать, что это выражение имеет тип Nat.

Команда #reduce редуцирует выражение. Поставив курсор на #reduce f1 Nat Nat 3 5, можно узнать, что результатом вычисления выражения является число 3.

И, наконец, команда #print печатает определение той или иной сущности. Например, #print f1 показывает полное определение этой функции.

Lean умеет сам выводить некоторые значения, в первую очередь типы. Чтобы попросить Lean вывести требуемое значение, достаточно написать символ подчёркивания на месте выводимого выражения. Например, следующим образом можно попросить Lean вывести типы, к которым применяется функция f1:

#check f1 _ _ 3 5

Подчёркивания в выражении называются дырками. Здесь Lean выводит, что требуемыми значениями на месте дырок является тип натуральных чисел Nat.

В лямбда-абстракции, тип при связывающей переменной можно просто опустить. Например, вместо λP: Prop => ¬P или λP: _ => ¬P можно писать просто λP => ¬P.

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

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

def f2 {α β: Type}(x:α)(_:β): α := x

В отличие от функции f1, функция f2 не требует перечисления типов в применении:

#check f2 3 5

При необходимости, неявные аргументы можно указать. Если в выражении перед именем функции стоит символ @, то тогда функция используется так же, как и функция, у которой все аргументы явные:

#check @f2 Nat Nat 3 5

Есть и другой способ указать явный аргумент — по имени:

#check f2 (β := Nat) 3 5

Lean позволяет обобщить определение или пример для всех вселенных типов. Например:

example {α β: Sort u}(x:α)(_:β): α := x

Кроме того, в примере выше {α β: Sort u} можно опустить:

example (x:α)(_:β): α := x

В этом случае, Lean сам обобщает пример для всех вселенных типов наиболее общим образом.

Рассмотрим теперь возможности Lean связанные с индуктивными типами.

Особой разновидностью индуктивных типов в Lean являются так называемые структуры. С точки зрения ядра Lean структуры являются индуктивными типами с единственным конструктором. Для пользователя, однако, Lean предоставляет дополнительные способы взаимодействия с ними.

Примером типа структуры является тип Prod, определённый следующим образом:

structure Prod (α : Type u) (β : Type v) where
  fst : α
  snd : β

Тип Prod α β представляет тип пар значений, где первое значение в паре имеет тип α, а второе значение имеет тип β. Тип пар также называют произведение типов α и β и обозначают как α × β (символ × вводится как \times).

Определение вводит индуктивный тип Prod с конструктором Prod.mk типа α → β → Prod α β. Кроме того, Lean определяет функции Prod.fst типа Prod α β → α и Prod.snd типа Prod α β → β, называемые проекциями структуры.

Вместе с типом, Lean также вводит одноимённое пространство имён. Точка предоставляет доступ к имени в пространстве имён, так, например, запись Prod.mk означает функцию mk в пространстве имён Prod.

Результатом применения Prod.fst и Prod.snd к значению типа Prod α β является, соответственно, левое и правое значение в паре. Например, результатом применения Prod.fst к Prod.mk 3 5 является число 3, когда же результатом применения Prod.snd является число 5.

Если e это значение типа T, а f это некоторая функция, определённая в пространстве имён T, то тогда e.f означает то же самое, что и T.f e. Например, (Prod.mk 3 5).fst это то же самое выражение, что и Prod.fst (Prod.mk 3 5).

Структуру можно построить, указав значение для каждой из её проекций:

#check ({fst := 3, snd := 5} : Nat × Nat)

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

#check (⟨3, 5⟩ : Nat × Nat)

Угловые скобки вводятся как \langle и \rangle.

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

#reduce
  let (Prod.mk f s) := Prod.mk 3 5
  f

В этом выражении, let определяет такие f и s, что Prod.mk f s это в точности то же значение, что и Prod.mk 3 5. Синтаксическое выражение слева от := называется образцом.

Нотацию для структур и перечисление в угловых скобках можно также использовать в качестве образца:

#reduce
  let {fst := f, snd := _} := Prod.mk 3 5
  f

#reduce
  let ⟨f,_⟩ := Prod.mk 3 5
  f

Упражнения#

Время упражнений! Будем доказывать простые логические тождества.

Конъюнкция, дизъюнкция, абсурд и квантор существования определены в Lean как индуктивные типы. Мы не будем разбирать их определения, всё, что нам нужно знать, это типы следующих функций:

And.intro : ∀{a b: Prop}, a → b → a ∧ b
And.left  : ∀{a b: Prop}, a ∧ b → a
And.right : ∀{a b: Prop}, a ∧ b → b

Or.inl  : ∀{a b: Prop}, a → a ∨ b
Or.inr  : ∀{a b: Prop}, b → a ∨ b
Or.elim : ∀{a b c: Prop}, a ∨ b → (a → c) → (b → c) → c

False.elim : ∀{C: Sort u}, False → C

Exists.intro : ∀{α: Sort u}{P: α → Prop},
  (x:α) → P x → Exists P
Exists.elim : ∀{α: Sort u}{P: α → Prop}{β : Prop},
  (∃x, P x) → (∀x:α, P x → β) → β

Эти функции выражают соответствующие правила введения и удаления связок и квантора всеобщности. Высказывание ¬P определено в Lean как P → False.

Рассмотрим теперь процесс доказательства высказываний на примерах.

Для начала, докажем, что если P ∨ Q, и если ¬P, то тогда Q. Начнём доказательство с записи соответствующего примера с дыркой на месте будущего свидетельства:

example {P Q: Prop}(pq: P ∨ Q)(np: ¬P): Q :=
  _

Lean не может придумать доказательство, требуемое на месте дырки. Но зато он может показать ожидаемый тип дырки и её контекст. Достаточно поставить курсор непосредственно перед дыркой, и Lean покажет следующее:

don't know how to synthesize placeholder
context:
pq : P ∨ Q
np : ¬P
⊢ Q

Нам необходимо построить значение типа Q. Чтобы решить эту задачу, можно использовать перечисленные в контексте значения. Использовать np типа ¬P мы пока что не можем, так как для этого требуется значение типа P, которого у нас нет. Но мы можем использовать pq, применив к нему функцию Or.elim:

example {P Q: Prop}(pq: P ∨ Q)(np: ¬P): Q :=
  pq.elim _ _

Lean Infoview позволяет узнать контекст как первой дырки:

pq : P ∨ Q
np : ¬P
⊢ P → Q

Так и второй:

pq : P ∨ Q
np : ¬P
⊢ Q → Q

Значением типа Q → Q является, очевидно, функция λq => q. Это позволяет немедленно закрыть вторую дырку:

example {P Q: Prop}(pq: P ∨ Q)(np: ¬P): Q :=
  pq.elim _ (λq => q)

Доказательством высказывания P → Q является лямбда-абстракция, предполагающая P:

example {P Q: Prop}(pq: P ∨ Q)(np: ¬P): Q :=
  pq.elim (λp => _) (λq => q)

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

pq : P ∨ Q
np : ¬P
p : P
⊢ Q

Теперь мы можем использовать np чтобы доказать Q. Для этого применим np к p, чтобы получить абсурд, и затем используем False.elim чтобы получить из абсурда свидетельство Q:

example {P Q: Prop}(pq: P ∨ Q)(np: ¬P): Q :=
  pq.elim (λp => False.elim (np p)) (λq => q)

Закрытие всех дырок завершает доказательство.

Важно уметь сопоставить выражение с рассуждением по шагам. Построенному доказательству соответствует следующее рассуждение:

Пусть \(P ∨ Q\), и пусть \(¬P\)
1. Рассмотрим \(P ∨ Q\)
  1. Пусть \(P\)
    1. Но это невозможно, так как \(¬P\)
  2. Пусть \(Q\)
    1. Тогда \(Q\)
Следовательно, \((P ∨ Q) → ¬P → Q\)

Рассмотрим теперь другой пример. Докажем, что из \(P ∧ (Q ∨ R)\) следует \((P ∧ Q) ∨ (P ∧ R)\). Начинаем, как и раньше, с дырки:

example {P Q R: Prop}(pqr: P ∧ (Q ∨ R)): (P ∧ Q) ∨ (P ∧ R) :=
  _

У нас есть свидетельство истинности \(P ∧ (Q ∨ R)\), и естественно разобрать его на свидетельство \(P\) и свидетельство \(Q ∨ R\). Для этого можно использовать функции And.left и And.right. Но And это индуктивный тип с единственным конструктором, что позволяет разобрать значение с помощью сопоставления с образцом:

example {P Q R: Prop}(pqr: P ∧ (Q ∨ R)): (P ∧ Q) ∨ (P ∧ R) :=
  let ⟨p,qr⟩ := pqr
  _

Контекст дырки при этом принимает вид:

pqr : P ∧ (Q ∨ R)
p : P
qr : Q ∨ R
⊢ P ∧ Q ∨ P ∧ R

Как и в прошлом примере, единственное что мы можем сделать это применить Or.elim. Сделаем это, заодно введя соответствующие лямбда-абстракции:

example {P Q R: Prop}(pqr: P ∧ (Q ∨ R)): (P ∧ Q) ∨ (P ∧ R) :=
  let ⟨p,qr⟩ := pqr;
  qr.elim (λq => _) (λr => _)

Контекст первой дырки выглядит следующим образом:

pqr : P ∧ (Q ∨ R)
p : P
qr : Q ∨ R
q : Q
⊢ P ∧ Q ∨ P ∧ R

Значение типа (P ∧ Q) ∨ (P ∧ R) можно построить либо из значения P ∧ Q, либо из значения P ∧ R. Выбираем первое, применив Or.inl:

example {P Q R: Prop}(pqr: P ∧ (Q ∨ R)): (P ∧ Q) ∨ (P ∧ R) :=
  let ⟨p,qr⟩ := pqr;
  qr.elim (λq => Or.inl _) (λr => _)

Новая цель, новый контекст:

pqr : P ∧ (Q ∨ R)
p : P
qr : Q ∨ R
q : Q
⊢ P ∧ Q

Значение типа P ∧ Q можно построить с помощью конструктора And.intro, но мы воспользуемся угловыми скобками:

example {P Q R: Prop}(pqr: P ∧ (Q ∨ R)): (P ∧ Q) ∨ (P ∧ R) :=
  let ⟨p,qr⟩ := pqr;
  qr.elim (λq => Or.inl ⟨p,q⟩) (λr => _)

Оставшееся дырка закрывается схожим образом:

example {P Q R: Prop}(pqr: P ∧ (Q ∨ R)): (P ∧ Q) ∨ (P ∧ R) :=
  let ⟨p,qr⟩ := pqr;
  qr.elim (λq => Or.inl ⟨p,q⟩) (λr => Or.inr ⟨p,r⟩)

Доказательству выше соответствует следующее рассуждение:

Пусть \(P ∧ (Q ∨ R)\)
1. Тогда \(P\)
2. И \(Q ∨ R\)
3. Рассмотрим \(Q ∨ R\)
  1. Пусть \(Q\)
    1. Тогда \(P ∧ Q\)
    2. И, следовательно, \((P ∧ Q) ∨ (P ∧ R)\)
  2. Пусть \(R\).
    1. Тогда \(P ∧ R\)
    2. И отсюда \((P ∧ Q) ∨ (P ∧ R)\)
Следовательно, \(P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)\)

Теперь посмотрим, как доказываются высказывания с кванторами. Докажем, что из \(∀x.\; P\ x ∧ Q\ x\) следует \((∀x.\; P\ x) ∧ (∀x.\; Q\ x)\):

example {P Q: α → Prop}(apq: ∀x, P x ∧ Q x): (∀x, P x) ∧ (∀x, Q x) :=
  _

Конъюнкцию можно построить с помощью угловых скобок:

example {P Q: α → Prop}(apq: ∀x, P x ∧ Q x): (∀x, P x) ∧ (∀x, Q x) :=
  ⟨_, _⟩

Посмотрим на контекст первой дырки:

P Q : α → Prop
apq : ∀ (x : α), P x ∧ Q x
⊢ ∀ (x : α), P x

Пусть x это значение типа α:

example {P Q: α → Prop}(apq: ∀x, P x ∧ Q x): (∀x, P x) ∧ (∀x, Q x) :=
  ⟨λx => _, _⟩

Контекст новой дырки:

P Q : α → Prop
apq : ∀ (x : α), P x ∧ Q x
x : α
⊢ P x

Применение apq к x даёт значение типа P x ∧ Q x, из которого свидетельство P x можно достать, применив проекцию:

example {P Q: α → Prop}(apq: ∀x, P x ∧ Q x): (∀x, P x) ∧ (∀x, Q x) :=
  ⟨λx => (apq x).left, _⟩

Аналогично закрывается последняя дырка:

example {P Q: α → Prop}(apq: ∀x, P x ∧ Q x): (∀x, P x) ∧ (∀x, Q x) :=
  ⟨λx => (apq x).left, λx => (apq x).right⟩

Рассуждение:

Пусть \(∀x.\; P\ x ∧ Q\ x\)
1. Пусть \(x:α\)
  1. Тогда \(P\ x ∧ Q\ x\)
  2. И отсюда \(P\ x\)
2. Следовательно, \(∀x.\; P\ x\)
3. Пусть \(x:α\)
  1. Тогда \(P\ x ∧ Q\ x\)
  2. И отсюда \(Q\ x\)
4. Следовательно, \(∀x.\; Q\ x\)
5. Отсюда \((∀x.\; P\ x) ∧ (∀x.\; Q\ x)\)
Следовательно, \((∀x.\; P\ x ∧ Q\ x) → (∀x.\; P\ x) ∧ (∀x.\; Q\ x)\)

Последний пример показывает, как доказываются высказывания с квантором существования. Докажем, что если ∃x, ∀y, P x y, то тогда ∀y, ∃x, P x y:

example {P: α → β → Prop}(eap: ∃x, ∀y, P x y): ∀y, ∃x, P x y :=
  _

Начнём доказательство с того, что разберём eap на части и предположим y:

example {P: α → β → Prop}(eap: ∃x, ∀y, P x y): ∀y, ∃x, P x y :=
  let ⟨x,ap⟩ := eap
  λy => _

Контекст дырки:

P : α → β → Prop
eap : ∃ x, ∀ (y : β), P x y
x : α
ap : ∀ (y : β), P x y
y : β
⊢ ∃ x, P x y

Чтобы доказать ∃x, P x y, нужно предоставить некоторое значение x вместе с доказательством P x y. Имена переменных предлагают взять x в качестве такого x:

example {P: α → β → Prop}(eap: ∃x, ∀y, P x y): ∀y, ∃x, P x y :=
  let ⟨x,ap⟩ := eap
  λy => ⟨x, _⟩

Осталось лишь доказать P x y. Для этого достаточно применить ap к y:

example {P: α → β → Prop}(eap: ∃x, ∀y, P x y): ∀y, ∃x, P x y :=
  let ⟨x,ap⟩ := eap
  λy => ⟨x, ap y⟩

Это завершает доказательство последнего из примеров.

Упражнения на связки и кванторы, которые читателю предстоит решить, находятся в файле Basics.lean. Решение этих упражнений сводится к замене заглушки sorry на корректное доказательство соответствующего высказывания.

Для решения этих упражнений не обязательно использовать продвинутые возможности Lean вроде сопоставления с образцом. Каждое из высказываний можно доказать, используя лишь типизированные лямбда-выражения и определённые для связок и квантора существования функции.

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

Особняком стоят упражнения на классическую логику. Их решать не обязательно (хотя ознакомиться с ними всё же полезно). Мы ближе познакомимся с классической логикой в будущем, когда будем рассматривать аксиому выбора.

Равенство#

Равенство в Lean определено как индуктивное семейство типов Eq. Оставим в очередной раз на потом обзор индуктивных семейств, и рассмотрим равенство с точки зрения его свойств.

Два ключевых свойства равенства

Любое значение равно самому себе
Равные значения взаимозаменяемы

Первое свойство называется рефлексивностью, и в Lean его выражает функция Eq.refl:

Eq.refl: {α: Sort u} → (a: α) → a = a

Эта функция также называется rfl.

Если значения взаимозаменяемы, то любое свойство, что верно для одного значения, верно и для другого. Функция Eq.subst утверждает в точности это:

Eq.subst: {α: Sort u} → {motive: α → Prop} → {a b: α} →
  (eq: a = b) → (m: motive a) → motive b

Функция Eq.ndrec обобщает эту идею за пределы Prop:

Eq.ndrec: {α: Sort u} → {a: α} → {motive: α → Sort v} →
  (m: motive a) → {b: α} → (eq: a = b) → motive b

Иной порядок аргументов у Eq.ndrec по сравнению с Eq.subst связан с тем, что Eq.ndrec представляет собой упрощённую версию рекурсора индуктивного семейства Eq.

Докажем теперь несколько свойств равенства. Для начала докажем симметричность: если x = y, то и y = x.

example {x y: α}(e: x = y): y = x :=
  e.subst (motive := λt => t = x) (rfl: x = x)

Доказательство работает следующим образом: поскольку равенство рефлексивно, x удовлетворяет свойству λt => t = x. Но x = y, и потому y должно удовлетворять тому же свойству.

Lean позволяет записать это доказательство короче:

example {x y: α}(e: x = y): y = x :=
  e ▸ (rfl: x = x)

Но в целях наглядности, мы пока будем использовать Eq.subst, явно указывая мотив.

Транзитивность равенства означает, что если x = y и y = z, то тогда x = y. Она доказывается почти так же, как и симметричность:

example {x y z: α}(xy: x = y)(yz: y = z): x = z :=
  yz.subst (motive := λt => x = t) (xy: x = y)

Применение функции сохраняет равенство: если x = y, то f x = f y. И снова то же самое доказательство, только с другим мотивом:

example {x y: α}{f: α → β}(e: x = y): f x = f y :=
  e.subst (motive := λt => f x = f t) (rfl: f x = f x)

Симметричность, транзитивность и применение функции к обеим частям равенства уже определены в Lean как Eq.symm, Eq.trans и Eq.congrArg.

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

В качестве таких значений возьмём значения false и true типа Bool. Этот индуктивный тип определён в Lean следующим образом:

inductive Bool : Type where
| false : Bool
| true : Bool

Рекурсором Bool является функция Bool.rec:

Bool.rec: {motive: Bool → Sort u} →
  motive false → motive true →
  (t: Bool) → motive t

Вместе с рекурсором, Lean также определяет различные полезные функции. Одной из них является функция Bool.casesOn, определенная следующим образом:

def Bool.casesOn {motive : Bool → Sort u} →
    (b: Bool) → motive false → motive true : motive t :=
  Bool.rec f t b

Наша задача состоит в том, чтобы доказать, что из false = true следует абсурд. Для этого рассмотрим следующее определение, также вводимое Lean вместе с индуктивным типом:

def Bool.noConfusionType (P: Sort u)(x:Bool)(y:Bool): Sort u :=
  x.casesOn (y.casesOn (P → P) P) (y.casesOn P (P → P))

Вычислим Bool.noConfusionType False a b для различных значений a и b:

#reduce Bool.noConfusionType False false false  -- False → False
#reduce Bool.noConfusionType False false true   -- False
#reduce Bool.noConfusionType False true false   -- False
#reduce Bool.noConfusionType False true true    -- False → False

Видно, что функция Bool.noConfusionType P, будучи применена к одним и тем же константам типа Bool, вычисляется в тип P → P, когда же применённая к различным константам, вычисляется в P.

Определим теперь функцию bool_d, которая для любого типа P и любого значения b типа Bool строит значение типа Bool.noConfusionType P b b. Начнём построение требуемого выражения с применения Bool.casesOn:

def bool_d {P: Sort u}(b: Bool): Bool.noConfusionType P b b :=
  b.casesOn _ _

Посмотрим на контекст левой дырки:

b : Bool
⊢ Bool.noConfusionType P false false

Тип дырки Bool.noConfusionType P false false вычислительно равен типу P → P, так что функция λp => p закрывает её:

def bool_d {P: Sort u}(b: Bool): Bool.noConfusionType P b b :=
  b.casesOn (λp => p) _

Правая дырка имеет тип Bool.noConfusionType P true true, и потому закрывается так же:

def bool_d {P: Sort u}(b: Bool): Bool.noConfusionType P b b :=
  b.casesOn (λp => p) (λp => p)

С помощью функции bool_d мы можем наконец доказать, что false не равно true:

example (h: false = true): False :=
  Eq.subst (motive := λt => Bool.noConfusionType _ false t) h (bool_d false)

Посмотрим внимательнее на это доказательство. Выражение bool_d false является значением типа Bool.noConfusionType False false false. Гипотетическое свидетельство равенства false и true позволяет преобразовать его в значение типа Bool.noConfusionType False false true. Но тип Bool.noConfusionType False false true вычислительно равен False, и потому построенное выражение является свидетельством абсурда.

Вместе с индуктивным типом Bool, Lean уже определил функцию Bool.noConfusion, обобщающую это доказательство:

Bool.noConfusion: {P : Sort u} → {a b : Bool} →
  (eq: a = b) → Bool.noConfusionType P a b

Так что значение произвольного типа P можно получить, просто применив Bool.noConfusion к гипотетическому свидетельству равенства false и true.

Мы можем различить два значения типа Bool только благодаря разбору во вселенную типов — отображению значения в тот или иной тип в зависимости от того, вычисляется ли оно в false или true.

Как мы говорили ранее, исчисление индуктивных построений не допускает подобный разбор для индуктивных типов в Prop. Таким образом нет никакой возможности различить два значения индуктивного типа в Prop. Нельзя, например, доказать, что Or.inl p ≠ Or.inr q.

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

И тут мы приходим к важному принципу: неразличимые значения неотличимы от равных.

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

Это позволяет доказать, к примеру, следующее:

example (P Q: Prop)(p: P)(q: Q): Or.inl p = Or.inr q :=
  rfl

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

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

А сейчас обратим внимание на следующее: нетривиальное равенство порождает различие между формой и смыслом. Возьмём для для примера знаменитое равенство:

\[0{,}(9) = 1\]

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

Lean

Contents

Lean#

Установка#

Основы Lean#

Упражнения#

Равенство#