Кок (программное обеспечение)

Кок (программное обеспечение)
Разработчики)	Команда разработчиков Coq
Начальная версия	1 мая 1989 г .; 35 лет назад (версия 4.10)
Стабильная версия	8.19.1 / 4 марта 2024 г .; 3 месяца назад
Репозиторий	github .с /coq /coq
Написано в	OCaml
Операционная система	Кросс-платформенный
Доступно в	Английский
Тип	Помощник по доказательствам
Лицензия	LGPLv2.1
Веб-сайт	петух .инрия .fr

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

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

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

Обзор [ править ]

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

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

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

В качестве примера доказательство коммутативности сложения натуральных чисел в Coq:

plus_comm   = 
 fun   n   m   :   nat   => 
 nat_ind   (  fun   n0   :   nat   =>   n0   +   m   =   m   +   n0  ) 
   (  plus_n_0   m  ) 
   (  fun   (  y   :   nat  )   (  H   :   y   +   m   =   m   +   y  )   => 
    eq_ind   (  S   (  m   +   y  )) 
      (  fun   n0   :   nat   =>   S   (  y   +   m  )   =   n0  ) 
      (  f_equal   S   H  ) 
      (  m   +   S   y  ) 
      (  plus_n_Sm   m   y  ))   n 
      :   forall   n   m   :   nat  ,   n   +   м   =   м   +   п

nat_ind означает математическую индукцию , eq_ind для замены равных, и f_equalдля взятия одной и той же функции в обе части равенства. Ссылки на более ранние теоремы показывают, что $m=m+0$ и $S(m+y)=m+Sy$ .

Известные виды использования [ править ]

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

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

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

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

Другие приложения [ править ]

CompCert : оптимизирующий компилятор почти для всего языка программирования C , который в основном запрограммирован и корректен в Coq.
Структура данных с непересекающимся множеством : доказательство корректности в Coq была опубликована в 2007 году. ^[13]
Теорема Фейта – Томпсона : формальное доказательство с использованием Coq было завершено в сентябре 2012 года. ^[14]

Тактический язык [ править ]

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

Требовать   импорт   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»). ^[18]^[19] Дальнейшие процедуры принятия решений были разработаны в виде библиотек, в том числе для алгебр Клини. ^[20] и еще один для определенных геометрических целей. ^[21]

См. также [ править ]

Ссылки [ править ]

^ «Выпуск Coq 8.19.1» . 4 марта 2024 г. Проверено 14 марта 2024 г.
^ «Альтернативные названия · coq/coq Wiki» . Гитхаб . Проверено 3 марта 2023 г.
^ «Дорожная карта Coq 069» . Гитхаб .
^ Краткое введение в Coq
^ Авигад, Джереми; Махбуби, Ассия (3 июля 2018 г.). Интерактивное доказательство теорем: 9-я Международная конференция ITP 2018, проходившая под именем... Springer. ISBN 9783319948218 . Проверено 21 октября 2018 г.
^ "Часто задаваемые вопросы" . Гитхаб . Проверено 8 мая 2019 г.
^ «Введение в исчисление индуктивных конструкций» . Проверено 21 мая 2019 г.
^ Адам Члипала. «Сертифицированное программирование с зависимыми типами»: «Библиотечные вселенные» .
^ Адам Члипала. «Сертифицированное программирование с зависимыми типами»: «Библиотека GeneralRec» . «Библиотека индуктивных типов» .
^ Гонтье, Жорж (2008). «Формальное доказательство — теорема о четырех цветах» (PDF) . Уведомления Американского математического общества . 55 (11): 1382–1393. МР 2463991 .
^ Гонтье, Жорж; Махбуби, Ассия (2010). «Введение в мелкомасштабное отражение в Coq» . Журнал формализованного рассуждения . 3 (2): 95–152. doi : 10.6092/ISSN.1972-5787/1979 .
^ «Библиотека математических компонентов 1.11.0» . Гитхаб .
^ Коншон, Сильвен; Филлиатр, Жан-Кристоф (2007). «Постоянная структура данных для поиска объединений». В Руссо, Клаудио В.; Дрейер, Дерек (ред.). Материалы семинара ACM по ML, 2007 г., Фрайбург, Германия, 5 октября 2007 г. Ассоциация вычислительной техники. стр. 37–46. дои : 10.1145/1292535.1292541 .
^ «Теорема Фейта-Томпсона полностью проверена в Coq» . Msr-inria.inria.fr. 20 сентября 2012 г. Архивировано из оригинала 19 ноября 2016 г. Проверено 25 сентября 2012 г.
^ Кайзер, Ян-Оливер; Зилиани, Бета; Кребберс, Робберт; Режис-Жианас, Янн; Дрейер, Дерек (30 июля 2018 г.). «Mtac2: типизированная тактика обратного рассуждения в Coq» . Труды ACM по языкам программирования . 2 (ICFP): 78:1–78:31. дои : 10.1145/3236773 . hdl : 21.11116/0000-0003-2E8E-B .
^ Грегуар, Бенджамин; Махбуби, Ассия (2005). «Доказательство равенства в коммутативном кольце, выполненное правильно в Coq». В Херде, Джо; Мелхэм, Том (ред.). Доказательство теорем в логике высшего порядка: 18-я Международная конференция, TPHOLs 2005, Оксфорд, Великобритания, 22–25 августа 2005 г., Труды . Конспекты лекций по информатике. Берлин, Гейдельберг: Springer. стр. 98–113. дои : 10.1007/11541868_7 . ISBN 978-3-540-31820-0 .
^ «Семейства тактик ринга и поля — документация Coq 8.11.1» . coq.inria.fr . Проверено 4 декабря 2023 г.
^ Бессон, Фредерик (2007). «Быстрорефлексивная арифметическая тактика в линейном случае и за его пределами» . В Альтенкирхе Торстен; Макбрайд, Конор (ред.). Типы доказательств и программ: Международный семинар, TYPES 2006, Ноттингем, Великобритания, 18–21 апреля 2006 г., Пересмотренные избранные статьи . Конспекты лекций по информатике. Том. 4502. Берлин, Гейдельберг: Springer. стр. 48–62. дои : 10.1007/978-3-540-74464-1_4 . ISBN 978-3-540-74464-1 .
^ «Микромега: решатели арифметических задач над упорядоченными кольцами — документация Coq 8.18.0» . coq.inria.fr . Проверено 4 декабря 2023 г.
^ Брайбант, Томас; Поус, Дэмиен (2010). Кауфманн, Мэтт; Полсон, Лоуренс К. (ред.). Эффективная тактика Coq для решения алгебр Клини . Интерактивное доказательство теорем: Первая международная конференция, ITP 2010, Эдинбург, Великобритания, 11–14 июля 2010 г., Труды. Конспекты лекций по информатике. Берлин, Гейдельберг: Springer. стр. 163–178. дои : 10.1007/978-3-642-14052-5_13 . ISBN 978-3-642-14052-5 . S2CID 3566183 .
^ Нарбу, Жюльен (2004). «Процедура принятия решения по геометрии в Coq» . В Слинде, Конрад; Бункер, Аннетт; Гопалакришнан, Ганеш (ред.). Доказательство теорем в логике высшего порядка: 17-я Международная конференция, TPHOLS 2004, Парк-Сити, Юта, США, 14–17 сентября 2004 г., Труды . Конспекты лекций по информатике. Том. 3223. Берлин, Гейдельберг: Springer. стр. 225–240. дои : 10.1007/978-3-540-30142-4_17 . ISBN 978-3-540-30142-4 . S2CID 11238876 .

Внешние ссылки [ править ]

Официальный сайт , на английском языке
Coq на GitHub , репозиторий исходного кода
Интерактивная онлайн-система JsCoq – позволяет Coq работать в веб-браузере без необходимости установки дополнительного программного обеспечения.
Alectryon — библиотека для обработки фрагментов Coq, встроенных в документы, отображающая цели и сообщения для каждого предложения Coq.
Кок вики
Библиотека математических компонентов – широко используемая библиотека математических структур, частью которой является язык доказательства SSReflect.
Хранилище Constructive Coq в Неймегене
Классы математики
Кок в Open Hub

Учебники

The Coq'Art - книга Ива Берто и Пьера Кастерана о Coq.
Сертифицированное программирование с зависимыми типами - онлайн- и печатный учебник Адама Члипалы
Основы программного обеспечения - онлайн-учебник Бенджамина К. Пирса и др.
Введение в мелкомасштабное отражение в Coq — учебник по SSReflect от Жоржа Гонтье и Ассии Махбуби.

Учебники

Введение в Coq Proof Assistant – видеолекция Эндрю Аппеля в Институте перспективных исследований
Видеоуроки Coq от Андрея Бауэра

[wikidata-3975ab80ea94b22b71d7b9bfcc6a914428fb10a2-v12-1] «Выпуск Coq 8.19.1» . 4 марта 2024 г. Проверено 14 марта 2024 г.

[2] «Альтернативные названия · coq/coq Wiki» . Гитхаб . Проверено 3 марта 2023 г.

[3] «Дорожная карта Coq 069» . Гитхаб .

[4] Краткое введение в Coq

[5] Авигад, Джереми; Махбуби, Ассия (3 июля 2018 г.). Интерактивное доказательство теорем: 9-я Международная конференция ITP 2018, проходившая под именем... Springer. ISBN 9783319948218 . Проверено 21 октября 2018 г.

[6] "Часто задаваемые вопросы" . Гитхаб . Проверено 8 мая 2019 г.

[7] «Введение в исчисление индуктивных конструкций» . Проверено 21 мая 2019 г.

[8] Адам Члипала. «Сертифицированное программирование с зависимыми типами»: «Библиотечные вселенные» .

[9] Адам Члипала. «Сертифицированное программирование с зависимыми типами»: «Библиотека GeneralRec» . «Библиотека индуктивных типов» .

[:0-10] Гонтье, Жорж (2008). «Формальное доказательство — теорема о четырех цветах» (PDF) . Уведомления Американского математического общества . 55 (11): 1382–1393. МР 2463991 .

[11] Гонтье, Жорж; Махбуби, Ассия (2010). «Введение в мелкомасштабное отражение в Coq» . Журнал формализованного рассуждения . 3 (2): 95–152. doi : 10.6092/ISSN.1972-5787/1979 .

[12] «Библиотека математических компонентов 1.11.0» . Гитхаб .

[13] Коншон, Сильвен; Филлиатр, Жан-Кристоф (2007). «Постоянная структура данных для поиска объединений». В Руссо, Клаудио В.; Дрейер, Дерек (ред.). Материалы семинара ACM по ML, 2007 г., Фрайбург, Германия, 5 октября 2007 г. Ассоциация вычислительной техники. стр. 37–46. дои : 10.1145/1292535.1292541 .

[14] «Теорема Фейта-Томпсона полностью проверена в Coq» . Msr-inria.inria.fr. 20 сентября 2012 г. Архивировано из оригинала 19 ноября 2016 г. Проверено 25 сентября 2012 г.

[15] Кайзер, Ян-Оливер; Зилиани, Бета; Кребберс, Робберт; Режис-Жианас, Янн; Дрейер, Дерек (30 июля 2018 г.). «Mtac2: типизированная тактика обратного рассуждения в Coq» . Труды ACM по языкам программирования . 2 (ICFP): 78:1–78:31. дои : 10.1145/3236773 . hdl : 21.11116/0000-0003-2E8E-B .

[16] Грегуар, Бенджамин; Махбуби, Ассия (2005). «Доказательство равенства в коммутативном кольце, выполненное правильно в Coq». В Херде, Джо; Мелхэм, Том (ред.). Доказательство теорем в логике высшего порядка: 18-я Международная конференция, TPHOLs 2005, Оксфорд, Великобритания, 22–25 августа 2005 г., Труды . Конспекты лекций по информатике. Берлин, Гейдельберг: Springer. стр. 98–113. дои : 10.1007/11541868_7 . ISBN 978-3-540-31820-0 .

[17] «Семейства тактик ринга и поля — документация Coq 8.11.1» . coq.inria.fr . Проверено 4 декабря 2023 г.

[18] Бессон, Фредерик (2007). «Быстрорефлексивная арифметическая тактика в линейном случае и за его пределами» . В Альтенкирхе Торстен; Макбрайд, Конор (ред.). Типы доказательств и программ: Международный семинар, TYPES 2006, Ноттингем, Великобритания, 18–21 апреля 2006 г., Пересмотренные избранные статьи . Конспекты лекций по информатике. Том. 4502. Берлин, Гейдельберг: Springer. стр. 48–62. дои : 10.1007/978-3-540-74464-1_4 . ISBN 978-3-540-74464-1 .

[19] «Микромега: решатели арифметических задач над упорядоченными кольцами — документация Coq 8.18.0» . coq.inria.fr . Проверено 4 декабря 2023 г.

[20] Брайбант, Томас; Поус, Дэмиен (2010). Кауфманн, Мэтт; Полсон, Лоуренс К. (ред.). Эффективная тактика Coq для решения алгебр Клини . Интерактивное доказательство теорем: Первая международная конференция, ITP 2010, Эдинбург, Великобритания, 11–14 июля 2010 г., Труды. Конспекты лекций по информатике. Берлин, Гейдельберг: Springer. стр. 163–178. дои : 10.1007/978-3-642-14052-5_13 . ISBN 978-3-642-14052-5 . S2CID 3566183 .

[21] Нарбу, Жюльен (2004). «Процедура принятия решения по геометрии в Coq» . В Слинде, Конрад; Бункер, Аннетт; Гопалакришнан, Ганеш (ред.). Доказательство теорем в логике высшего порядка: 17-я Международная конференция, TPHOLS 2004, Парк-Сити, Юта, США, 14–17 сентября 2004 г., Труды . Конспекты лекций по информатике. Том. 3223. Берлин, Гейдельберг: Springer. стр. 225–240. дои : 10.1007/978-3-540-30142-4_17 . ISBN 978-3-540-30142-4 . S2CID 11238876 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]