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

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

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

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

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

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

В этой главе читатель будет доказывать простые теоремы про арифметические операции на натуральных числах, вроде того, что $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.

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

```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
```

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

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

```lean
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`, которую мы ранее использовали, просто применяет рекурсор:

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

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

```lean
inductive False: Prop
```

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

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

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

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

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

```lean
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
```

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

```lean
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 она определена следующим образом:

```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` это тождественная функция:

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

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

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

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

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

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

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

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

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

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

```lean
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, тип натуральных чисел определён следующим образом:

```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`, определённые следующим образом:

```lean
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 ...`. Вот пример его использования:

```lean
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 следующим образом:

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

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

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

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

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

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

```lean
#eval 2 + 3
```

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

```lean
#reduce λn ↦ n + 3
```

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

```lean
example: 1 + 1 = 2 := rfl
```

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

```lean
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 это доказательство выражается следующим образом:

```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)
```

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

```lean
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{aligned}
0 + n.succ &= (0 + n).succ  & &(add\_succ)\\
&= n.succ & &(\text{предположение индукции})
\end{aligned}$$

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

```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` позволяет соединить последовательность равенств. Общая форма этого выражения:

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

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

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

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

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

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

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

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

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

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

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

```
n : Nat
⊢ 0 + n = n
```

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

```lean
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
```

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

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

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

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

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

И закроем её:

```lean
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` чтобы ввести предположения:

```lean
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 помечает затенённую переменную символом `✝`.

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

```lean
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`:

```lean
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` чтобы переписать цель доказательства:

```lean
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` сама применяет её к требуемым значениям.

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

```lean
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`, чтобы заменить цель на вычислительно ей равную:

```lean
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`.

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

```lean
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
```

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

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

```lean
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]
```

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

```lean
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 позволяет доказать её ещё короче:

```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`.

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

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

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

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

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

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

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

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

```lean
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`. Она позволяет доказать, что нуль не следует ни за каким натуральным числом:

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

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

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

## Сравнения

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

```lean
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
```

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

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

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

```lean
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
```

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

```lean
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`:

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

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

```lean
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
```

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

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

```lean
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)
```

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

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

```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)
```

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

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

```lean
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` позволяет разбить сложную задачу на составляющие её простые части. Декомпозиция столь же важна в математике как и в программировании, без неё невозможно решать сложные задачи.

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

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

```lean
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
```

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

```lean
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`. Мы дали ей другое, более короткое имя.

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

```lean
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 это сделано следующим образом:

```lean
infix:50 " ≤ " => LE.le
```

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

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

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

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

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

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

```lean
#synth LE Nat    -- instLENat
```

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

```lean
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 также сводятся к соответствующим классам типов:

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

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

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

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

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

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

```lean
#synth HAdd Nat Nat Nat    -- instHAdd
```

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

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

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

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

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

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

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

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

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

```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` или ложно.

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

```lean
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)`:

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

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

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

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

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

```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` истинно. Доказательство:

```lean
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` позволяет доказывать высказывания вычислением:

```lean
example: 0 ≤ 2 := of_decide_eq_true rfl
```

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

```lean
example: 0 ≤ 2 := by decide
```

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

```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` записывается следующим образом:

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

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

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

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

```lean
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 также вводит следующую аксиому:

```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 определена следующим образом:

```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` повторяют определение:

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

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

```lean
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` является хорошим примером использования сопоставления с образцом. Рассмотрим его подробнее:

```lean
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 следит, чтобы были рассмотрены все возможности.

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

```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:

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

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

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

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

```lean
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`:

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

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

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

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

```lean
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`, без которого это доказательство не работает.

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

```lean
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`, связывающее каждое натуральное число с его предшественником:

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

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

```{figure} /_img/succ-rel.svg
```

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

```lean
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` индуктивно:

```lean
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`, определённое следующим образом:

```lean
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
```

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

```lean
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` является фундированным:

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

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

```lean
#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`: воспроизводить индуктивный тип по соответствующему отношению.

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

```lean
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)
```

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

```lean
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`:

```{figure} /_img/lt-rel.svg
```

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

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

```lean
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
```

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

```lean
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, прообраз отношения определён следующим образом:

```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$:

```lean
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
```

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

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

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

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

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

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

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

```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`.

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

```lean
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 следующим образом:

```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
```

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

```lean
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:

```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`, получаем ещё четыре леммы:

```lean
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]
```

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

```lean
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]
```

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

```lean
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`.

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

```lean
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
```

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

```lean
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` в самом деле ведут себе как деление и взятие остатка от деления — если мы докажем свойства этих функций, связанные со сложением и умножением.

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

```lean
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`.

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

```lean
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`.

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

```lean
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]
```

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

```lean
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](https://lean-lang.org/documentation/). В частности, там можно найти [список всех тактик](https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/), являющихся частью стандартной библиотеки Lean.

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

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