Как бы я изучил основную теорию ассистента Coq proof?

40

Я перебираю примечания к курсу на CIS 500: основы программного обеспечения и упражнения - это очень весело. Я только на третьем упражнении, но я хотел бы узнать больше о том, что происходит, когда я использую тактику, чтобы доказать такие вещи, какforall (n m : nat), n + n = m + m -> n = m.

lo.logic type-theory proof-assistants proof-theory coq davidk01
источник

Ответы:

32

Одним из мест для начала является справочное руководство Coq ( pdf ). Глава 4 описывает основную логику Coq, и в конечном итоге все основано на этом. Это называется исчислением (со) индуктивных конструкций, и многие статьи описывают. Попадание в руки книги Coq'Art Интерактивное доказательство теорем и разработка программы обеспечивает более неторопливое, но не дешевое введение в Coq.

Чтобы узнать, как работает тактика, взгляните на этот предыдущий вопрос: как «тактика» работает в помощниках по доказательству?

Чтобы построить требуемую теорию, вам нужно узнать о теории типов . Наиболее тесно связаны с теорией, лежащей в основе помощника по доказательству, вероятно, заметки (или книга ) Интуиционистской теории типов Пера Мартина-Лёфа или книга « Программирование в теории типов Мартина-Лёфа» , которая на самом деле о написании и доказательстве теорем в теории типов. Перспектива языка программирования по теории типов может быть получена из Типов и языков программирования Пирса . « Доказательства и типы» Жирара и др. , В которых также рассматривается важность корреспонденции Карри-Ховарда , является еще одним прекрасным справочным материалом. Тогда вы, вероятно, хорошо и действительно готовы читать "Кокванд" и "Уэт".Исчисление конструкций . Наконец, найдите некоторые ссылки в конце руководства Coq.

Есть и другие помощники по проверке, HOL, NuPRL, Mizar, Twelf и т. Д., И у них тоже есть свои теории, так что вы тоже можете многому научиться, читая в этом направлении.

Наконец, для обзора истории и будущего помощников по проверке ознакомьтесь с недавней статьей Herman Geuvers.

Дэйв Кларк
источник
5
Хороший список. Я добавлю порядок чтения. TAPL Пирса покрывает фон; большая часть остальных не будет иметь смысла, пока вы не станете свободно владеть правилами набора текста. Глава 2 ATTAPL вводит зависимые типы относительно осторожно. Затем вы можете прочитать главу 4 руководства по Coq, в котором есть правила набора текста (вам нужно проверить библиографию для некоторых продвинутых вещей, таких как точные правила для рекурсии). Параллельно книга Coq'Art имеет более практическую перспективу. Бонусный совет: Show Treeв соц.
Жиль "ТАК - перестань быть злым"
2
Я - кто-то в более или менее той же позиции, что и ОП, хотя немного дальше. После некоторых экспериментов я наконец нашел порядок 1) Изучить функциональное программирование 2) Прочитать TAPL 3) Прочитать о зависимых типах в ATTAPL, чтобы они работали лучше других. Рад, что я нахожусь на правильном пути.
Джон Сальватье
1
Я тоже был здесь и получил книгу Coq'Art. Это абсолютно идеально подходит для понимания, они подробно описывают каждую тактику и объясняют, когда и как ее использовать. Книга также проведет вас быстро через каждое базовое правило в теории типов, научит вас обозначениям и тому, как их использовать в Coq. Люблю эту книгу.
Лэнс Поллард
15

Что касается типизированного лямбда-исчисления, интуиционистской логики, различных систем доказательств и изоморфизма Карри-Ховарда, которые являются частью математического фона Coq, я настоятельно рекомендую «Лекции по изоморфизму Карри-Ховарда» (П. Уржичин и М. Серенсен).

Марчин Котовски
источник
Мы, кажется, сегодня на одной волне . ;-)
Марк Хаманн
Кажется, это день Карри-Ховарда: cstheory.stackexchange.com/questions/5848/…
Дейв Кларк,
6

Книга Ло о Расширенном исчислении конструкций также является хорошим справочным материалом. ECC был весьма влиятельным в разработке теории типов Coq.

Доминик Маллиган
источник