Coq

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

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

Теоретической базой Coq считается исчисление конструкций.

Примеры

Ассоциативность композиции функций

Доказательство «на бумаге».

$(f \circ g) \circ h$

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

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

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

$f \circ (g \circ h)$

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

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

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

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

$(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.

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

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

Доказательство «на бумаге»

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

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

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

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

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

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

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

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

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

«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) проекции. Значение $i$ из множества int_bipart можно понимать как решение уравнения $x + (pneg~i) = (ppos~i)$, где $x$ — неизвестная величина. Если $(pneg~i) > (ppos~i)$, то решение является отрицательным числом.

Сложение в кольце определено как покомпонентное сложение, то есть 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.

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

$(pneg~n) \cdot (ppos~m) + (ppos~n) \cdot (pneg~m)$

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

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

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

$(pneg~n) \cdot (pneg~m) + (ppos~n) \cdot (ppos~m)$

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

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

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

Инструменты

• Язык реализации — 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». Список литературы можно найти в^[2], «Fixpoint definitions» и «Coinductive types».
  • Неявное приведение типов, или наследование (см.^[2], «Implicit Coercions»)
• Автоматический вывод типов
• Вывод значений аргументов из типов. Например, тип второго аргумента или результата функции $f$ зависит от значения первого аргумента (то есть функция $f$ имеет зависимый тип). Тогда значение первого аргумента можно вывести из типа второго аргумента или результата соответственно. Символ подчёркивания на месте аргумента указывает, что аргумент должен быть выведен автоматически. Если аргумент объявлен как неявный, его вообще можно опускать после имени функции (см.^[2], «Implicit arguments»). Coq может автоматически обнаруживать аргументы, которые имеет смысл объявить неявными
• Тактики можно писать на:
  • Языке программирования ML (см.^[2], «Building a toplevel extended with user tactics»)
  • Специальном языке для тактик Ltac (см.^[2], «The tactic language»)
  • Coq, используя тактику quote
• Имеет обширный набор примитивных тактик (например, intro, elim) и меньший набор развитых тактик для специфических теорий (например, field для поля, omega для арифметики Пресбургера)
• Тактики группы setoid для имитации фактормножеств: задаётся отношение эквивалентности; функции, сохраняющие это отношение; далее можно подставлять в термах эквивалентные (по вышеупомянутому отношению) значения
• Интегрированы классы типов а-ля-Haskell (начиная с версии 8.2).
• Program и Russel для создания верифицированных программ из неверифицированных (см.^[2], «Program»)

Библиотеки и приложения

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

Литература

1. ↑ http://logical.inria.fr/
2. ↑ ^{1 2 3 4 5 6} The Coq Development Team. The Coq Proof Assistant Reference Manual. Version 8.2.. Архивировано из первоисточника 27 марта 2012. Проверено 26 февраля 2009.  (англ.)

Ссылки

• The Coq proof assistant — официальный сайт Coq
• Cocorico!, the Coq Wiki — Кукареку!, вики по Coq