Coq: доказательство программ

Coq — интерактивный помощник доказательства, на котором проверяют теоремы и программы. Он основан на исчислении индуктивных конструкций с зависимыми типами: утверждение формулируется как тип, а доказательство — как терм этого типа, который проверяет ядро. Если ядро приняло терм, ошибки в доказательстве нет по построению. В 2025 году проект переименован в Rocq, но имя Coq по-прежнему широко используется в дистрибутивах, литературе и названиях библиотек. Разберём установку, первое доказательство, тактики, сборку проекта и извлечение кода.

Зачем это нужно на практике

Обычные тесты проверяют несколько примеров и не покрывают все входы. Coq позволяет доказать свойство для всех значений сразу: что сортировка возвращает перестановку входа, что компилятор сохраняет семантику, что протокол не выдаёт секрет. На нём построены проверенный компилятор CompCert, библиотеки математики Mathematical Components и криптографические реализации HACL*.

Порог входа высокий: нужно привыкнуть к зависимым типам и к тому, что доказательство — это программа. Зато результат не стареет: доказанное свойство остаётся верным, пока не изменились формулировка и аксиомы.

Установка

Проще всего поставить через opam — менеджер пакетов OCaml, на котором написан сам Coq. Отдельные пакеты есть в Debian, Ubuntu и Fedora, но версия в репозиториях часто отстаёт.

opam init
opam switch create coq-env ocaml-base-compiler.4.14.2
opam install coq coqide

Для работы в редакторе есть несколько вариантов: CoqIDE идёт в комплекте, Proof General работает в Emacs, VsCoq — расширение для VS Code, Coqtail — для Vim. Все они общаются с одним и тем же ядром, разница только в удобстве.

coqc --version
coqtop

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

Первое доказательство

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

Require Import Arith.
Require Import Lia.

Theorem plus_comm_example : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  lia.
Qed.

Тактика intros вводит переменные из цели, lia решает линейную арифметику. Для более сложных утверждений придётся разбирать структуру: induction по n, simpl для вычислений, rewrite для подстановки равенств.

Проверить, что доказательство принято, можно командой Print plus_comm_example. Coq покажет терм — иногда он выглядит устрашающе, но это нормально: терм строит машина, а не человек.

Тактики и структура доказательства

Доказательство в Coq — последовательность тактик между Proof и Qed. Qed проверяет терм и делает его непрозрачным; Defined оставляет тело видимым, что нужно, если доказательство потом вычисляется.

• intros — вводит предпосылки и переменные.
• apply — применяет гипотезу или лемму к цели.
• rewrite — заменяет подвыражение по равенству.
• induction и destruct — разбирают случаи и индукцию.
• simpl и compute — упрощают и вычисляют.
• split, exists, constructor — работают с конъюнкцией и кванторами.
• auto, lia, ring — автоматические решатели для своих областей.

Стиль имеет значение. Длинное доказательство без промежуточных утверждений трудно сопровождать; используйте assert или have, чтобы зафиксировать локальный факт с понятным именем.

Списки и индукция

Библиотека списков подключается из стандартной поставки. Нотации включаются отдельно, иначе квадратные скобки не разбираются.

From Coq Require Import List.
Import ListNotations.

Lemma app_nil_r : forall (A : Type) (xs : list A), xs ++ [] = xs.
Proof.
  intros A xs.
  induction xs as [| x rest IH].
  - reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.

Здесь видно типичный каркас: индукция даёт два случая, для пустого списка работает reflexivity, для шага — simpl и применение гипотезы индукции. Именно так доказывается большинство свойств рекурсивных функций.

Сборка проекта

Для одного файла хватает coqc, но проект из десятков файлов собирают через coq_makefile. Файл _CoqProject задаёт логические пути и порядок компиляции.

coq_makefile -f _CoqProject -o Makefile
make
make install

В _CoqProject указываются флаги -Q для привязки каталога к логическому имени и список файлов. Без -Q импорт между файлами не найдёт библиотеку, и вы получите ошибку «Cannot find library».

-Q src MyProject
src/Util.v
src/Main.v

Для непрерывной интеграции есть официальные Docker-образы; сборка в контейнере полезна, когда версия Coq должна совпадать у всех участников.

Извлечение кода

Одна из сильных сторон — извлечение проверенных функций в OCaml, Haskell или Scheme. Вы пишете и доказываете на Coq, а исполняемый код генерируется автоматически.

Require Import Extraction.
Extraction Language OCaml.
Extraction plus.

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

Отладка доказательств

Ошибки типов в Coq многословны, но информативны. Первое, что стоит сделать, — включить полную печать: Set Printing All показывает все неявные аргументы и нотации в развёрнутом виде.

• «Cannot find library» — проверьте флаги -Q и -R, порядок файлов в _CoqProject.
• «Expected a proof of…» — цель не совпала с тем, что вы применяете; смотрите на неявные аргументы.
• Тактика не срабатывает — проверьте, не раскрыто ли определение; поможет unfold или cbv.
• Доказательство долго проверяется — упростите терм, уберите compute и лишние simpl.

Команды Check, Print, Search и Locate экономят часы: Check показывает тип, Search ищет леммы по шаблону, Locate находит определение по имени. Show Proof выводит текущий терм доказательства.

Ограничения и здравый смысл

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

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

Итог

Coq, а теперь и Rocq, — инструмент для тех, кому нужна уверенность сильнее тестов. Он требует времени и аккуратности, зато даёт машинно проверяемое доказательство, которое не зависит от настроения ревьюера. Начните с opam, coqtop и простой теоремы о сложении, затем перейдите к спискам и сборке через coq_makefile. Извлечение кода в OCaml покажет, что формальная математика вполне пригодна для практических программ.