Coq

Coq (software)
Тип	Proof assistant
Розробник	The Coq development team
Перший випуск	1 травня, 1989; 34 роки тому (version 4.10)
Стабільний випуск	8.10.2 (29 листопада, 2019; 4 роки тому)
Платформа	кросплатформова програма
Операційна система	Cross-platform
Мова програмування	OCaml
Доступні мови	English
Ліцензія	LGPLv2.1
Репозиторій	github.com/coq/coq
Вебсайт	coq.inria.fr
	Медіафайли у Вікісховищі;

Coq (фр. coq — півень) — інтерактивний програмний засіб доведення теорем, використовує власну мову функціонального програмування (Gallina)^[2] з залежними типами. Дозволяє записувати математичні теореми і їхні доведення, починаючи з цілі (гіпотези, яку потрібно довести). Coq може автоматично знаходити доведення в деяких обмежених теоріях за допомогою тактик. Coq використовується для верифікації програм.

Історія розробки[ред. | ред. код]

Coq розроблений у Франції в рамках проекту TypiCal (раніше — LogiCal), спільно керується INRIA [Архівовано 26 лютого 2009 у Wayback Machine.], Політехнічною школою, Університетом Париж-Південь XI і Національним центром наукових досліджень, раніше була виділена група і в Вищій школі Ліона.

Теоретичною базою Coq є числення конструкцій; а назва — це абревіатура (CoC, англ. calculus of constructions) і скорочення прізвища творця обчислення — Тьєррі Кокана.

У 2013 році асоціація обчислювальної техніки нагородила Тьєррі Кокана, Жерар П'єр Хуета, Крістін Пауліна-Морінга, Бруно Барраса та інших премією ACM Software System Award за Coq.

Особливості програмного забезпечення[ред. | ред. код]

Coq дозволяє:

маніпулювати твердженнями обчислення
механічно перевіряти докази цих тверджень
сприяти пошуку формальних доведень
синтезувати сертифіковані програми на основі конструктивного підтвердження їх специфікацій

Нещодавно^[коли?] Coq удосконалили все більшими можливостями автоматизації. До них належить тактика Омега, яка визначає арифметику Пресбургера.

Це безкоштовне програмне забезпечення, яке розповсюджується на умовах ліцензії GNU LGPL.

Використання[ред. | ред. код]

Серед великих успіхів Coq можна відзначити:^{[джерело?]}

Проблема чотирьох фарб: була повністю механізована, демонстрація була завершена в 2005 році Жоржем Гонтьє та Бенджаміном Вернером
Система неперетинних множин: доказ коректності у Coq був опублікований у 2007 році.
Теорема Фейта-Томпсона: доказ теореми був завершений Жоржем Гонтьє та його командою у вересні 2012 року
CompCert: компілятор, оптимізований для мови програмування C, який значною мірою запрограмований та перевірений у Coq

Проблема чотирьох фарб та розширення Ssreflect [ред. | ред. код]

Жорж Гонтье (з Microsoft Research, в Кембриджі , Англія) і Бенджамін Вернер (з INRIA) використовуючи Coq довели теорему про Проблему чотирьох фарб.

На основі цієї роботи було розроблено значне розширення Coq під назвою Ssreflect (що означає «відображення в малих масштабах»). Більшість нових функцій, доданих в Ssreflect, є загальноприйнятими функціями, корисними не просто для стилю обчислювального відображення доведення. До них належать:

Додаткові зручні позначення для неспростовного та спростовуваного узгодження шаблону на індуктивних типах з одним або двома конструкторами
Неявні аргументи для функцій, застосованих до нульових аргументів — що корисно при програмуванні з функціями вищого порядку
Стислі анонімні аргументи
Вдосконалена setтактика з більш потужним узгодженням
Підтримка роздумів

Ssreflect 1.4 є у вільному доступі з подвійною ліцензією за ліцензією CeCILL-B або CeCILL-2.0 з відкритим кодом та сумісний з Coq 8.4.

Інше[ред. | ред. код]

До користувачів системи Coq належав Володимир Воєводський, лауреат медалі Філдса.^[3]

Інструменти[ред. | ред. код]

Мова реалізації — 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».
- Неявне приведення типів, або спадкування

Автоматичне виведення типів

Виведення значень аргументів з типів
Тактики можна писати на:
- Мові програмування ML^[4]
- Спеціальній мові для тактик Ltac ^[5]
- Coq, використовуючи тактику quote
Має великий набір примітивних тактик (наприклад, intro, elim) і менший набір розвинених тактик для специфічних теорій (наприклад, field для поля, omega для арифметики Пресбургер)
Тактики групи setoid для імітації фактор-множин: задається відношення еквівалентності; функції, що зберігають це відношення; далі можна підставляти в термах еквівалентні (за вищезазначеною відношенню) значення
Інтегровані класи типів (в стилі Haskell, починаючи з версії 8.2)
Program і Russel для створення верифікованих програм з не верифікованих^[6]

Див. також[ред. | ред. код]

Lean

Посилання[ред. | ред. код]

The Coq proof assistant [Архівовано 25 серпня 2004 у Wayback Machine.] — офіційний англійський вебсайт
coq/coq [Архівовано 31 грудня 2019 у Wayback Machine.] — сховище коду на GitHub
JsCoq Interactive Online System [Архівовано 14 жовтня 2019 у Wayback Machine.] — дозволяє запускати Coq у веббраузері без необхідності будь-якої інсталяції програмного забезпечення
Coq Wiki [Архівовано 24 грудня 2019 у Wayback Machine.]
Mathematical Components library [Архівовано 21 листопада 2019 у Wayback Machine.] –широко використовувана бібліотека математичних структур, частиною якої є мова Ssreflect
Constructive Coq Repository at Nijmegen [Архівовано 2 жовтня 2011 у Wayback Machine.]
Math Classes [Архівовано 1 січня 2019 у Wayback Machine.]

Підручники:

The Coq'Art [Архівовано 24 вересня 2019 у Wayback Machine.] — книга про Coq Іва Бертота та П'єра Кастерана
Certified Programming with Dependent Types [Архівовано 9 вересня 2011 у Wayback Machine.] — онлайн та друкований підручник Адама Чліпала
Software Foundations [Архівовано 9 листопада 2013 у Wayback Machine.] — онлайн-підручник Бенджаміна К. Пірса та ін.
An introduction to small scale reflection in Coq [Архівовано 23 лютого 2020 у Wayback Machine.] — навчальний посібник з SSreflect Жоржа Гонтьє та Ассіа Махбубі

Introduction to the Coq Proof Assistant [Архівовано 4 грудня 2019 у Wayback Machine.] — відео лекція Ендрю Апеля в Інституті підвищення кваліфікації
Video tutorials for the Coq proof assistant [Архівовано 4 грудня 2019 у Wayback Machine.] від Андрея Бауера

Джерела[ред. | ред. код]

↑ Coq 8.10.2 is out. 29 листопада 2019. Архів оригіналу за 31 грудня 2019. Процитовано 30 листопада 2019.
↑ Adam Chlipala. Library Universes (англ.). Архів оригіналу за 2 січня 2014. Процитовано 3 грудня 2019.
↑ Hartnett, Kevin (19 травня 2015). Will Computers Redefine the Roots of Math?. Quanta Magazine.
↑ Manual, 2009, «Building a toplevel extended with user tactics».
↑ Manual, 2009, «The tactic language».
↑ Manual, 2009, «Program».

[1] Coq 8.10.2 is out. 29 листопада 2019. Архів оригіналу за 31 грудня 2019. Процитовано 30 листопада 2019.

[Chlipala2013-2] Adam Chlipala. Library Universes (англ.). Архів оригіналу за 2 січня 2014. Процитовано 3 грудня 2019.

[3] Hartnett, Kevin (19 травня 2015). Will Computers Redefine the Roots of Math?. Quanta Magazine.

[FOOTNOTEManual2009«Building_a_toplevel_extended_with_user_tactics»-4] Manual, 2009, «Building a toplevel extended with user tactics».

[FOOTNOTEManual2009«The_tactic_language»-5] Manual, 2009, «The tactic language».

[FOOTNOTEManual2009«Program»-6] Manual, 2009, «Program».

[1]

[2]

[3]

[4]

[5]

[6]

Coq