Coq

Coq
Тип	Средство доказательства теорем
Разработчики	INRIA; команда разработчиков
Написана на	OCaml; C
Операционная система	кроссплатформенность
Первый выпуск	1 мая 1989 года
Аппаратная платформа	кроссплатформенное
Последняя версия	8.20.0 (3 сентября 2024)[1]
Репозиторий	github.com/coq/coq
Читаемые форматы файлов: Coq file format[вд]
Создаваемые форматы файлов: Coq file format[вд]
Состояние	активное
Лицензия	LGPL 2.1
Сайт	coq.inria.fr
Медиафайлы на Викискладе

Coq (фр. coq — петух) — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina)^[2] с зависимыми типами. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ.

Coq разработан во Франции в рамках проекта TypiCal (ранее — LogiCal)^[3], совместно управляемом INRIA, Политехнической школой, Университетом Париж-юг XI и Национальным центром научных исследований, ранее была выделенная группа и в Высшей нормальной школе Лиона.

Теоретической базой Coq считается исчисление конструкций; в названии скрыта его аббревиатура (CoC, англ. calculus of constructions) и сокращение от фамилии создателя исчисления — Тьерри Кокана.

Coq можно использовать для вычислений. Пример вычисления факториала^[4]:

 Fixpoint factorial n := match n with
                         | 0 => 1
                         | (S n') => n * factorial n'
                         end.
 Compute factorial 5.

Здесь использована конструкция сопоставления с образцом, в частности, (S n') — это сопоставление с конструктором S, представляющим следующее натуральное число.

Доказательство «на бумаге» ассоциативности композиции функций:

${\displaystyle (f\circ g)\circ h}$

${\displaystyle =\lambda x.(f\circ g)(h~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.(\lambda y.f(g~y))(h~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.(f(g(h~x)))}$ ; β-эквивалентность

${\displaystyle f\circ (g\circ h)}$

${\displaystyle =\lambda x.f((g\circ h)~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.f((\lambda y.g(h~y))~x)}$ ; δ-эквивалентность

${\displaystyle =\lambda x.f(g(h~x))}$ ; β-эквивалентность

По транзитивности равенства:

${\displaystyle (f\circ g)\circ h=f\circ (g\circ h)}$

Доказательство в Coq:

  Definition cf := fun t0 t1 t2 : Type
    => fun (f : t1 -> t2) (g : t0 -> t1) => fun x => f (g x).
  Implicit Arguments cf [t0 t1 t2].
  Notation "f @ g" := (cf f g) (at level 65, left associativity).
  
  Definition cf_assoc := fun (t0 t1 t2 t3 : Type)
    (f : t2 -> t3) (g : t1 -> t2) (h : t0 -> t1)
    => (refl_equal _) : (f @ g) @ h = f @ (g @ h).

cf — определение композиции функций. Notation вводит инфиксное обозначение @ для композиции функций.

cf_assoc — собственно доказательство. Coq основан на изоморфизме Карри — Ховарда, поэтому доказательство есть терм лямбда-исчисления.

fun … => … в Coq обозначает лямбда-абстракцию. Функциям даются имена f, g, h, а их областям определения и областям значений даются имена t0, t1, t2, t3.

Кроме лямбда-абстракции доказательство состоит из refl_equal — аксиомы рефлексивности равенства. Нам нужно привести левую и правую части равенства с помощью βδ-редукций к одному выражению. Coq сам выполняет βδ-редукцию, поэтому доказательство практически пустое.

Чтобы понять роль refl_equal, выполните Check (refl_equal 2). Coq покажет автоматически выведенный тип этого терма, а именно, 2 = 2. Но в доказательстве cf_assoc аргумент refl_equal заменён на подчёркивание. Coq сам может вывести этот аргумент (см. «Вывод значений аргументов из типов»). Это сокращает объём доказательства. Выполнив Print cf_assoc., можно убедиться, что Coq вывел терм (f @ g) @ h вместо подчёркивания.

Тип натуральных чисел определён в стандартной библиотеке индуктивно:

  Inductive nat : Set :=
    | O : nat
    | S : nat -> nat.

Конструкторы ${\displaystyle O}$ и ${\displaystyle S}$ суть ноль и функция, возвращающая следующее число.

Необходимо доказать, что ${\displaystyle n\cdot m=m\cdot n}$. Доказательство коммутативности в арифметике Пеано строится с помощью математической индукции по одному из множителей.

Будут использоваться обозначения, принятые в Coq, чтобы было легче сопоставить оба доказательства.

Выполним индукцию по ${\displaystyle n}$.

База индукции: доказать ${\displaystyle O\cdot m=m\cdot O}$. Высказывание ${\displaystyle O\cdot m=O}$ следует из βδι-преобразования. ${\displaystyle O=m\cdot O}$ доказывается отдельной леммой (см. Coq.Init.Peano.mult_n_O).

Шаг индукции: имея индуктивную гипотезу ${\displaystyle n\cdot m=m\cdot n}$, доказать ${\displaystyle (S~n)\cdot m=m\cdot (S~n)}$. Из βδι-преобразования следует ${\displaystyle (S~n)\cdot m=m+n\cdot m}$. Имеется лемма (см. Coq.Init.Peano.mult_n_Sm), которая утверждает ${\displaystyle m\cdot n+m=m\cdot (S~n)}$. Используем коммутативность сложения и индуктивную гипотезу.

Следующее доказательство скопировано с небольшими изменениями из стандартной библиотеки. Оно использует тактики.

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

Чтобы использовать тактики, необходимо после Definition указать тип (цель, высказывание, которое нужно доказать), но опустить лямбда-терм, то есть само доказательство. Тогда Coq переходит в режим редактирования доказательства, где можно построить доказательство с помощью тактик.

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

Режим редактирования доказательства (англ. proof editing mode) не запрещает строить доказательство как лямбда-терм. Тактика refine (см. «#Коммутативность умножения в кольце Гротендика») доказать цель с помощью указанного после refine лябмда-терма. refine имеет следующую дополнительную возможность: если в лямбда-терме вместо некоторых подтермов стоит подчёркивание и Coq не может вывести значение подтермов автоматически, то это подчёркивание генерирует подцель. Таким образом, refine может генерировать произвольное количество подцелей.

  Require Import Coq.Arith.Plus.
  
  Definition mult_comm : forall n m, n * m = m * n.
  Proof.
  intros. elim n.
  auto with arith.
  intros. simpl in |- *. elim mult_n_Sm. elim H. apply plus_comm.
  Qed.

intros вводит предпосылки (n и m). elim применяет математическую индукцию, после чего цель доказательства разбивается на две подцели: база и шаг индукции. auto with arith доказывает базу индукции; тактика auto ищет простым перебором подходящую теорему в базе данных теорем и подставляет её в доказательство. В данном случае она находит лемму mult_n_O. В этом можно убедиться, выполнив Show Proof. При доказательстве шага индукции применяются леммы mult_n_Sm, plus_comm, и индуктивная гипотеза H. Имя индуктивной гипотезы было сгенерировано автоматически тактикой intros, второе вхождение тактики. simpl in |- * выполняет βδι-преобразование цели. Хотя она не генерирует доказательства, но она приводит цель к такому виду, который нужен для вывода аргументов тактикой apply plus_comm.

То же доказательство можно выразить лямбда-термом.

  Definition mult_comm := fun n:nat
  => fix rec (m : nat)
  : n * m = m * n
  := match m as m return n * m = m * n with
    | O => sym_eq (mult_n_O _)
    | S pm => match rec pm in _ = dep return _ = n + dep
      with refl_equal =>
        match mult_n_Sm _ _ in _ = dep return dep = _
        with refl_equal => plus_comm _ _ end
      end
    end.

elim n соответствует fix … match … as …. Остальные elim соответствуют match … in _=dep …. В доказательстве с помощью тактик нет нужды указывать конструкторы O и S, так как они выводятся из nat.

  Definition mult_comm := fun n:nat
  => nat_ind (fun m => n * m = m * n)
    (sym_eq (mult_n_O _))
    (fun _ rec =>
      eq_ind _ (fun dep => _ = n + dep)
      (eq_ind _ (fun dep => dep = _)
        (plus_comm _ _) _ (mult_n_Sm _ _))
      _ rec).

Это более компактная, хотя менее наглядная запись. nat_ind и eq_ind называются принципами индукции и являются функциями, сгенерированными согласно структуре индуктивных типов (nat, если nat_ind, и eq, если eq_ind). Тактики вставляют в доказательство именно эти функции.

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

Это пример использования специализированной тактики ring. Она выполняет преобразования формул, построенных из операций полукольца или кольца.

Кольцо Гротендика конструируется из полукольца следующим образом. int_bipart — носитель кольца — есть вторая декартова степень nat — носителя полукольца.

  Record int_bipart : Set := {pneg : nat; ppos : nat}.

Record не только конструирует декартово произведение множеств, но и генерирует левую (названа pneg) и правую (названа ppos) проекции. Значение ${\displaystyle i}$ из множества int_bipart можно понимать как решение уравнения ${\displaystyle x+(pneg~i)=(ppos~j)}$, где ${\displaystyle x}$ — неизвестная величина. Если ${\displaystyle (pneg~i)>(ppos~j)}$, то решение является отрицательным числом.

Сложение в кольце определено как покомпонентное сложение, то есть pneg левого слагаемого складывается с pneg правого слагаемого, ppos левого слагаемого складывается с ppos правого слагаемого.

  Notation "a !+ b" := (Peano.plus a b) (at level 50, left associativity).
  Definition plus a b := Build_int_bipart
    (pneg a !+ pneg b) (ppos a !+ ppos b).
  Notation "a + b" := (plus a b).

Мы обозначаем сложение в полукольце как «!+» и сложение в кольце как «+».

Умножение определяется так: в часть pneg (это первый аргумент Build_int_bipart) идут произведения разных компонент, в часть ppos (это второй аргумент Build_int_bipart) идут произведения одинаковых компонент.

  Notation "a !* b" := (Peano.mult a b) (at level 40, left associativity).
  Definition mult a b := Build_int_bipart
    (pneg a !* ppos b !+ ppos a !* pneg b)
    (pneg a !* pneg b !+ ppos a !* ppos b).
  Notation "a * b" := (mult a b) (at level 40, left associativity).

Мы обозначаем умножение в полукольце как «!*» и умножение в кольце как «*».

Сначала докажем лемму «если оба компонента int_bipart равны, то int_bipart равны».

  Definition int_bipart_eq_part
    : forall an bn, an = bn -> forall ap bp, ap = bp
    -> Build_int_bipart an ap = Build_int_bipart bn bp.
  Proof.
  refine (fun _ _ eqn _ _ eqp => _).
  refine (eq_ind _ (fun n => _ = Build_int_bipart n _) _ _ eqn).
  refine (f_equal _ eqp).
  Qed.

Теперь докажем коммутативность умножения в кольце, то есть n * m = m * n.

  Require Import ArithRing.
  
  Definition mult_comm : forall n m, n * m = m * n.
  Proof.
  refine (fun n m => int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
  Qed.

Нужно доказать равенство двух int_bipart. Лемма int_bipart_eq_part разбивает нашу цель на две подцели. Первая подцель есть равенство компонент pneg, вторая подцель есть равенство компонент ppos. Увидеть эти подцели можно, если сразу после Proof. выполнить refine (fun n m => int_bipart_eq_part _ _ _ _ _ _). «;» между refine и (simpl; ring) означает, что комбинированная тактика (simpl; ring) доказывает все подцели, генерируемые тактикой refine.

Чтобы доказать «на бумаге», нужно последовательно применить свойства операций полукольца:

${\displaystyle (pneg~n)\cdot (ppos~m)+(ppos~n)\cdot (pneg~m)}$

${\displaystyle =(ppos~m)\cdot (pneg~n)+(ppos~n)\cdot (pneg~m)}$ ; коммутативность умножения

${\displaystyle =(ppos~m)\cdot (pneg~n)+(pneg~m)\cdot (ppos~n)}$ ; коммутативность умножения

${\displaystyle =(pneg~m)\cdot (ppos~n)+(ppos~m)\cdot (pneg~n)}$ ; коммутативность сложения

${\displaystyle (pneg~n)\cdot (pneg~m)+(ppos~n)\cdot (ppos~m)}$

${\displaystyle =(pneg~m)\cdot (pneg~n)+(ppos~n)\cdot (ppos~m)}$ ; коммутативность умножения

${\displaystyle =(pneg~m)\cdot (pneg~n)+(ppos~m)\cdot (ppos~n)}$ ; коммутативность умножения

Тактика ring генерирует все эти преобразования автоматически.

Coq используется для большого количества работ в математике и информатике^[5]:

• В качестве платформы для моделирования языков программирования. Он использовался для проверки безопасности JavaCard и для формальных спецификаций, таких как x86, LLVM и C.
• Создание формально верифицированного программного обеспечения, включая компилятор CompCert для C и гипервизор CertiKOS. Он также применялся для разработки CertiCrypt и верифицированных реализаций архитектуры RISC-V с открытыми исходниками.
• В среде функционального программирования с зависимыми типами Coq стимулировал инновации, такие как внедрение «реляционных логических выводов Хоара» в системе Ynot.
• В качестве системы интерактивного доказательства для верификации ключевых математических результатов. С его помощью было создано доказательство теоремы о четырёх красках и теоремы Фейта — Томпсона.

• Язык реализации — OCaml и Си
• Лицензия — GNU Lesser General Public Licence Version 2.1
• Среды разработки:
  • Компилятор coqc и инструменты для работы с проектами, состоящими из множества файлов
  • coqtop — консольная интерактивная среда
  • Среды разработки с графическим интерфейсом пользователя:
    • CoqIDE
    • Eclipse Proof General
    • Режим для Emacs
• coqdoc — генератор документации к библиотекам, выход в LaTeX и HTML
• Экспорт доказательств в XML для проектов HELM1 и MoWGLI
• Конструктивная математика известна тем, что из доказательства существования величины можно экстрагировать алгоритм получения этой величины. Coq может экспортировать алгоритмы в языки ML и Haskell. Значения, имеющие тип, принадлежащий сорту Prop, не экстрагируются; обычно эти значения есть доказательства.
• Coq можно расширять, не ухудшая надёжности. Корректность проверки доказательств зависит от proof-checker, который есть небольшая часть от всего проекта. Он проверяет доказательства, сгенерированные тактиками, поэтому некорректная тактика не приводит к принятию доказательства с ошибкой. Таким образом, Coq следует принципу де Брёйна.

• Пользователь может вводить собственные аксиомы
• Основан на предикативном исчислении (ко)индуктивных конструкций, что означает:
  • Все возможности исчисления конструкций:
  • Кумулятивная иерархия универсумов, состоящая из Prop, Set и множества Type, индексированного натуральными числами
  • Prop импредикативный, Set и Type предикативные
  • Индуктивные или алгебраические типы данных
  • Коиндуктивные типы данных
  • Возможно задать только общерекурсивные функции, то есть такие функции, вычисление которых останавливается, то есть не зацикливается. В Coq можно записать функцию Аккермана. Остановка рекурсии по индуктивным типам данных (таким, как натуральные числа и списки) гарантируется синтаксической проверкой определения функции, называемой «guarded by destructors». Остановка функций, которые используют сопоставление с образцом коиндуктивных типов, гарантируется условием «guarded by contructors».
  • Неявное приведение типов, или наследование^[6]
• Автоматический вывод типов
• Вывод значений аргументов из типов. Например, тип второго аргумента или результата функции ${\displaystyle f}$ зависит от значения первого аргумента (то есть функция ${\displaystyle f}$ имеет зависимый тип). Тогда значение первого аргумента можно вывести из типа второго аргумента или результата соответственно. Символ подчёркивания на месте аргумента указывает, что аргумент должен быть выведен автоматически. Если аргумент объявлен как неявный, его вообще можно опускать после имени функции^[7]. Coq может автоматически обнаруживать аргументы, которые имеет смысл объявить неявными
• Тактики можно писать на:
  • Языке программирования ML^[8]
  • Специальном языке для тактик Ltac^[9]
  • Coq, используя тактику quote
• Имеет обширный набор примитивных тактик (например, intro, elim) и меньший набор развитых тактик для специфических теорий (например, field для поля, omega для арифметики Пресбургера)
• Тактики группы setoid для имитации фактормножеств: задаётся отношение эквивалентности; функции, сохраняющие это отношение; далее можно подставлять в термах эквивалентные (по вышеупомянутому отношению) значения
• Интегрированы классы типов (в стиле Haskell, начиная с версии 8.2).
• Program и Russel для создания верифицированных программ из неверифицированных^[10]

• Формализация различных разделов математики:
  • Общая алгебра
  • Арифметика и теория чисел
  • Геометрия
  • Комбинаторика
  • Лямбда-исчисление
  • Математическая логика, включая само исчисление конструкций и Pure Type Systems
  • Математический анализ
  • Теория графов, включая доказательство существования решения проблемы четырёх красок — «доказательство практически невозможно проверить, не используя компьютер»
  • Теория категорий
  • Теория множеств, классическая и интуиционистская
  • Формальные языки и автоматы
• Информатика:
  • Семантика языков программирования
  • Корректность алгоритмов RSA, алгоритма Хаффмана и других
  • Параллельные системы и протоколы
  • Логические игры
• Верификация программ:
  • Why — платформа для верификации программ, которая используется в:
    • Krakatoa — инструмент для верификации программ на языках программирования Java и Java Card, аннотированных с помощью Java Modeling Language^[англ.]
    • Frama-C^[англ.] — инструмент для верификации программ на Си
  • Ynot^[11] — библиотека для верификации императивных программ. Использует развитие монады IO (из Haskell), логику Хоара, сепарационную логику
  • Coq может использоваться^[12] в качестве альтернативной системы доказательства в инструменте GNATprove, используемом для формальной верификации программ на языке SPARK (диалекте Ады)

• Bertot, Y. and Pierre Castéran, P. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. — Springer, 2004. — ISBN 9783540208549.
• Henri Habrias, Marc Frappier. Chapter 16. Coq // Software Specification Methods. — John Wiley & Sons, 2006. — 418 p. — ISBN 978-1-905-20934-7.
• Chlipala, A. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. — MIT Press, 2013. — 440 p. — ISBN 9780262026659. — доступное изложение применения Coq в доказательном программировании
• Ilya Sergey. Programs and Proofs: Mechanizing Mathematics with Dependent Types. — 2014. — (Lecture Notes).

• The Coq proof assistant Архивная копия от 25 августа 2004 на Wayback Machine — официальный сайт Coq
• Cocorico!, the Coq Wiki Архивная копия от 21 июля 2011 на Wayback Machine — Кукареку!, вики по Coq
• The Coq Development Team. The Coq Proof Assistant Reference Manual. Version 8.2.  (неопр.) Дата обращения: 26 февраля 2009. Архивировано из оригинала 26 марта 2012 года.