Coq | |
---|---|
| |
Тип | Средство доказательства теорем |
Разработчик | INRIA; команда разработчиков |
Написана на | OCaml; C |
Операционная система | кроссплатформенность |
Первый выпуск | 1 мая 1989 года |
Аппаратная платформа | кросплатформенное |
Последняя версия | |
Состояние | активное |
Лицензия | LGPL 2.1 |
Сайт | coq.inria.fr |
Coq (фр. coq — петух) — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina)[2] с зависимыми типами. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ.
Coq разработан во Франции в рамках проекта TypiCal (ранее — LogiCal)[3], совместно управляемом INRIA, Политехнической школой, Университетом Париж-юг XI и Национальным центром научных исследований, ранее была выделенная группа и в Высшей нормальной школе Лиона.
Теоретической базой Coq считается исчисление конструкций; в названии скрыта его аббревиатура (CoC, англ. calculus of constructions) и сокращение от фамилии создателя исчисления — Тьерри Кокана.
Доказательство «на бумаге» ассоциативности композиции функций:
По транзитивности равенства:
Доказательство в 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.
Конструкторы и суть ноль и функция, возвращающая следующее число.
Необходимо доказать, что . Доказательство коммутативности в арифметике Пеано строится с помощью математической индукции по одному из множителей.
Будут использоваться обозначения, принятые в Coq, чтобы было легче сопоставить оба доказательства.
Выполним индукцию по .
База индукции: доказать . Высказывание следует из βδι-преобразования. доказывается отдельной леммой (см. Coq.Init.Peano.mult_n_O).
Шаг индукции: имея индуктивную гипотезу , доказать . Из βδι-преобразования следует . Имеется лемма (см. Coq.Init.Peano.mult_n_Sm), которая утверждает . Используем коммутативность сложения и индуктивную гипотезу.
Следующее доказательство скопировано с небольшими изменениями из стандартной библиотеки. Оно использует тактики.
Тактика автоматически генерирует доказательство (или его часть), опираясь на цель (что нужно доказать). Конечно, чтобы тактика сработала, должен существовать алгоритм поиска доказательства. В некоторых случаях тактики могут сильно уменьшить объём доказательства.
Чтобы использовать тактики, необходимо после 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
) проекции. Значение
из множества 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
генерирует все эти преобразования автоматически.
Для улучшения этой статьи желательно: |
Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".
Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.
Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .