Coq (программное обеспечение)
Помощник по проверке

Coq (программное обеспечение)
Оригинальный автор(ы)Тьерри Коканд , Жерар Юэ , Кристин Полен-Морен , Брюно Баррас, Жан-Кристоф Филлиатр, Уго Эрбелен, Четан Мюрти, Ив Берто, Пьер Кастеран
Разработчик(и)INRIA , Политехническая школа , Университет Париж-Юг , Парижский университет Дидро , CNRS , ENS Lyon
Первоначальный выпуск1 мая 1989 г .; 35 лет назад (версия 4.10) ( 1989-05-01 )
Стабильный релиз
8.20.0 [1]  / 3 сентября 2024 г. ; 5 месяцев назад ( 3 сентября 2024 г. )
Репозиторийgithub.com/coq/coq
Написано вOCaml
Операционная системаКроссплатформенный
Доступно вАнглийский
ТипПомощник по проверке
ЛицензияLGPLv2.1
Веб-сайтcoq.inria.fr
Интерактивный сеанс проверки в CoqIDE, показывающий скрипт проверки слева и состояние проверки справа.

Coq — интерактивный доказатель теорем, впервые выпущенный в 1989 году. Он позволяет выражать математические утверждения, механически проверять доказательства этих утверждений, помогает находить формальные доказательства и извлекать сертифицированную программу из конструктивного доказательства ее формальной спецификации . Coq работает в рамках теории исчисления индуктивных конструкций , производной от исчисления конструкций . Coq не является автоматизированным доказательством теорем , но включает в себя тактики ( процедуры ) автоматического доказательства теорем и различные процедуры принятия решений .

Ассоциация вычислительной техники наградила Тьерри Коканда , Жерара Юэ , Кристин Полен-Моринг , Бруно Барраса, Жана-Кристофа Филлиатра, Уго Эрбелена, Шетана Мурти, Ива Берто и Пьера Кастерана премией ACM Software System Award 2013 за Coq.

Название Coq представляет собой игру слов на основе имени Тьерри Коканда, исчисления конструкций или CoC , и следует французской традиции в области компьютерных наук называть программное обеспечение в честь животных ( coq по-французски означает «петух»). [2] 11 октября 2023 года команда разработчиков объявила, что в ближайшие месяцы Coq будет переименован в The Rocq Prover , и начала обновлять кодовую базу, веб-сайт и связанные с ними инструменты. [3]

Обзор

Если рассматривать Coq как язык программирования , он реализует зависимо типизированную функциональную модель программирования ; [4] если рассматривать его как логическую систему, он реализует теорию типов более высокого порядка . Разработка Coq поддерживалась с 1984 года Французским институтом исследований в области компьютерных наук и автоматизации (INRIA), в настоящее время в сотрудничестве с École Polytechnique , Университетом Париж-Юг , Университетом Париж Дидро и Французским национальным центром научных исследований (CNRS). В 1990-х годах École normale supérieure de Lyon (ENS Lyon) также была частью проекта. Разработка Coq была инициирована Жераром Юэ и Тьерри Коканом, и более 40 человек, в основном исследователей, внесли свой вклад в основную систему с момента ее создания. Группу внедрения последовательно координировали Жерар Юэ, Кристин Полен-Моринг, Хьюго Эрбелен и Матье Созо. Coq в основном реализован на OCaml с небольшим добавлением C. Базовая система может быть расширена с помощью механизма подключаемых модулей . [5]

Название coq означает « петух » на французском языке и происходит от французской традиции называть инструменты для разработки исследований в честь животных. [6] До 1991 года Coquand реализовывал язык, называемый исчислением конструкций , и тогда он назывался просто CoC . В 1991 году была начата новая реализация, основанная на расширенном исчислении индуктивных конструкций , и название было изменено с CoC на Coq в косвенной ссылке на Coquand, который разработал исчисление конструкций вместе с Жераром Юэ и внес вклад в исчисление индуктивных конструкций вместе с Кристиной Полин-Мёринг. [7]

Coq предоставляет язык спецификаций, называемый Gallina [8] (« hen » на латыни, испанском, итальянском и каталонском). Программы, написанные на Gallina, обладают свойством слабой нормализации , подразумевающим, что они всегда завершаются. Это отличительное свойство языка, поскольку бесконечные циклы (незавершающиеся программы) распространены в других языках программирования [9] и являются одним из способов избежать проблемы остановки .

В качестве примера рассмотрим доказательство леммы о том, что взятие следующего элемента натурального числа меняет его четность. Тактика сворачивания-разворачивания, введенная Дэнви [10], используется для упрощения доказательства.

Ltac  fold_unfold_tactic  имя  :=  вступления ;  имя разворачивания  ; имя сворачивания ; рефлексивность .   Требуется  импорт  Arith  Nat  Bool .Fixpoint  is_even  ( n  :  nat )  :  bool  :=  match  n  with  |  0  =>  true  |  S  n'  =>  eqb  ( is_even  n' )  false  end .Лемма  fold_unfold_is_even_0 :  is_even  0  =  true .Доказательство .  Тактика_сложения_раскрытия  является_четной . Вопрос .Лемма  fold_unfold_is_even_S :  forall  n'  :  nat ,  is_even  ( S  n' )  =  eqb  ( is_even  n' )  false .Доказательство .  Тактика_сложения_раскрытия  является_четной . Вопрос .Лемма  successor_flips_evenness :  forall  n  :  nat ,  is_even  n  =  negb  ( is_even  ( S  n )).Доказательство .  Введение  . Переписать -> ( fold_unfold_is_even_S n ). Разрушить ( is_even  n ) .       *  простая рефлексивность  .​ *  просто рефлексивность . Вопрос .​

Известные применения

Теорема о четырех цветах и ​​расширение SSReflect

Жорж Гонтье из Microsoft Research в Кембридже , Англия , и Бенджамин Вернер из INRIA использовали Coq для создания обзорного доказательства теоремы о четырех цветах , которое было завершено в 2002 году. [11] Их работа привела к разработке пакета SSReflect («Small Scale Reflection»), который стал значительным расширением Coq. [12] Несмотря на свое название, большинство функций, добавленных в Coq с помощью SSReflect, являются функциями общего назначения и не ограничиваются вычислительно- рефлексивным стилем программирования доказательства. Эти функции включают в себя:

  • Добавлены удобные обозначения для неопровержимого и опровержимого сопоставления с образцом для индуктивных типов с одним или двумя конструкторами.
  • Неявные аргументы для функций, применяемых к нулевым аргументам, что полезно при программировании с использованием функций высшего порядка.
  • Краткие анонимные аргументы
  • Улучшенная setтактика с более мощным подбором
  • Поддержка размышлений

SSReflect 1.11 распространяется бесплатно, имеет двойную лицензию с открытым исходным кодом CeCILL-B или CeCILL-2.0 и совместим с Coq 8.11. [13]

Другие приложения

  • CompCert : оптимизирующий компилятор практически для всего языка программирования C , большая часть которого запрограммирована и корректно работает в Coq.
  • Структура данных непересекающихся множеств : доказательство корректности в Coq было опубликовано в 2007 году. [14]
  • Теорема Фейта–Томпсона : формальное доказательство с использованием Coq было завершено в сентябре 2012 года. [15]
  • Занятой бобр : ценность занятого бобра, победившего в 5 штатах, была обнаружена Хайнером Марксеном и Юргеном Бантроком в 1989 году, но была доказана только победившим пятым занятым бобром — стилизованным как BB(5) — в 2024 году с использованием доказательства в Coq. [16] [17]

Тактический язык

В дополнение к явному построению терминов Gallina, Coq поддерживает использование тактик, написанных на встроенном языке Ltac или OCaml. Эти тактики автоматизируют построение доказательств, выполняя тривиальные или очевидные шаги в доказательствах. [18] Несколько тактик реализуют процедуры принятия решений для различных теорий. Например, тактика «кольцо» решает теорию равенства по модулю аксиом кольца или полукольца с помощью ассоциативно - коммутативной перезаписи. [19] Например, следующее доказательство устанавливает сложное равенство в кольце целых чисел всего за одну строку доказательства: [20]

Требуется  импорт  ZArith . Открыть  область действия  Z_scope . Цель  для всех  a  b  c : Z ,  ( a  +  b  +  c )  ^  2  =  a  *  a  +  b  ^  2  +  c  *  c  +  2  *  a  *  b  +  2  *  a  *  c  +  2  *  b  *  c .  вступления ;  кольцо . Вопрос .

Встроенные процедуры принятия решений также доступны для пустой теории («конгруэнтность»), пропозициональной логики («тауто»), линейной целочисленной арифметики без кванторов («lia») и линейной рациональной/вещественной арифметики («lra»). [21] [22] Дальнейшие процедуры принятия решений были разработаны в виде библиотек, включая одну для алгебр Клини [23] и другую для определенных геометрических целей. [24]

Смотрите также

Ссылки

  1. ^ "Выпуск Coq 8.20.0". 3 сентября 2024 г.
  2. ^ "Альтернативные названия · coq/coq Wiki". GitHub . Получено 3 марта 2023 г.
  3. ^ "Coq roadmap 069". GitHub .
  4. ^ Краткое введение в Coq
  5. ^ Авигад, Джереми; Махбуби, Ассия (3 июля 2018 г.). Интерактивное доказательство теорем: 9-я международная конференция, ITP 2018, проводившаяся как ... Springer. ISBN 9783319948218. Получено 21 октября 2018 г.
  6. ^ "Часто задаваемые вопросы". GitHub . Получено 8 мая 2019 г.
  7. ^ "Введение в исчисление индуктивных построений" . Получено 21 мая 2019 г.
  8. ^ Адам Члипала. «Сертифицированное программирование с зависимыми типами»: «Библиотечные вселенные».
  9. ^ Адам Члипала. «Сертифицированное программирование с зависимыми типами»: «Library GeneralRec». «Library InductiveTypes».
  10. ^ Дэнви, Оливье (2022). «Сворачивание-разворачивание лемм для рассуждений о рекурсивных программах с использованием помощника доказательства Coq». Журнал функционального программирования . 32. doi : 10.1017/S0956796822000107 . ISSN  0956-7968.
  11. ^ Гонтье, Жорж (2008). «Формальное доказательство — теорема о четырех цветах» (PDF) . Notices of the American Mathematical Society . 55 (11): 1382– 1393. MR  2463991.
  12. ^ Гонтье, Жорж; Махбуби, Ассия (2010). «Введение в мелкомасштабное отражение в Coq». Журнал формализованных рассуждений . 3 (2): 95– 152. doi :10.6092/ISSN.1972-5787/1979.
  13. ^ "Библиотека математических компонентов 1.11.0". GitHub .
  14. ^ Conchon, Sylvain; Filliâtre, Jean-Christophe (2007). "Постоянная структура данных union-find". В Russo, Claudio V.; Dreyer, Derek (ред.). Труды семинара ACM по машинному обучению, 2007, Фрайбург, Германия, 5 октября 2007 г. Ассоциация вычислительной техники. стр.  37–46 . doi :10.1145/1292535.1292541. ISBN 978-1-59593-676-9.
  15. ^ "Теорема Фейта-Томпсона полностью проверена в Coq". Msr-inria.inria.fr. 20 сентября 2012 г. Архивировано из оригинала 19 ноября 2016 г. Получено 25 сентября 2012 г.
  16. ^ "[2 июля 2024 г.] Мы доказали, что "BB(5) = 47 176 870"". The Busy Beaver Challenge . 2 июля 2024 г. . Получено 2 июля 2024 г. .
  17. ^ "The Busy Beaver Challenge". bbchallenge.org . Получено 2 июля 2024 г. .
  18. ^ Кайзер, Ян-Оливер; Зилиани, Бета; Кребберс, Роббер; Режис-Жианас, Янн; Дрейер, Дерек (30 июля 2018 г.). «Mtac2: типизированные тактики для обратных рассуждений в Coq». Труды ACM по языкам программирования . 2 (ICFP): 78:1–78:31. doi : 10.1145/3236773 . hdl : 21.11116/0000-0003-2E8E-B .
  19. ^ Грегуар, Бенджамин; Махбуби, Ассия (2005). «Доказательство равенств в коммутативном кольце, выполненное правильно в Coq». В Hurd, Joe; Melham, Tom (ред.). Доказательство теорем в логике высшего порядка: 18-я международная конференция, TPHOLs 2005, Оксфорд, Великобритания, 22–25 августа 2005 г., Труды. Конспект лекций по информатике. Берлин, Гейдельберг: Springer. стр.  98–113 . doi :10.1007/11541868_7. ISBN 978-3-540-31820-0.
  20. ^ "Семейства тактики кольца и поля — документация Coq 8.11.1". coq.inria.fr . Получено 4 декабря 2023 г. .
  21. ^ Бессон, Фредерик (2007). «Быстрые рефлексивные арифметические тактики в линейном случае и далее». В Альтенкирхе, Торстене; Макбрайде, Коноре (ред.). Типы для доказательств и программ: Международный семинар, TYPES 2006, Ноттингем, Великобритания, 18–21 апреля 2006 г., пересмотренные избранные статьи . Конспект лекций по информатике. Том 4502. Берлин, Гейдельберг: Springer. стр.  48–62 . doi :10.1007/978-3-540-74464-1_4. ISBN 978-3-540-74464-1.
  22. ^ "Micromega: решатели для арифметических задач над упорядоченными кольцами — документация Coq 8.18.0". coq.inria.fr . Получено 4 декабря 2023 г. .
  23. ^ Braibant, Thomas; Pous, Damien (2010). Kaufmann, Matt; Paulson, Lawrence C. (ред.). Эффективная тактика Coq для решения алгебр Клини. Интерактивное доказательство теорем: Первая международная конференция, ITP 2010 Эдинбург, Великобритания, 11–14 июля 2010 г., Труды. Конспект лекций по информатике. Берлин, Гейдельберг: Springer. стр.  163–178 . doi :10.1007/978-3-642-14052-5_13. ISBN 978-3-642-14052-5. S2CID  3566183.
  24. ^ Narboux, Julien (2004). "Процедура принятия решения для геометрии в Coq". В Slind, Konrad; Bunker, Annette; Gopalakrishnan, Ganesh (ред.). Доказательство теорем в логике высшего порядка: 17-я международная конференция, TPHOLS 2004, Парк-Сити, штат Юта, США, 14–17 сентября 2004 г., Труды . Заметки лекций по информатике. Том 3223. Берлин, Гейдельберг: Springer. стр.  225–240 . doi :10.1007/978-3-540-30142-4_17. ISBN 978-3-540-30142-4. S2CID  11238876.
На Викискладе есть медиафайлы по теме Coq (язык программирования) .
  • Официальный сайт на английском языке
  • Coq на GitHub , репозиторий исходного кода
  • Интерактивная онлайн-система JsCoq – позволяет запускать Coq в веб-браузере без необходимости установки дополнительного программного обеспечения.
  • Alectryon – библиотека для обработки фрагментов Coq, встроенных в документы, показывающая цели и сообщения для каждого предложения Coq
  • Кок Вики
  • Библиотека математических компонентов – широко используемая библиотека математических структур, частью которой является язык доказательства SSReflect.
  • Конструктивный репозиторий Coq в Неймегене
  • Уроки математики
  • Coq в Open Hub
Учебники
  • Coq'Art – книга о Coq, написанная Ивом Берто и Пьером Кастераном
  • Сертифицированное программирование с зависимыми типами – онлайн и печатный учебник Адама Члипалы
  • Основы программного обеспечения – онлайн-учебник Бенджамина К. Пирса и др.
  • Введение в мелкомасштабное отражение в Coq – учебное пособие по SSReflect от Жоржа Гонтье и Ассии Махбуби
  • Моделирование и доказательство в теории вычислительных типов с использованием Coq Proof Assistant — учебник Герта Смолки, используемый для курса вычислительной логики — см. также ресурсы курса в Университете Саара
Учебники
Взято с "https://en.wikipedia.org/w/index.php?title=Coq_(программное обеспечение)&oldid=1263243132"