23-10-2023
В информатике Coq есть доказатель теорем, использующий собственный язык функционального программирования (Gallina) с зависимыми типами. Он позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ.
Coq разработан во TypiCal (англ.) (ранее LogiCal), совместно управляемом Paris-Sud 11 University (англ.) и École Normale Supérieure de Lyon (англ.).
Название «coq» на французском означает «петух». Оно следует французской традиции именовать исследовательские проекты названиями животных. Название также намекает на Thierry Coquand, который разработал исчисление конструкций вместе с Gérard Huet. Исчисление конструкций является теоретической базой Coq.
Содержание |
Доказательство «на бумаге».
; δ-эквивалентность
; δ-эквивалентность
; δ-эквивалентность
; δ-эквивалентность
; β-эквивалентность
По транзитивности равенства
Доказательство в 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», где можно построить доказательство с помощью тактик.
Если тактика смогла полностью доказать цель, она генерирует ноль подцелей. Если тактика не смогла довести доказательство до конца, хотя и выполнила некоторые шаги, то тактика генерирует ненулевое количество подцелей. Чтобы завершить доказательство, нужно доказать подцели с помощью других тактик. Таким образом можно комбинировать разные тактики.
«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
генерирует все эти преобразования автоматически.
Coq.