Натуральные числа#

Большинство людей находят концепцию программирования очевидной, но само программирование невозможным. (Алан Перлис)

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

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

Основой любого высокого искусства является быт. Одной лишь идеи недостаточно, чтобы решить задачу, нужно ещё проделать действия, ведущие к её решению, сколь бы тривиальными они ни были. Чтобы решить сложную задачу, нужно уметь решать простые задачи. Для компьютерных доказательств эта необходимость ещё острее: нельзя в качестве решения просто сказать «очевидно», так у компьютера свои представления об очевидном, отличные от человеческих.

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

В этой главе читатель будет доказывать простые теоремы про арифметические операции на натуральных числах, вроде того, что \(a + b = b + a\) для любых \(a\) и \(b\). Хотя истинность подобных высказываний кажется очевидной, их доказательства не столь просты. Они не лишены содержания.

Все материалы этой главы, включая упражнения, находятся в файле Nat.lean в том же репозитории, который читатель клонировал в предыдущей главе. Читателю следует открыть Visual Studio Code, и там же открыть этот файл. Перед тем, как открывать файл, имеет смысл нажать F1 и ввести команду git pull, чтобы обновить репозиторий до последней версии.

Глава будет долгой и трудной, поэтому стоит вспомнить всё то, что было раньше. Для начала, полезно вспомнить правила типизации исчисления построений:

  • Вселенные:

\[\frac{}{Γ ⊢ \mathcal U_i : \mathcal U_{i + 1}}\]

  • Предположения:

\[\frac{Γ \vdash {\color{red}τ}:\mathcal U_i}{\Gamma,\, {\color{red}x}:{\color{red}τ} \vdash {\color{red}x}:{\color{red}τ}} \qquad \frac{\Gamma \vdash {\color{red}e}:{\color{red}τ} \qquad Γ \vdash {\color{red}σ}:\mathcal U_i} {\Gamma,\, {\color{red}x}:{\color{red}σ} \vdash {\color{red}e}:{\color{red}τ}}, \qquad {\color{red}x} \mathbin\# Γ\]

  • Тип зависимых функций:

\[\frac{ Γ ⊢ {\color{red}σ}: \mathcal U_i \qquad Γ,({\color{red}x}: {\color{red}σ}) ⊢ {\color{red}τ}: \mathcal U_j }{Γ ⊢ (∀{\color{red}x}:{\color{red}σ}.\; {\color{red}τ}): \mathcal U_k},\quad k = imax(i,j)\]

  • Абстракция:

\[\frac { Γ,({\color{red}x}:{\color{red}σ}) ⊢ {\color{red}e}:{\color{red}τ} \qquad Γ ⊢ (∀{\color{red}x}:{\color{red}σ}.\;{\color{red}τ}):\mathcal U_i } {Γ ⊢ (λ{\color{red}x}:{\color{red}σ}.\;{\color{red}e}): (∀{\color{red}x}:{\color{red}σ}.\;{\color{red}τ}) }\]

  • Применение:

\[\frac { Γ ⊢ {\color{red}f}:(∀{\color{red}x}:{\color{red}σ}.\;{\color{red}τ})\qquad Γ ⊢ {\color{red}v}:{\color{red}σ} } {Γ ⊢ ({\color{red} f\ v}): {\color{red}τ}[{\color{red}x} := {\color{red}v}]}\]

  • Вычислительное равенство:

\[\frac { Γ ⊢ \textcolor{red}e: \textcolor{red}σ\qquad \textcolor{red}σ \equiv \textcolor{red}τ\qquad Γ ⊢ \textcolor{red}τ: \mathcal U_i} {Γ ⊢ \textcolor{red}e:\textcolor{red}τ}\]

Если читатель не помнит смысл этих правил, ему следует перечитать главу «Исчисление построений».

В предыдущей главе мы работали со связками и квантором существования, используя заранее определённые функции. Посмотрим теперь, как эти типы и функции определены в Lean.

Конъюнкция представляет собой структуру:

structure And (a b: Prop): Prop where
  intro ::
  left: a
  right: b

Конструктором значений типа And a b является функция And.intro типа a → b → And a b, когда же функции And.left и And.right являются проекциями структуры.

Как и у любого другого индуктивного типа, у конъюнкции есть рекурсор:

And.rec.{u}: {a b: Prop} → {motive: a ∧ b → Sort u} →
  ((left: a) → (right: b) → motive ⟨left, right⟩) →
  (t: a ∧ b) → motive t

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

Дизъюнкция же определена следующим образом:

inductive Or (a b: Prop): Prop where
| inl (h: a): Or a b
| inr (h: b): Or a b

Это индуктивный тип с двумя конструкторами: Or.inl типа a → Or a b и Or.inr типа b → Or a b. Рекурсор же имеет тип

Or.rec: ∀{a b: Prop} {motive: a ∨ b → Prop},
  (∀h: a, motive (Or.inl h)) → (∀h: b, motive (Or.inr h)) →
  ∀t: a ∨ b, motive t

Функция Or.elim, которую мы ранее использовали, просто применяет рекурсор:

theorem Or.elim {c: Prop} (h: Or a b) (left: a → c) (right: b → c): c :=
  Or.rec left right h

Абсурд это индуктивный тип без конструкторов значений:

inductive False: Prop

Его рекурсор:

False.rec.{u}: (motive: False → Sort u) → (t: False) → motive t

Как и Or.elim, False.elim просто применяет рекурсор:

def False.elim {C: Sort u} (h: False): C :=
  h.rec

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

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

Его рекурсор:

Exists.rec.{u}: ∀ {α: Sort u} {p: α → Prop} {motive: Exists p → Prop},
  (∀(w: α)(h: p w), motive (Exists.intro w h)) →
  ∀t: Exists p, motive t

И как и удаление связок, удаление квантора существования это просто применение рекурсора:

theorem Exists.elim {α: Sort u} {p: α → Prop} {b: Prop}
    (h₁: Exists (λx ↦ p x)) (h₂: ∀a: α, p a → b): b :=
  Exists.rec h₂ h₁

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

structure Iff (a b: Prop): Prop where
  intro ::
  mp: a → b
  mpr: b → a

Тип Iff a b также записывается как a ↔ b. Символ ↔ записывается как \iff.

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

Рефлексивность утверждает, что каждое значение равно само себе:

rfl: {α: Sort u} → (a: α) → a = a

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

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

Равенство симметрично и транзитивно:

Eq.symm:  {α: Sort u} → {a b: α} → (h: a = b) → b = a
Eq.trans: {α: Sort u} → {a b c: α} → (h₁: a = b) → (h₂: b = c) → a = c

Наконец, применение функции к равным значениям даёт равные результаты:

congrArg: {α: Sort u} → {β: Sort v} → {x y: α}
  (f: α → β) → (h: x = y) → f x = f y

Вместо того, чтобы явно использовать функции Eq.subst или Eq.ndrec, в Lean можно преобразовывать значение t типа M a в значение типа M b с помощью записи eq ▸ t, где eq это свидетельство равенства a и b.

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

Функция id это тождественная функция:

def id {α: Sort u} (a: α): α := a

Функция absurd это удобный способ получить значение любого типа из свидетельств истинности a и ¬a:

def absurd {a: Prop} {b: Sort v} (h₁: a) (h₂: Not a): b :=
  (h₂ h₁).rec

Композиция строит функцию, склеивая две других функции:

def Function.comp {α: Sort u} {β: Sort v} {δ: Sort w} (f: β → δ) (g: α → β): α → δ :=
  fun x => f (g x)

Выражение Function.comp f g также записывается как f ∘ g. Символ ∘ вводится как \circ.

Одним из полезных применений композиции является следующее:

example (nq: ¬q)(h: p → q): ¬p :=
  nq ∘ h

Если p → q, то тогда ¬q → ¬p. Композиция позволяет применить функцию типа p → q к значению типа ¬q, чтобы получить значение ¬p.

Например, если ¬p, то можно применить And.left чтобы получить свидетельство ¬(p ∧ q):

example (np: ¬p): ¬(p ∧ q) :=
  np ∘ And.left

Синтаксически различные типы в Lean имеют разные пространства имён. Так, хотя тип Not p определён как p → False, у этого типа собственное пространство имён, отличное от пространства имён функций.

Это позволяет определять пространстве имён Not функции, которые имеют смысл именно для отрицания. Одной из таких функций является Not.elim:

Not.elim.{u_1} {p: Prop} {α: Sort u_1} (H1: ¬p) (H2: p): α

Эта функция отличается от функции absurd лишь порядком аргументов. Но в отличие от последней, её можно использовать через точку: h.elim ....

Рассмотрим теперь некоторые новые выражения, полезные для доказательства теорем:

  • have name: type := val;  expr это то же, что и аналогичное выражение с let, но для доказательств высказываний

    • have: type := val это то же, что и have this: type := val

    • Указание типа можно иногда опустить

  • suffices: h type from expr1; expr2 это удобная форма выражения (λh: type ↦ expr1) expr2. В рассуждениях это соответствует конструкции «чтобы доказать Y, достаточно доказать X».

  • show type from expr это другая форма выражения (expr : type)

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

inductive Nat where
| zero: Nat
| succ (n: Nat): Nat

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

Nat.rec: {motive: Nat → Sort u} →
  motive Nat.zero → (∀n: Nat, motive n → motive n.succ) →
  ∀t: Nat, motive t

Для каждого индуктивного типа Lean автоматически определяет некоторый набор вспомогательных функций. Для типа натуральных чисел, одними из таких функций являются Nat.recOn и Nat.casesOn, определённые следующим образом:

def Nat.recOn: {motive: Nat → Sort u} →
    (t: Nat) →
    motive Nat.zero → ((n: Nat) → motive n → motive n.succ) →
    motive t :=
  λ{motive} t zero succ ↦ Nat.rec zero succ t

def Nat.casesOn: {motive: Nat → Sort u} →
    (t: Nat) → motive Nat.zero → ((n: Nat) → motive n.succ) → motive t :=
  λ{motive} t zero succ ↦ Nat.rec zero (fun n n_ih => succ n) t

Кроме использования casesOn, значение индуктивного типа можно разобрать используя сопоставление с образцом. Для этого в Lean есть выражение match ... with .... Вот пример его использования:

example (n: Nat): Nat :=
  match n with
  | Nat.zero => 1
  | Nat.succ n => n

Кроме наглядности, у сопоставления с образцом есть ещё одно преимущество. Выражение match заменяет разбираемое выражение в контексте каждой из ветвей на соответствующие каждой из ветвей выражения. Так, если контекст вне выражения match содержит h: M n, то в ветви Nat.zero это предположение превращается в h: M Nat.zero, а в ветви Nat. succ n — в M (Nat.succ n).

Сложение#

Сложение двух натуральных чисел определено в Lean следующим образом:

def Nat.add: Nat → Nat → Nat
| a, Nat.zero   => a
| a, Nat.succ b => Nat.succ (Nat.add a b)

Это рекурсивное определение, использующее сопоставление с образцом. Ту же самую функцию можно определить, используя рекурсор:

noncomputable
example (n k: Nat): Nat :=
  k.recOn n (λ_ s ↦ Nat.succ s)

Lean это одновременно и средство доказательство теорем, и язык программирования. Ядро Lean, ответственное за проверку типов, оперирует рекурсорами, однако компилятор в машинный код понимает только сопоставление с образцом. Ключевое слово noncomputable (не имеющее отношения к математическому понятию вычислимости) указывает, что функция не предназначена для компиляции.

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

Скомпилировать и выполнить выражение в Lean можно с помощью команды #eval:

#eval 2 + 3

Скомпилированный код выполняется намного быстрее, чем код, интерпретируемый ядром Lean. Однако, компиляция применима только к выражениям, результатом которых является значение типа данных. Напротив, команда #reduce способно символьно вычислять выражения даже внутри абстракции:

#reduce λn ↦ n + 3

Перейдём, наконец, к доказательствам. Легенда гласит, что Уайтхеду и Расселу потребовалось более сотни страниц чтобы доказать, что \(1+1 = 2\) 1. Конструктивная природа исчисления построений, однако, позволяет доказать это высказывание в одну строчку:

example: 1 + 1 = 2 := rfl

Схожим образом доказываются и некоторые другие высказывания:

theorem add_zero  (n: Nat):   n + 0 = n                  := rfl
theorem add_one   (n: Nat):   n + 1 = n.succ             := rfl
theorem add_succ  (n k: Nat): n + k.succ = (n + k).succ  := rfl

Однако, высказывание \(0 + n = n\) доказать вычислением уже нельзя. Но его можно доказать индуктивно:

  • База индукции: \(0+0 = 0\) по определению

  • Шаг индукции: пусть для любого \(n\) верно \(0+n = n\). Тогда верно \((0+n).succ = n.succ\), что по определению совпадает с высказыванием \(0 + n.succ = n.succ\), которое требовалось доказать

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

theorem zero_add (n: Nat): 0 + n = n :=
  n.recOn
    (show 0 + 0 = 0 from rfl)
    (λn (h: 0 + n = n) ↦
      show 0 + n.succ = n.succ from
      congrArg Nat.succ h)

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

theorem zero_add_match: (n: Nat) → 0 + n = n
| 0 => show 0 + 0 = 0 from rfl
| Nat.succ n =>
  show 0 + n.succ = n.succ from
  congrArg Nat.succ (zero_add_match n)

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

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

\[\begin{split}\begin{aligned} 0 + n.succ &= (0 + n).succ & &(add\_succ)\\ &= n.succ & &(\text{предположение индукции}) \end{aligned}\end{split}\]

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

example (n: Nat): 0 + n = n :=
  n.recOn
    rfl
    (λn (h: 0 + n = n) ↦
      calc
        0 + n.succ = (0 + n).succ := add_succ 0 n
        _          = n.succ       := h.symm ▸ (rfl : n.succ = n.succ))

Выражение calc позволяет соединить последовательность равенств. Общая форма этого выражения:

calc
  e1 = e2 := (доказательство равенства e1 и e2)
  e2 = e3 := (доказательство равенства e2 и e3)
  ...

Части выражений в равенствах можно заменять на дырки. Обычно, заменяют левые части равенств кроме самого первого равенства в цепочке.

Доказательство (0 + n).succ = n строится из n.succ = n.succ заменой n.succ на 0 + n. Замена осуществляется применением индукционного предположения с помощью ▸, который осуществляет подстановку, выводя требуемый мотив.

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

В доказательстве выше указание типа rfl не требуется. Оно было добавлено для наглядности.

Выражение это не единственная форма доказательств в Lean. Высказывание также можно доказать, используя тактики.

Тактика это инструкция, строящая доказательство цели. При этом она может открывать новые цели и влиять на контекст доказательства.

Рассмотрим как использовать тактики на примере доказательства всё того же высказывания. Начнём с заготовки доказательства:

example (n: Nat): 0 + n = n := by
  sorry

Ключевое слово by открывает блок тактик. Тактика sorry аналогична соответствующему выражению — это заготовка, которую следует заменить доказательством.

Поставим курсор непосредственно перед словом sorry. Lean Infoview отобразит соответствующий позиции курсора контекст доказательства:

n : Nat
⊢ 0 + n = n

Нам дано число n, и нам требуется построить доказательство 0 + n = n. Сделаем это, используя тактику refine:

example (n: Nat): 0 + n = n := by
  refine n.recOn ?z ?s

Тактика refine использует данное ей выражение для доказательства цели. Части выражения могут быть заменены метапеременными (которые обозначаются вопросительным знаком), при этом refine создаёт новые цели, соответствующие метапеременным.

Lean теперь сообщает нам, что доказательство не завершено, так как есть незакрытые цели:

unsolved goals

case z
n : Nat
⊢ 0 + Nat.zero = Nat.zero

case s
n : Nat
⊢ ∀ (n : Nat), 0 + n = n → 0 + n.succ = n.succ

Закроем их заглушками:

example (n: Nat): 0 + n = n := by
  refine n.recOn ?z ?s
  · sorry
  · sorry

Символ ⋅, которые вводится как \., начинает блок, фокусирующийся на первой из доступных целей.

Укажем явно первую цель с помощью тактики show:

example (n: Nat): 0 + n = n := by
  refine n.recOn ?z ?s
  · show 0 + 0 = 0
    sorry
  · sorry

И закроем её:

example (n: Nat): 0 + n = n := by
  refine n.recOn ?z ?s
  · show 0 + 0 = 0
    exact rfl
  · sorry

Тактика exact работает точно так же, как и тактика refine, но в отличие от неё не создаёт новых целей.

Рефлексивность также доказывается тактикой rfl, без использования exact.

Перейдём ко второй цели. Её контекст:

case s
n : Nat
⊢ ∀ (n : Nat), 0 + n = n → 0 + n.succ = n.succ

Используем тактику intro чтобы ввести предположения:

example (n: Nat): 0 + n = n := by
  refine n.recOn ?z ?s
  · show 0 + 0 = 0
    exact rfl
  · intro n (h: 0 + n = n)
    sorry

После введения предположений контекст доказательства принимает вид:

case s
n✝ n : Nat
h : 0 + n = n
⊢ 0 + n.succ = n.succ

Тактика intro ... действует как refine λ... ↦ ?_. Ввод новой переменной затеняет предыдущую переменную с тем же именем, и Lean Infoview помечает затенённую переменную символом ✝.

Завершим доказательство, закрыв вторую цель:

example (n: Nat): 0 + n = n := by
  refine n.recOn ?z ?s
  · show 0 + 0 = 0
    exact rfl
  · intro n (h: 0 + n = n)
    show 0 + n.succ = n.succ
    exact congrArg Nat.succ h

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

Начнём с использования refine:

example (n: Nat): 0 + n = n := by
  refine n.recOn rfl (λn h ↦ ?_)

Контекст доказательства:

n✝ n : Nat
h : 0 + n = n
⊢ 0 + n.succ = n.succ

Используем тактику rw чтобы переписать цель доказательства:

example (n: Nat): 0 + n = n := by
  refine n.recOn rfl (λn h ↦ ?_)
  rw [add_succ]

Контекст после применения rw:

n✝ n : Nat
h : 0 + n = n
⊢ (0 + n).succ = n.succ

Тактика rw использует данное ей свидетельство равенства чтобы переписать цель. Если вместо свидетельства равенства ей даётся функция, результатом которой является свидетельство равенства, то тактика rw сама применяет её к требуемым значениям.

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

example (n: Nat): 0 + n = n := by
  refine n.recOn rfl (λn h ↦ ?_)
  rw [add_succ]
  rw [h]

Вместо того, чтобы применять rw несколько раз, можно просто перечислить все применяемые равенства в квадратных скобках перед rw. Чтобы равенство использовалось в обратную сторону, достаточно поставить символ ← (вводится как \gets или \leftarrow) перед дающим равенство выражением, например, как в rw [←add_succ].

Переписывание чувствительно к форме типа, и потому в доказательстве выше rw [add_succ] нельзя опустить. Однако, можно использовать тактику show, чтобы заменить цель на вычислительно ей равную:

example (n: Nat): 0 + n = n := by
  refine n.recOn rfl (λn h ↦ ?_)
  show (0 + n).succ = n.succ
  rw [h]

Тактики suffices, have, let и calc работают точно так же, как и соответствующие выражения. Тактика match же отличается от выражения тем, что её ветвями являются блоки тактик, а не выражения.

Данная книга добавляет в Lean ещё одну тактику: reader. Она является синонимом sorry и обозначает то, что читатель должен доказать самостоятельно.

Блок тактик является выражением. Поэтому, вместо того, чтобы использовать выражения в тактиках с помощью refine, можно наоборот использовать тактики в выражениях с помощью by.

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

theorem succ_add (n k: Nat): n.succ + k = (n + k).succ := by reader
theorem add_comm (n k: Nat): n + k = k + n := by reader

У читателя есть возможность выбрать переменную индукции. Он выбирает мудро, но если доказательство зашло в тупик, выбирает другую переменную.

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

theorem add_assoc (m n k: Nat): (m + n) + k = m + (n + k) := by
  refine k.recOn rfl (λk h ↦ ?_)
  calc
    (m + n) + k.succ = ((m + n) + k).succ := by rw [add_succ]
    _                = (m + (n + k)).succ := by rw [h]
    _                = m + (n + k).succ   := by rw [←add_succ]
    _                = m + (n + k.succ)   := by rw [←add_succ]

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

example (m n k: Nat): (m + n) + k = m + (n + k) := by
  refine k.recOn rfl (λk h ↦ ?s)
  calc
    (m + n) + k.succ = ((m + n) + k).succ := rfl
    _                = (m + (n + k)).succ := by rw [h]

Но Lean позволяет доказать её ещё короче:

example {m n k: Nat}: (m + n) + k = m + (n + k) :=
  k.recOn rfl (λk h ↦ by simp only [add_succ, h])

Тактика simp это автоматизированная версия тактики rw, которая, вместо того, чтобы применять равенства по порядку, сама ищет нужную последовательность применений. Если она не может закрыть цель, она осуществляет направленное переписывание цели пока это возможно.

Важно иметь в виду, чтобы если набор равенств допускает бесконечное переписывание, тактика simp может просрочиться, так и не найдя решение.

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

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

example (a b c d e: Nat): (((a + b) + c) + d) + e = (c + ((b + e) + a)) + d :=
  by ac_rfl

Тактика ac_rfl доказывает, что два значения равны с точностью до перестановки скобок и членов в скобках.

Функция Nat.pred определена следующим образом:

def Nat.pred: Nat → Nat
| 0      => 0
| succ a => a

Для неё по определению верны следующие равенства:

theorem pred_zero: (0: Nat).pred = 0 := rfl
theorem pred_succ (n: Nat): n.succ.pred = n := rfl

Используя функцию Nat.pred, читателю не составит большого труда доказать следующие леммы:

theorem succ_cancel {n k: Nat}(e: n.succ = k.succ): n = k := by reader
theorem add_right_cancel {m n k: Nat}: (m+k = n+k) → m = n := by reader
theorem add_left_cancel {m n k: Nat}: (k+m = k+n) → m = n := by reader
theorem add_eq_zero_left {n k: Nat}: (n + k = 0) → n = 0 := by reader
theorem add_eq_zero_right {n k: Nat}: (n + k = 0) → k = 0 := by reader

Замечание: у большинства этих упражнений справа от двоеточия находится импликация. Это не случайно. Таким образом, предположения могут стать частью мотива индукции.

Как и с типом Bool, который мы рассматривали в предыдущей главе, вместе с типом Nat Lean определяет функцию Nat.noConfusion. Она позволяет доказать, что нуль не следует ни за каким натуральным числом:

theorem succ_ne_zero (n:Nat): n.succ ≠ 0 := Nat.noConfusion

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

theorem succ_ne_self (n:Nat): n.succ ≠ n := by reader

Сравнения#

Символ ≤ представляет собой отношение «меньше или равно» и вводится как \le. На натуральных числах это отношение определено следующим образом:

inductive Nat.le (n: Nat): Nat → Prop
| refl     : Nat.le n n
| step {m} : Nat.le n m → Nat.le n (succ m)

Nat.le это параметризованное индуктивное семейство типов. Семейство типов это функция, результат применения которой к некоторому значению, называемому индексом, является типом. Например, результатом применения Nat.le n к индексу k является тип Nat.le n k.

Мы говорим, что тип принадлежит семейству типов, если он построен применением семейства типов к некоторому индексу.

В отличие от конструкторов значений индуктивного типа, которые строят всегда значения одного и того же типа, конструктор значений семейства типов строят значение, тип которого зависит от данного конструктора и его аргументов. При этом, этот тип принадлежит соответствующему семейству типов. Например, @Nat.le.refl n имеет тип Nat.le n n и принадлежит семейству типов Nat.le n.

Вычислительные равенства, которым удовлетворяет рекурсор семейства типов, аналогичны равенствам, которым удовлетворяет индуктивный тип. Например, рекурсор семейства типов Nat.le n удовлетворяет следующим равенствам:

Nat.le.rec r s (@Nat.le.refl n) ≡ r
Nat.le.rec r s (@Nat.le.step n m h) ≡ s m h (Nat.le.rec r s h)

Из этих равенств следует, что он имеет следующий тип:

Nat.le.rec: ∀{n: Nat} {motive: ∀m: Nat, n ≤ a → Prop},
  motive n Nat.le.refl →
  (∀{m: Nat} (h: n ≤ m), motive m h → motive m.succ (Nat.le.step h)) →
  ∀{m: Nat} (h: n ≤ m), motive m h

Тип рекурсора можно всегда узнать с помощью команд #print или #check.

Кстати, равенство также является семейством типов, и его рекурсор схож с рекурсором Nat.le:

Eq.rec.{u, v}: ∀{α: Sort v} {a: α} {motive: ∀b: α, a = b → Sort u},
  motive a (Eq.refl a) →
  ∀{b: α} (t: a = b), motive b t

Отношение «меньше» на натуральных числах определяется через отношение «меньше или равно»:

def Nat.lt (n k: Nat): Prop :=
  Nat.le (succ n) k

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

theorem le_refl (n: Nat): n ≤ n := Nat.le.refl
theorem le_succ (n: Nat): n ≤ n.succ := Nat.le.step (le_refl n)
theorem le_succ_of_le {n k: Nat}: n ≤ k → n ≤ k.succ := Nat.le.step

Докажем теперь, что отношение «меньше или равно» транзитивно:

theorem le_trans {m n k: Nat}(mn: m ≤ n)(nk: n ≤ k): m ≤ k :=
  nk.recOn
    (show m ≤ n from mn)
    (λ{k} (_: n ≤ k) (h: m ≤ k) ↦
      show m ≤ k.succ from le_succ_of_le h)

Это доказательство индукцией по отношению «меньше или равно». Фигурные скобки при лямбде позволяют указать неявной аргумент функции, к которой применяется рекурсор.

Доказательство транзитивности даёт нам право соединять цепь неравенств в выражении calc:

example {m n k: Nat}(mn: m ≤ n)(nk: n ≤ k): m ≤ k :=
  calc
    m ≤ n := mn
    n ≤ k := nk

Следующие высказывания предстоит доказать читателю:

theorem le_of_succ_le {n k: Nat}(le: n.succ ≤ k): n ≤ k := by reader
theorem succ_le_succ {n m: Nat}(le: n ≤ m): n.succ ≤ m.succ := by reader
theorem zero_le (n: Nat): 0 ≤ n := by reader
theorem zero_lt_succ (n: Nat): 0 < n.succ := by reader

theorem pred_le (n: Nat): n.pred ≤ n := by reader
theorem pred_lt {n: Nat}(pn: n ≠ 0): n.pred < n := by reader
theorem pred_le_of_le {n k: Nat}(le: n ≤ k): n.pred ≤ k := by reader
theorem pred_le_pred {n k: Nat}(le: n ≤ k): n.pred ≤ k.pred := by reader
theorem le_of_succ_le_succ {n m: Nat}: n.succ ≤ m.succ → n ≤ m := by reader

Замечание: индукция по отношению «меньше или равно», как правило, полезнее индукции по числу.

Докажем теперь, что единица не является меньше или равной нулю:

theorem not_one_le_zero: ¬1 ≤ 0 := by
  suffices any_zero: ∀k, 1 ≤ k → k = 0 → False from
    λh ↦ any_zero 0 h rfl
  exact λk ok ↦ ok.recOn
    (λ(h: 1 = 0) ↦ succ_ne_zero 0 h)
    (λ{k} _ _ (ksz: k.succ = 0) ↦ succ_ne_zero k ksz)

Хотя это доказательство очевидно, его не так просто найти 2. Мы обобщаем задачу: доказываем, что для любого k, если 1 ≤ k, то k не равно нулю. Это обобщение позволяет использовать индукцию по 1 ≤ k.

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

example: ∀k: Nat, 1 ≤ k → k = 0 → False :=
  λk ok ↦ @Nat.le.recOn _ (λk _ ↦ k = 0 → False) k ok
    (λ(h: 1 = 0) ↦ succ_ne_zero 0 h)
    (λ{k} _ _ (ksz: k.succ = 0) ↦ succ_ne_zero k ksz)

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

Ещё упражнения:

theorem not_succ_le_zero (n: Nat): ¬n.succ ≤ 0 := by reader
theorem not_succ_le_self (n: Nat): ¬n.succ ≤ n := by reader
theorem eq_zero_of_le_zero {n: Nat} (h: n ≤ 0): n = 0 := by reader
theorem lt_irrefl (n: Nat): ¬n < n := by reader
theorem pos_iff_ne_zero {n: Nat}: 0 < n ↔ n ≠ 0 := ⟨by reader, by reader⟩

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

Поскольку доказательства становятся сложнее, нужно сказать пару слов о том, как писать доказательства.

Написание доказательства это глубоко нелинейный процесс. Когда в доказательстве возникает трудное место, не стоит немедленно брать его наскоком. Вместо этого стоит использовать have: proposition := sorry, чтобы отложить доказательство трудного шага на потом, и вернутся к нему, когда будут готовы остальные части доказательства изначального высказывания.

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

Совершение ошибок и их исправление — неотъемлемая часть мышления. Изначальный план может зайти в тупик, и тогда нужно вернуться назад и пересмотреть принятые ранее решения.

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

theorem le_add (n k: Nat): n ≤ n + k := by reader
theorem le_add_of_le {m n: Nat}(k: Nat)(le: m ≤ n): m ≤ n + k := by reader
theorem add_le_add_left {n k: Nat}(l: n ≤ k): ∀p, n + p ≤ k + p := by reader
theorem le_of_add_le_add_left {m n k: Nat}: (h: m + n ≤ m + k) → n ≤ k := by reader
theorem not_add_le_self (n: Nat){k: Nat}(pk: 0 < k): ¬(n + k ≤ n) := by reader

Следующие две леммы связывают отношение «меньше или равно» с существованием числа:

theorem exists_of_le {n k: Nat}(le: n ≤ k): ∃p, n + p = k :=
  le.recOn
    ⟨0, rfl⟩
    (λ_ ⟨p,h⟩ ↦ ⟨p.succ, congrArg Nat.succ h⟩)

theorem le_of_exists {n k: Nat}: (ex: ∃d, n + d = k) → n ≤ k := by
  refine k.recOn ?_ ?_
  · intro ex
    show n ≤ 0
    let ⟨d, (hd: n + d = 0)⟩ := ex
    suffices nz: n = 0 from nz ▸ le_refl n
    exact add_eq_zero_left hd
  · intro k _ ex
    show n ≤ k.succ
    let ⟨d, (hd: n + d = k.succ)⟩ := ex
    suffices h: n ≤ n + d from hd ▸ h
    exact le_add n d

Первая лемма в стандартной библиотеке Lean имеет имя Nat.exists_eq_add_of_le. Мы дали ей другое, более короткое имя.

Ещё упражнения читателю:

theorem le_antisymm {n k: Nat}(nk: n ≤ k): (kn: k ≤ n) → n = k := by reader
theorem eq_or_lt_of_le {n m: Nat}(nm: n ≤ m): (n = m) ∨ (n < m) := by
  suffices h: ∀m, n ≤ m → (n = m) ∨ (n < m) from h m nm
  reader
theorem lt_or_ge (n k: Nat): n < k ∨ k ≤ n :=
  suffices h: ∀n, n < k ∨ k ≤ n from h n
  by reader
theorem not_le_of_gt {n k: Nat}(h: n > k): ¬n ≤ k := by reader
theorem not_lt_of_ge {n k: Nat}(h: k ≥ n): ¬(k < n) := by reader

Подсказка: в доказательствах eq_or_lt_of_le и lt_or_ge можно неоднократно использовать match.

Разрешимость#

Время узнать, как на самом деле определены бинарные отношения и связки в Lean. Начнём с отношения «меньше или равно».

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

infix:50 " ≤ " => LE.le

Эта запись синтаксически определяет a ≤ b как LE.le x y.

Посмотрим теперь на определение LE:

class LE (α : Type u) where
  le : α → α → Prop

LE это так называемый класс типов. Класс типов представляет собой параметризованный индуктивный тип. В случае LE, это структура с единственным полем LE.le.

Значение класса типов называется инстансом класса. В Lean есть механизм для поиска объявленных инстансов данного класса.

Используем команду #synth чтобы найти инстанс типа LE Nat:

#synth LE Nat    -- instLENat

Инстанс instLENat объявлен следующим образом:

instance instLENat: LE Nat where
  le := Nat.le

Таким образом, instLENat.le это по определению функция Nat.le.

Посмотрим теперь на тип функции LE.le:

LE.le: {α: Type u} → [self: LE α] → α → α → Prop

В отличие от обычной структуры, значение типа LE α в типе LE.le является неявным параметром. Этот параметр обозначается не фигурными скобками, а квадратными, что означает, что значение находится не с помощью унификации (решения синтаксических уравнений), а с помощью механизма поиска инстансов класса.

Таким образом, если n и k это натуральные числа, то поскольку инстансом типа Nat.le Nat является instLENat, LE.le n k раскрывается в LE.le (self := instLENat) n k, что по определению равно Nat.le n k.

Натуральные, целые и вещественные числа представлены различными типами, которым соответствуют три различных определения отношения «меньше или равно». Класс типов LE позволяет использовать одну и ту же запись для этих трёх отношений.

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

Арифметические операции в Lean также сводятся к соответствующим классам типов:

infixl:65 " + " => HAdd.hAdd
infixl:65 " - " => HSub.hSub
infixl:70 " * " => HMul.hMul
infixl:70 " / " => HDiv.hDiv
infixl:70 " % " => HMod.hMod

Посмотрим на определение класса HAdd:

class HAdd (α: Type u) (β: Type v) (γ: outParam (Type w)) where
  hAdd: α → β → γ

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

Тождественная функция outparam указывает Lean, что γ является выходным параметром класса. Выходные параметры отличаются от обычных порядком вывода типов. Когда Lean пытается вывести тип HAdd ?α ?β ?γ, он откладывает вывод типа ?γ до тех пор, пока типы ?α и ?β не будут известны. Но когда эти типы известны, Lean ищет инстанс типа HAdd ?α ?β ?δ, и, если находит, разрешает тип ?γ как тип ?δ.

Попробуем найти инстанс класса HAdd для натуральных чисел:

#synth HAdd Nat Nat Nat    -- instHAdd

В определение найденного инстанса, однако, тип Nat не входит:

instance instHAdd [Add α]: HAdd α α α where
  hAdd a b := Add.add a b

instHAdd представляет собой обобщённый инстанс, определённый для любого типа α, для которого существует инстанс типа Add α. Поскольку инстанс instHAdd определён для натуральных чисел, должен быть также определён инстанс типа Add Nat.

Класс Add определён следующим образом:

class Add (α: Type u) where
  add: α → α → α

А инстанс этого класса сводит сложение натуральных чисел к применению функции Nat.add:

instance instAddNat: Add Nat where
  add := Nat.add

Одним из важнейших понятий конструктивной математики является разрешимость.

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

class inductive Decidable (p: Prop) where
| isFalse (h: ¬p): Decidable p
| isTrue (h: p): Decidable p

В отличие от высказывания p ∨ ¬p, Decidable p имеет тип Type. Это означает, что варианты типа Decidable p различимы, используя рекурсор или сопоставление с образцом можно построить то или иное значение в зависимости от того, истинно p или ложно.

Отношение «меньше или равно» на натуральных числах разрешимо:

def decLe: (n m: Nat) → Decidable (n ≤ m)
| Nat.zero, Nat.zero     => Decidable.isTrue (le_refl 0)
| Nat.zero, m            => Decidable.isTrue (zero_le m)
| Nat.succ n, Nat.zero   => Decidable.isFalse (not_succ_le_zero n)
| Nat.succ n, Nat.succ m =>
  match decLe n m with
  | Decidable.isTrue h  => Decidable.isTrue (succ_le_succ h)
  | Decidable.isFalse h => Decidable.isFalse (h ∘ le_of_succ_le_succ)

Попросим Lean найти инстанс типа Decidable (2 ≤ 3):

#synth Decidable (2 ≤ 3)    -- Nat.decLe 2 3

Таким же образом, для любых натуральных n и k, Lean может автоматически построить значение типа Decidable (n ≤ k).

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

def Decidable.decide (p: Prop) [h: Decidable p]: Bool :=
  h.casesOn (λ_ ↦ false) (λ_ ↦ true)

Очевидно, что для любого разрешимого высказывания p, decide p равно false когда p ложно, и равно true, когда p истинно. В стандартной библиотеке Lean это доказывается следующими леммами:

def decide_eq_false [inst : Decidable p]: ¬p → (decide p) = false :=
  inst.recOn (λ_ _ ↦ rfl) (λhp hnp ↦ absurd hp hnp)

def decide_eq_true [inst : Decidable p]: p → (decide p) = true :=
  inst.recOn (λhnp hp ↦ absurd hp hnp) (λ_ _ ↦ rfl)

Но верно и обратное: из того, что decide p = true следует, что p истинно. Доказательство:

def of_decide_eq_true [inst: Decidable p](eq: (decide p) = true): p :=
  match (generalizing := false) inst with
  | isTrue h => h
  | isFalse h => absurd eq (ne_true_of_eq_false (decide_eq_false h))

Опция generalizing := false указывает, что предположение не должно быть включено в мотив сопоставления с образцом. Это необходимо, так как в противном случае неявный аргумент функции decide_eq_false не совпадёт с инстансом inst.

Лемма of_decide_eq_true позволяет доказывать высказывания вычислением:

example: 0 ≤ 2 := of_decide_eq_true rfl

И, разумеется, в Lean для этого уже есть тактика:

example: 0 ≤ 2 := by decide

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

def ite {α: Sort u} (c: Prop) [h: Decidable c] (t e: α): α :=
  h.casesOn (fun _ => e) (fun _ => t)

Хотя это функцию можно использовать напрямую, Lean также определяет для неё синтаксис вида if c then t else e. Так, например, с помощью этого синтаксиса выражение ite (n ≤ k) true false записывается следующим образом:

example (n k: Nat): Bool :=
  if n ≤ k then
    true
  else
    false

Иногда, чтобы построить значение, требуется свидетельство истинности высказывания или его отрицания. Для этого в Lean определена зависимая версия функции ite:

def dite {α: Sort u} (c: Prop) [h: Decidable c] (t: c → α) (e: Not c → α): α :=
  h.casesOn e t

Как и для функции ite, для функции dite Lean вводит отдельный синтаксис. Этот синтаксис почти тот же, что и у функции ite:

example [Decidable p]: p ∨ ¬p :=
  if h: p then Or.inl h
  else Or.inr h

Для функций ite и dite, в стандартной библиотеке Lean определены функции со следующими типами:

if_pos: {c: Prop} → {h: Decidable c} →
  (hc: c) → {α: Sort u} → {t e: α} → (ite c t e) = t
if_neg: {c: Prop} → {h: Decidable c} →
  (hnc: ¬c) → {α: Sort u} → {t e: α} → (ite c t e) = e

dif_pos: {c: Prop} → {h: Decidable c} →
  (hc: c) → {α: Sort u} → {t: c → α} → {e: ¬c → α} → (dite c t e) = t hc
dif_neg: {c: Prop} → {h: Decidable c} →
  (hnc: ¬c) → {α: Sort u} → {t: c → α} → {e: ¬c → α} → (dite c t e) = e hnc

Забегая вперёд, в стандартной библиотеке Lean также вводит следующую аксиому:

axiom propext {a b: Prop}: (a ↔ b) → a = b

Тактика simp использует эту аксиому чтобы преобразовывать истинные и ложные высказывания, соответственно, в высказывания True и False. После чего, для упрощения выражений используются леммы из стандартной библиотеки для этих двух высказываний.

Обсуждение аксиомы propext мы оставим на потом, и потому в этой главе для работы с ite и dite мы будем использовать леммы if_pos, if_neg, dif_pos и dif_neg.

Вычитание#

Разность двух натуральных чисел в Lean определена следующим образом:

def Nat.sub: Nat → Nat → Nat
| a, 0          => a
| a, Nat.succ b => pred (Nat.sub a b)

Вычитание на натуральных числах это вычитание с насыщением: результатом вычитания большего числа из меньшего является нуль. Такое вычитание ведёт себя хуже, чем привычное вычитание на целых числах, так как оно в общем случае не коммутирует со сложением (то есть \((a + b) - c ≠ a + (b - c)\)).

Леммы sub_zero и sub_succ повторяют определение:

theorem sub_zero (n: Nat): n - 0 = n := rfl
theorem sub_succ (n k: Nat): n - k.succ = (n - k).pred := rfl

Остальные леммы кроме одной докажет читатель. Сначала эти:

theorem zero_sub (n: Nat): 0 - n = 0 := by reader
theorem succ_sub_succ (n m: Nat): n.succ - m.succ = n - m := by reader
theorem sub_self (n: Nat): n - n = 0 := by reader
theorem sub_eq_zero_of_le {n k: Nat}(h: n ≤ k): n - k = 0 := by reader
theorem sub_le (n m: Nat): n - m ≤ n := by reader

Доказательство леммы sub_lt является хорошим примером использования сопоставления с образцом. Рассмотрим его подробнее:

theorem sub_lt {n m: Nat}(pn: 0 < n)(pm: 0 < m): n - m < n :=
  match n, m with
  | Nat.zero, _ => absurd pn (lt_irrefl 0)
  | _, Nat.zero => absurd pm (lt_irrefl 0)
  | Nat.succ n, Nat.succ m =>
    calc
      n.succ - m.succ = n - m := by rw [succ_sub_succ]
      _ < n.succ := succ_le_succ (sub_le n m)

Сопоставление с образцом может быть применено к нескольким значениям одновременно. При этом Lean следит, чтобы были рассмотрены все возможности.

Остальные леммы также докажет читатель:

theorem sub_le_sub_left {n m: Nat}(h: n ≤ m)(k: Nat): k - m ≤ k - n := by reader

theorem sub_le_sub_right {n m: Nat} (le: n ≤ m) (k: Nat): n - k ≤ m - k :=
  suffices h: ∀k, n ≤ m → n - k ≤ m - k from h k le
  by reader

theorem sub_sub (n m k: Nat): n - m - k = n - (m + k) := by reader

theorem add_sub_cancel (n m: Nat): n + m - m = n := by reader

theorem succ_sub {n k: Nat}(h: k ≤ n): n.succ - k = (n - k).succ := by
  let ⟨d, hd⟩ := exists_of_le h
  rw [←hd]
  reader

theorem sub_add_comm {n m k: Nat}(h: k ≤ n): n + m - k = n - k + m := by reader

theorem sub_add_cancel {n k: Nat} (h: k ≤ n): n - k + k = n := by reader

theorem add_sub_assoc {m k: Nat} (h: k ≤ m) (n: Nat): n + m - k = n + (m - k) := by
  let ⟨d, hd⟩ := exists_of_le h
  rw [←hd]
  reader

Умножение#

Определение умножения в Lean:

def Nat.mul: Nat → Nat → Nat
| a, Nat.zero   => a
| a, Nat.succ b => Nat.add (Nat.mul a b) a

И соответствующие этому определению леммы:

theorem mul_zero (n: Nat):   n * 0 = 0               := rfl
theorem mul_succ (n k: Nat): n * k.succ = n * k + n  := rfl

Как и раньше, читатель докажет всё остальное. Сначала основные свойства умножения:

theorem mul_one (n: Nat): n * 1 = n := by reader
theorem zero_mul (n: Nat): 0 * n = 0 := by reader
theorem succ_mul (n k: Nat): n.succ * k = n * k + k := by reader
theorem one_mul (n:Nat): 1*n = n := by reader

theorem mul_comm (n k: Nat): n * k = k * n := by reader
theorem mul_left_distr (n k p: Nat): n * (k + p) = n * k + n * p := by reader
theorem mul_right_distr (n k p: Nat): (n + k) * p = n * p + k * p := by reader
theorem mul_assoc (m n k: Nat): (m * n) * k = m * (n * k) := by reader

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

Доказав коммутативность и ассоциативность, мы имеем право использовать ac_rfl:

example {a b c d e: Nat}: (((a * b) * c) * d) * e = (c * ((b * e) * a)) * d :=
by ac_rfl

Ещё одна лемма:

theorem mul_eq_zero {n k: Nat}: (n * k = 0) → n = 0 ∨ k = 0 := by reader

Следующая лемма значительно труднее остальных:

theorem mul_left_cancel {m n k: Nat}(pm: m ≠ 0): (m * n = m * k) → n = k := by
  suffices h: ∀n, (m * n = m * k) → n = k from h n
  refine k.recOn ?_ ?_
  · reader
  · reader

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

Остальные леммы:

theorem pos_of_mul_pos_left {n k: Nat}(h: 0 < n * k): 0 < k := by reader

theorem mul_le_mul_left {n k: Nat}(m: Nat)(h: n ≤ k): m * n ≤ m * k := by reader

theorem le_of_mul_le_mul_left {m n k: Nat}(pk: 0 < m): (m * n ≤ m * k) → n ≤ k :=
  match lt_or_ge k n with
  | Or.inr h => by reader
  | Or.inl (nm: k < n) => by reader

theorem mul_sub_left_distrib (m n k: Nat): m * (n - k) = m * n - m * k :=
  if h: n ≥ k then by reader
  else by reader

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

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

Сильная индукция#

В главе «Исчисление построений», когда рассматривали индуктивные типы, мы сопоставляли индукции процесс построения доказательства для каждого значения индуктивного типа. Так, если \(M\) это некоторое доказанное индукцией свойство натуральных чисел, то тогда доказательство \(M\ 3\) строится следующим образом:

  1. Так как для любого \(n\), из \(M\ n\) следует \(M\ (succ\ n)\), чтобы доказать \(M\ (succ\ (succ\ (succ\ zero)))\), достаточно доказать \(M\ (succ\ (succ\ zero))\)

  2. Чтобы доказать \(M\ (succ\ (succ\ zero))\), достаточно доказать \(M\ (succ\ zero)\)

  3. Чтобы доказать \(M\ (succ\ zero))\), достаточно доказать \(M\ zero\)

  4. Но \(M\ zero\) это база индукции

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

Но чтобы рекурсивно построить доказательство, не обязательно сводить выполнимость свойства для данного числа к выполнимости свойства для непосредственного его предшественника. Ясно, что если всегда брать любое число меньшее данного, не важно какое, то процесс доказательства в конце-концов завершится. Это позволяет предположить следующий принцип.

Принцип сильной индукции: пусть для каждого натурального \(n\) из того, что для любого натурального \(k\) меньше \(n\) и верно \(M\ k\), следует \(M\ n\). Тогда для любого \(n\) верно \(M\ n\).

Формально, это высказывание записывается следующим образом:

\[(∀n: ℕ.\; (∀k: ℕ.\; k < n → M\ k) → M\ n) → ∀n.\; M\ n\]

Нашей задачей будут доказательство и обобщение этого принципа.

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

def Nat.succRel (n k: Nat) := n.succ = k

Графически, это отношение можно изобразить следующим образом:

../_images/succ-rel.svg

Пусть \(r\) это бинарное отношение на типе \(α\). Будем называть отношение \(r\) индуктивным, если оно удовлетворяет следующему свойству:

def Ind.{u} (r: α → α → Prop) :=
  ∀{M: α → Sort u}, (∀x, (∀y, r y x → M y) → M x) → ∀x, M x

.{u} перед именем функции означает уровень вселенной. При применении функции, уровень можно уточнить, указав соответствующее число в фигурных скобках. Так, Ind.{0} означает функцию Ind, где уровень u это нуль.

Отношение Nat.succRel индуктивно:

def indSuccRel: Ind Nat.succRel :=
  λ{M} (ind: ∀x, (∀y: Nat, y.succRel x → M y) → M x) ↦ by
    refine Nat.rec ?z (λn (h: M n) ↦ ?_)
    · show M 0
      exact ind 0 (λn s ↦ absurd s (succ_ne_zero n))
    · suffices hk: ∀k, k.succRel n.succ → M k from ind n.succ hk
      intro k s
      have: k = n := congrArg Nat.pred s
      exact this ▸ h

Таким образом, и обычная, и сильная индукция являются частными случаями индукции по индуктивному отношению. Принцип сильной индукции равносилен тому, что Nat.le является индуктивным отношением.

Каждому индуктивному типу можно сопоставить бинарное отношение, подобное Nat.succRel, что соотносит каждому значению t индуктивного типа значение того же типа, являющееся частью, из которой t было построено. Но можно и наоборот, сопоставить бинарному отношению соответствующий ему индуктивный тип.

Пусть \(r\) это бинарное отношение на \(α\). Значение \(x\) типа \(α\) называется достижимым по \(r\), если достижимы все \(y\), такие, что \(r\ y\ x\).

Отношение \(r\) называется фундированным, если каждый \(x\) типа \(α\) достижим по \(r\).

В Lean, достижимость представляет собой индуктивное семейство Acc, определённое следующим образом:

inductive Acc {α: Sort u}(r: α → α → Prop): α → Prop where
| intro (x: α)(h: (y: α) → r y x → Acc r y): Acc r x

Интуитивно, достижимость значения означает, что значение связано цепью отношений \(r\) с некоторым «наименьшим» значением \(y\), то есть со значением, для которого \(r\ y\ x\) ложно для любого \(z\).

Посмотрим теперь на рекурсор семейства типов Acc:

Acc.rec.{u, v}: {α: Sort v} → {r: α → α → Prop} →
  {motive: ∀a, Acc r a → Sort u} →
  (∀x, (h: ∀y, r y x → Acc r y) →
    (∀y, (a: r y x) → motive y (h y a)) →
    motive x (Acc.intro x h)) →
  {a: α} → (t: Acc r a) → motive a t

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

def wf_of_ind {r: α → α → Prop}(ind: Ind.{0} r): ∀x, Acc r x :=
  by reader

noncomputable def ind_of_wf {r: α → α → Prop}(wf: ∀x, Acc r x): Ind r :=
  λ{M} (h: ∀x, (∀y, r y x → M y) → M x) x ↦
    show M x from (wf x).recOn (λx _ (wh: ∀y, r y x → M y) ↦ h x wh)

Таким образом, каждое отношение является фундированным тогда и только тогда, когда оно индуктивно. В частности, отношение Nat.succRel является фундированным:

theorem acc_succ_rel: ∀n, Acc Nat.succRel n :=
  wf_of_ind indSuccRel

Полезно вычислить применение функции acc_succ_rel к некоторому конкретному значению. Вычислим acc_succ_rel 3:

#reduce acc_succ_rel 3
-- Acc.intro 3 fun k s =>
--   ((s ▸ Eq.refl k) ▸ Eq.refl k) ▸
--     Acc.intro 2 fun k s =>
--       ((s ▸ Eq.refl k) ▸ Eq.refl k) ▸
--         Acc.intro 1 fun k s =>
--           ((s ▸ Eq.refl k) ▸ Eq.refl k) ▸
--             Acc.intro 0 fun n s =>
--               False.rec
--                 (fun x => Acc (fun n k => n.succ = k) n)
--                 ((s ▸ fun h11 a => a (Eq.refl n)) s)

Термы (s ▸ Eq.refl k) ▸ Eq.refl k) в это выражении имеют типы 2 = k, 1 = k и 0 = k, что сводит результат функции типа (k: Nat) → Nat.succRel n k → Acc Nat.succRel n к единственному возможному значению для каждого k. Таким образом выражение по своей структуре повторяет терм Nat.succ (Nat.succ (Nat.succ Nat.zero)), что соответствует предназначению типа Acc: воспроизводить индуктивный тип по соответствующему отношению.

У нас всё готово для доказательства принципа сильной индукции. Нам потребуется небольшая лемма:

def Acc.inv {x y: α}(ax: Acc r x): r y x → Acc r y :=
  ax.recOn (λx (f: ∀y, r y x → Acc r y) _ ↦ f y)

С помощью которой мы докажем, что отношение «меньше или равно» на натуральных числах является фундированным:

def lt_wf (n: Nat): Acc Nat.lt n := by
  refine n.recOn (Acc.intro 0 ?_) ?_
  · intro y (h: y < 0)
    exact absurd h (not_succ_le_zero y)
  · intro n (an: Acc Nat.lt n)
    suffices ih: ∀m, m < n.succ → Acc Nat.lt m from Acc.intro n.succ ih
    intro m h
    have elt: m = n ∨ m < n := eq_or_lt_of_le (le_of_succ_le_succ h)
    exact elt.elim
      (λ(e: m = n) ↦ e.symm ▸ an)
      (λ(l: m < n) ↦ Acc.inv an l)

Поскольку фундированность равносильная индуктивности, отсюда непосредственно следует принцип сильной индукции.

В отличие от acc_succ_rel, терм, получающийся после применения функции lt_wf к конкретному значению велик и не нагляден. Полезно, однако, нарисовать дерево, соответствующее значению lt_wf 4:

../_images/lt-rel.svg

С помощью сильной индукции можно определять рекурсивные функции на натуральных числах. В качестве примера, определим функцию, результатом которой является остаток от деления числа на два, то есть 0 если число чётно, и 1 если нечётно.

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

def modTwoStep (n: Nat) (f: ∀k: Nat, k < n → Nat): Nat :=
  if h: n ≥ 2 then
    have: n - 2 + 1 ≤ n := sub_add_comm h ▸ sub_le n 1
    f (n - 2) this
  else n

И затем используем сильную индукцию чтобы получить требуемую функцию:

noncomputable
def modTwoFix: Nat → Nat :=
  ind_of_wf lt_wf modTwoStep

#reduce modTwoFix 3    -- 1

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

Пусть \(r\) это бинарное отношение на типе \(β\), а \(f\) это функция из типа \(α\) в тип \(β\). Будем называть отношение \(λx\,y.\; r\ (f\ x)\ (f\ y)\) на типе \(α\) прообразом \(r\) для функции \(f\). В Lean, прообраз отношения определён следующим образом:

def InvImage {α: Sort u}{β: Sort v}(r: β → β → Prop)(f: α → β): α → α → Prop :=
  λx y ↦ r (f x) (f y)

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

Для этого докажем вспомогательную лемму: пусть \(r\) это отношение на типе \(β\), и пусть \(f\) это функция из \(α\) в \(β\). Тогда, если \(f\ x\) достижимо по \(r\), то \(x\) достижимо по \(InvImage\ r\ f\):

def acc_invImage {x: α}(f: α → β)(acc: Acc r (f x)): Acc (InvImage r f) x := by
  suffices h: ∀y, Acc r y → ∀w, f w = y → Acc (InvImage r f) w
    from h (f x) acc x rfl
  refine λy (a: Acc r y) ↦ a.recOn ?_
  intro z _ (h: ∀y, r y z → ∀t, f t = y → Acc (InvImage r f) t)
  show ∀w, f w = z → Acc (InvImage r f) w
  intro w e
  suffices h: ∀t, r (f t) (f w) → Acc (InvImage r f) t
    from Acc.intro _ h
  exact λt ht ↦ h _ (e ▸ ht) t rfl

Из доказанного непосредственно следует, что прообраз фундированного отношения это фундированное отношение:

def wf_invImage (wf: ∀y: β, Acc r y)(f: α → β): ∀x: α, Acc (InvImage r f) x :=
  λx ↦ acc_invImage f (wf (f x))

Поскольку отношение «меньше или равно», определённое на натуральных числах, фундированно, любая функция из \(α\) в натуральные числа (которую будем называть мерой значений типа α) задаёт фундированное отношение на \(α\):

def wf_measure: (f: α → Nat) → ∀x: α, Acc (InvImage Nat.lt f) x :=
  wf_invImage lt_wf

Это позволяет определить индукцию по мере — обобщение сильной индукции для произвольного типа \(α\):

noncomputable example (m: α → Nat)(step: ∀x: α, (∀y: α, m y < m x → α) → α): α → α :=
  ind_of_wf (wf_measure m) step

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

def modTwo (n: Nat): Nat :=
  if h: n ≥ 2 then modTwo (n - 2)
  else n
termination_by n
decreasing_by
  simp_wf
  show n - 2 + 1 ≤ n
  exact sub_add_comm h ▸ sub_le n 1

Выражение после ключевого слова termination_by указывает меру, по которой ведётся индукция. Блок тактик после ключевого слова decreasing_by же доказывает, что шаг индукции уменьшает меру.

В доказательстве уменьшения меры, тактика simp_wf раскрывает связанные с индукцией определения в цели доказательства. Эту тактику можно опустить, если явно указать цель с помощью тактики show.

Определение функции modTwo не требует ключевого слова noncomputable, так как компилятор Lean понимает такую форму определения функций. По этой причине, использование такой формы определения предпочтительнее прямого использования функций вроде wf_measure.

Напоследок, докажем ещё один важный принцип, называемый принципом бесконечного спуска:

def inf_desc {r: α → α → Prop}(arx: Acc r x){p: α → Prop}
    (h: ∀x, p x → ∃y, r y x ∧ p y): p x → False :=
  arx.recOn (λx _ (ih: ∀y, r y x → p y → False) px ↦
    let ⟨y, ⟨ryx, py⟩⟩ := h x px
    ih y ryx py)

Согласно этому принципу, если для любого \(x\), из \(p\ x\) следует существование некоторого \(y\), такого, что \(r\ y\ x\) и \(p\ y\), то \(p\ x\) ложно для любого достижимого по \(r\) значения \(x\). Иначе говоря, если лестница вниз конечна, то спуск по ней не может потребовать бесконечного числа шагов.

Принцип бесконечного спуска для доказательств невозможности, связанных с натуральными числами. Например, с его помощью можно доказать, что у уравнений \(n^2 = 2 k^2\) и \(m^2 + n^2 = 3 k^2\) нет решений в положительных натуральных числах.

Мы готовы перейти к заключительной части этой главы — делению.

Деление и остаток#

Целочисленное деление на натуральных числах определено в Lean следующим образом:

def div_rec_lemma {n k: Nat}: (0 < k ∧ k ≤ n) → n - k < n :=
  λ⟨(pk: 0 < k), (kn: k ≤ n)⟩ ↦ sub_lt (le_trans pk kn) pk

def Nat.div (n k: Nat) : Nat :=
  if h: 0 < k ∧ k ≤ n then
    Nat.div (n - k) k + 1
  else
    0
termination_by n
decreasing_by exact div_rec_lemma h

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

def modCore (n k: Nat): Nat :=
  if h: 0 < k ∧ k ≤ n then
    modCore (n - k) k
  else
    n
termination_by n
decreasing_by exact div_rec_lemma h

def Nat.mod: Nat → Nat → Nat
| 0, _ => 0
| x, y => modCore x y

Эти функции определены даже тогда, когда второй аргумент равен нулю. Хотя результат деления на нуль как обращения умножения не имеет смысла, ничто не мешает определить соответствующее значения так, чтобы с функциями Nat.div и Nat.mod было удобно работать. Разумеется, свойства деления, связанные с обращением умножения, при этом требуют дополнительное условие, что делитель не равен нулю.

Функция Nat.mod определена через функцию modCore, хотя можно доказать, что результаты применения этих функций совпадают. Дополнительное сопоставление с образцом, вводимое функцией Nat.mod, нужно для того, чтобы Nat.mod 0 k было по определению равно нулю для любого k, тем самым не требуя использования соответствующей леммы.

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

theorem div_eq (n k: Nat): n / k = if 0 < k ∧ k ≤ n then (n - k) / k + 1 else 0 :=
  Nat.div_eq n k

theorem mod_eq (n k: Nat): n % k = if 0 < k ∧ k ≤ n then (n - k) % k else n :=
  Nat.mod_eq n k

Комбинируя эти леммы с функциями if_pos и if_neg, получаем ещё четыре леммы:

theorem div_eq_if_pos {n k: Nat}(h: 0 < k ∧ k ≤ n): n / k = (n - k) / k + 1 :=
  by rw [div_eq, if_pos h]

theorem div_eq_if_neg {n k: Nat}(h: ¬(0 < k ∧ k ≤ n)): n / k = 0 :=
  by rw [div_eq, if_neg h]

theorem mod_eq_if_pos {n k: Nat}(h: 0 < k ∧ k ≤ n): n % k = (n - k) % k :=
  by rw [mod_eq, if_pos h]

theorem mod_eq_if_neg {n k: Nat}(h: ¬(0 < k ∧ k ≤ n)): n % k = n :=
  by rw [mod_eq, if_neg h]

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

theorem mod_zero (n: Nat): n % 0 = n := by
  have: ¬(0 < 0 ∧ 0 ≤ n) := lt_irrefl 0 ∘ And.left
  rw [mod_eq_if_neg this]

Читатель же, пользуясь этими леммами, докажет следующее:

theorem mod_eq_of_lt {n k: Nat}(h: n < k): n % k = n := by reader
theorem mod_eq_sub_mod {n k: Nat}(h: n ≥ k): n % k = (n - k) % k := by reader
theorem mod_one (n: Nat): n % 1 = 0 := by reader
theorem zero_mod (n: Nat): 0 % n = 0 := by reader
theorem zero_div (n: Nat): 0 / n = 0 := by reader
theorem div_one (n: Nat): n / 1 = n := by reader

Замечание: высказывания вроде 0 < 1 можно доказать, используя тактику decide.

С любой рекурсивной функцией естественным образом связан некий принцип индукции. Сформулируем и докажем такой принцип для функций деления и взятия остатка:

def divmod_ind.{u}
    {motive: Nat → Nat → Sort u}
    (base: ∀n k, ¬(0 < k ∧ k ≤ n) → motive n k)
    (ind: ∀n k, 0 < k ∧ k ≤ n → motive (n - k) k → motive n k)
    (n k: Nat): motive n k :=
  if h: 0 < k ∧ k ≤ n then
    ind n k h (divmod_ind base ind (n - k) k)
  else
    base n k h
termination_by n
decreasing_by exact div_rec_lemma h

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

theorem mod_add_div (n k: Nat): n % k + k * (n / k) = n := by
  refine divmod_ind (motive := λn k ↦ n % k + k * (n / k) = n) ?_ ?_ n k
  · intro n k (h: ¬(0 < k ∧ k ≤ n))
    calc
      n % k + k * (n / k) = n + k * 0 := by rw [div_eq_if_neg h, mod_eq_if_neg h]
      _                   = n         := by rw [mul_zero, add_zero]
  · intro n k (h: 0 < k ∧ k ≤ n)
    intro (ih: (n - k) % k + k * ((n - k) / k) = n - k)
    calc
      n % k + k * (n / k) = (n - k) % k + k * ((n - k) / k + 1) :=
        by rw [div_eq_if_pos h, mod_eq_if_pos h]
      _ = (n - k) % k + k * ((n - k) / k) + k :=
        by simp only [add_assoc, mul_succ]
      _ = n :=
        by simp only [ih, sub_add_cancel h.right]

Поскольку Lean не удалось вывести мотив индукции, мы указываем его явно.

Из доказанного следует, что функции Nat.div и Nat.mod в самом деле ведут себе как деление и взятие остатка от деления — если мы докажем свойства этих функций, связанные со сложением и умножением.

Автор надеется, что читатель сможет их все доказать:

theorem add_div_right (n: Nat){k: Nat}(h: 0 < k): (n + k) / k = (n / k).succ := by reader
theorem add_mod_right (n k: Nat): (n + k) % k = n % k := by reader
theorem add_mod_left (n k: Nat): (k + n) % k = n % k := by reader
theorem add_mul_div_left (m n: Nat){k: Nat}(h: 0 < k): (m + k * n) / k = m / k + n := by reader
theorem mul_div_cancel (m: Nat){n: Nat}(h: 0 < n): m * n / n = m := by reader
theorem add_mul_mod_self_left (m n k: Nat): (m + k * n) % k = m % k := by reader
theorem add_mul_mod_self_right (m n k: Nat): (m + n * k) % k = m % k := by reader
theorem mul_mod_left (n k: Nat): n * k % k = 0 := by reader
theorem mul_mod_right (n k: Nat): k * n % k = 0 := by reader

Замечание: при доказательстве add_mod_right можно рассмотреть случаи, когда 0 = k и когда 0 < k.

В завершение, докажем некоторые важные свойства остатка от деления. Читатель докажет следующие две леммы:

theorem mod_lt (n: Nat){k: Nat}: 0 < k → n % k < k := by reader
theorem mod_mod (n k: Nat): n % k % k = n % k := by reader

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

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

theorem mul_mod_mul_left (m n k: Nat): m * n % (m * k) = m * (n % k) := by
  match m with
  | Nat.zero => simp only [zero_mul, mod_zero]
  | Nat.succ m =>
    refine divmod_ind
      (motive := λn k ↦ m.succ * n % (m.succ * k) = m.succ * (n % k)) ?_ ?_ n k
    · intro n k (h: ¬(0 < k ∧ k ≤ n))
      have: ¬(0 < m.succ * k ∧ m.succ * k ≤ m.succ * n) :=
        h ∘ (λ⟨msk, k_le_msn⟩ ↦
          ⟨pos_of_mul_pos_left msk,
          le_of_mul_le_mul_left (zero_lt_succ m) k_le_msn⟩)
      calc
        m.succ * n % (m.succ * k) = m.succ * n       := by rw [mod_eq_if_neg this]
        m.succ * n                = m.succ * (n % k) := by rw [mod_eq_if_neg h]
    · intro n k ⟨_, (yx: k ≤ n)⟩
      intro (h2: m.succ * (n - k) % (m.succ * k) = m.succ * ((n - k) % k))
      calc
        m.succ * n % (m.succ * k) = (m.succ * n - m.succ * k) % (m.succ * k) :=
          by rw [mod_eq_sub_mod (mul_le_mul_left _ yx)]
        _ = (m.succ * (n - k)) % (m.succ * k) :=
          by simp only [mul_sub_left_distrib]
        _ = m.succ * ((n - k) % k) := h2
        _ = m.succ * (n % k)       := by rw [←mod_eq_sub_mod yx]

Последние два свойства взятия остатка от деления снова докажет читатель:

theorem add_mod (m n k: Nat): (m + n) % k = (m % k + n % k) % k := by reader
theorem mul_mod (m n k: Nat): (m * n) % k = ((m % k) * (n % k)) % k := by reader

Доказательство этих свойств сводится к использованию леммы mod_add_div и последующим алгебраическим преобразованиям.

Где найти леммы?#

В Lean есть тактики для поиска лемм. Тактика exact? ищет лемму, закрывающую текущую цель, когда же тактика apply? ищет лемму, результатом применения которой является текущая цель. Тактика rw? ищет лемму, позволяющую переписать цель каким-либо образом.

Леммы также можно найти на сайте https://loogle.lean-lang.org/. Этот сайт ищет леммы не только среди лемм стандартной библиотеки Lean, но также и в Mathlib — одной из крупнейших библиотек компьютерных доказательств. Хотя эта книга не использует Mathlib, эта библиотека может быть весьма полезна в личных проектах.

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

1

На самом деле, конечно, в Principia Mathematica доказывается нечто другое. Подробнее на эту тему см. https://blog.plover.com/math/PM.html.

2

Автор нашёл это доказательство с помощью #reduce not_one_le_zero, когда эта лемма доказывалась с помощью exists_of_le.