Coq — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina) с зависимыми типами.
Теоретической базой Coq считается исчисление конструкций; в названии скрыта его аббревиатура (CoC, англ. calculus of constructions) и сокращение от фамилии создателя исчисления — Тьерри Кокана. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать).
Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ. В новой версии была значительно доработана стандартная библиотека и документация, а также исправлен ряд ошибок.
Тактика автоматически генерирует доказательство (или его часть), опираясь на цель (что нужно доказать). Конечно, чтобы тактика сработала, должен существовать алгоритм поиска доказательства. В некоторых случаях тактики могут сильно уменьшить объём доказательства.
Чтобы использовать тактики, необходимо после Definition указать тип (цель, высказывание, которое нужно доказать), но опустить лямбда-терм, то есть само доказательство. Тогда Coq переходит в режим редактирования доказательства, где можно построить доказательство с помощью тактик.