Rocq

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

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

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

Примеры

Вычисления Средство можно использовать для вычислений. Пример вычисления факториала: Fixpoint factorial n := match n with | 0 => 1 | (S n') => n * factorial n' end. Compute factorial 5. Здесь использована конструкция сопоставления с образцом, в частности, (S n') — это сопоставление с конструктором S, представляющим следующее натуральное число.

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

; δ-эквивалентность ; δ-эквивалентность ; β-эквивалентность

; δ-эквивалентность ; δ-эквивалентность ; β-эквивалентность

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

Доказательство в Rocq: 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. Конструкторы и суть ноль и функция, возвращающая следующее число.

Необходимо доказать, что . Доказательство коммутативности в арифметике Пеано строится с помощью математической индукции по одному из множителей.

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

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

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

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

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

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

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

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

Режим редактирования доказательства () не запрещает строить доказательство как лямбда-терм. Тактика 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) проекции. Значение из множества int_bipart можно понимать как решение уравнения , где  — неизвестная величина. Если , то решение является отрицательным числом.

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

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

; коммутативность умножения ; коммутативность умножения ; коммутативность сложения

; коммутативность умножения ; коммутативность умножения

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

Применения Система используется для большого количества работ в математике и информатике . В качестве платформы для моделирования языков программирования применялась для проверки безопасности JavaCard и для формальных спецификаций, таких как x86, LLVM и Си. Использовалась для создания формально верифицированного программного обеспечения, в том числе компилятора CompCert для Си и гипервизора CertiKOS, применялась для разработки CertiCrypt и верифицированных реализаций архитектуры RISC-V с открытыми исходными кодами.

В среде функционального программирования с зависимыми типами система стимулировала инновации, такие как внедрение «реляционных логических выводов Хоара» в системе Ynot.

С помощью системы было создано доказательство теоремы о четырёх красках и теоремы Фейта — Томпсона.

Инструменты Язык реализации — OCaml и Си. Лицензия — GNU Lesser General Public Licence Version 2.1.

Система включает следующие средства разработки: компилятор coqc и инструменты для работы с проектами, состоящими из множества файлов; coqtop — консольную интерактивную среду; coqdoc — генератор документации к библиотекам, выход в LaTeX и HTML среду разработки с графическим интерфейсом пользователя CoqIDE.