Coq
 | |
 | |
| Тип | Proof assistant |
|---|---|
| Розробник | The Coq development team |
| Перший випуск | 1 травня, 1989 (version 4.10) |
| Стабільний випуск | 8.10.2[1] (29 листопада, 2019) |
| Платформа | кросплатформова програма |
| Операційна система | 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
Жорж Гонтье (з 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».
- Неявне приведення типів, або спадкування
- Автоматичне виведення типів
- Виведення значень аргументів з типів
- Тактики можна писати на:
- Має великий набір примітивних тактик (наприклад, intro, elim) і менший набір розвинених тактик для специфічних теорій (наприклад, field для поля, omega для арифметики Пресбургер)
- Тактики групи setoid для імітації фактор-множин: задається відношення еквівалентності; функції, що зберігають це відношення; далі можна підставляти в термах еквівалентні (за вищезазначеною відношенню) значення
- Інтегровані класи типів (в стилі Haskell, починаючи з версії 8.2)
- Program і Russel для створення верифікованих програм з не верифікованих[6]
- 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».
