Пропозиции как типы на практике: Coq и Lean

От теории к инструментам: что значит «доказать на компьютере» и где это уже применяется всерьёз.

Пруверы на зависимых типах (Coq, Agda, Lean) — системы, где теорема — это тип, доказательство — терм этого типа, а доверять нужно лишь маленькому проверяющему ядру.

Как устроен прувер

В Coq/Lean утверждение записывается как тип, а доказательство строится как терм. Писать терм-доказательство руками тяжело, поэтому используют тактики — команды, пошагово конструирующие доказательство («примени это правило», «разбери случаи», «индукция по n»). Но ключевой принцип — малое доверенное ядро (de Bruijn criterion): какими бы умными ни были тактики, итоговый терм проверяет крошечный, многократно проаудированный type checker. Ошибка в тактике не пропустит ложную теорему — её отвергнет ядро.

Theorem and_comm : forall A B : Prop, A /\ B -> B /\ A.
Proof.
  intros A B H.        (* ввели гипотезы *)
  destruct H as [a b]. (* разобрали конъюнкцию *)
  split.               (* цель B /\ A -- две подцели *)
  - exact b.           (* B *)
  - exact a.           (* A *)
Qed.                   (* ядро проверило терм-доказательство *)

Этот скрипт строит ровно ту функцию-перестановку пары, что мы писали на Python в уроке про Карри — Говарда. Тактики — лишь удобный способ собрать терм; суть та же.

Что реально доказано

Это не упражнения. На пруверах получены результаты промышленного масштаба.

Демонстрация: «доказываем» индукцией на Python

Coq доказывает свойства всех натуральных чисел индукцией — конечным термом, а не перебором. Покажем структуру индуктивного доказательства «сумма 0..n = n(n+1)/2»: база плюс шаг. На Python мы лишь проверяем на примерах, но структура (база/шаг) — ровно та, что формализует прувер.

# свойство P(n): 0+1+...+n == n*(n+1)//2
def lhs(n): return sum(range(n + 1))
def rhs(n): return n * (n + 1) // 2

# база P(0) и шаг: если P(n), то P(n+1)
def base_holds():
    return lhs(0) == rhs(0)
def step_holds(n):
    # P(n+1) сводится к P(n) + (n+1)
    return (rhs(n) + (n + 1)) == rhs(n + 1)

print("база P(0)            :", base_holds())
print("шаг для n=0..4 верен :", all(step_holds(n) for n in range(5)))
print("проверка P(n) n=0..6 :", all(lhs(n) == rhs(n) for n in range(7)))
print("в Coq база+шаг => P(n) для ВСЕХ n (одним термом-доказательством)")

Вывод:

база P(0)            : True
шаг для n=0..4 верен : True
проверка P(n) n=0..6 : True
в Coq база+шаг => P(n) для ВСЕХ n (одним термом-доказательством)

Разница принципиальна: наш Python проверил конечное число n; индуктивное доказательство в Coq покрывает все натуральные числа сразу — это сила типов, а не тестов.

Как работает под капотом

Индукция в пруверах — это рекурсивная функция-доказательство по структуре индуктивного типа Nat = Zero | Succ Nat: база обрабатывает Zero, шаг — Succ n, используя доказательство для n. Чтобы такие рекурсивные доказательства были надёжны, прувер требует завершаемости (структурной убывающей рекурсии) — иначе незавершающийся «доказатель» доказал бы ложь. Это прямое следствие связи завершаемость = состоятельность логики.

Частые ошибки

• Считать тактики «доказательством». Доказательство — это терм; тактики лишь собирают его, а проверяет ядро.
• Доверять всему коду прувера. Доверять нужно только ядру; библиотеки тактик могут быть сколь угодно сложны.
• Путать «доказано» и «протестировано». Индукция покрывает все случаи; тест — конечное число.

Итоги

• В Coq/Lean теорема — тип, доказательство — терм; доверяем лишь малому ядру.
• Тактики пошагово собирают терм-доказательство, ядро его перепроверяет.
• Реальные результаты: CompCert, seL4, теорема о четырёх красках, mathlib.
• Индукция = рекурсивное доказательство с обязательной завершаемостью.