Jak mógłbym zacząć uczyć się podstawowej teorii asystenta dowodu Coq?

40

Przeglądam notatki z kursu na CIS 500: podstawy oprogramowania i ćwiczenia są świetną zabawą. Jestem dopiero na trzecim zestawie ćwiczeń, ale chciałbym dowiedzieć się więcej o tym, co się dzieje, gdy używam taktyki do udowodnienia, żeforall (n m : nat), n + n = m + m -> n = m.

— davidk01
źródło

32

Jednym z nich jest podręcznik referencyjny Coq ( pdf ). Rozdział 4 opisuje podstawową logikę Coq i ostatecznie wszystko na tym opiera się. Nazywa się to rachunkiem (ko) konstrukcji indukcyjnych i wiele artykułów opisuje. Zdobycie książki o Coq'Art Interaktywne sprawdzanie twierdzeń i programowanie zapewnia spokojniejsze, ale nie tanie wprowadzenie do Coq.

Aby dowiedzieć się, jak działają taktyki, spójrz na to wcześniejsze pytanie: Jak działają „taktyki” w asystentach dowodowych?

Aby zbudować wymaganą teorię, musisz poznać teorię typów . Najściślej związany z teorią leżącą u podstaw asystenta dowodu jest prawdopodobnie Intutionistic Teoria typów Per Martina- Löfa (lub książka ) lub książka Programowanie w teorii typu Martin-Löf , która tak naprawdę dotyczy pisania i dowodzenia twierdzeń w teorii typów. Perspektywa języka programowania dla teorii typów można uzyskać z Pierce's Types and Programming Languages . Dowody i typy Girarda i in. , Które również odnoszą się do znaczenia korespondencji Curry-Howarda , są kolejnym doskonałym odniesieniem. W takim razie jesteś prawdopodobnie dobrze przygotowany do czytania Coquanda i HuetaRachunek konstrukcji . Na koniec przejrzyj niektóre referencje z tyłu podręcznika Coq.

Są inni asystenci dowodowi , HOL, NuPRL, Mizar, Twelf itd., I mają też swoją teorię, więc możesz się wiele nauczyć, czytając w tym kierunku.

Na koniec, aby zapoznać się z historią i przyszłością asystentów ds. Dowodów, zapoznaj się z najnowszym artykułem Hermana Geuversa.

— Dave Clarke
źródło

5

Ładna lista. Dodam kolejność czytania. TAPL Pierce'a obejmuje tło; większość reszty nie ma sensu, dopóki nie opanujesz zasad pisania na klawiaturze. Rozdział 2 ATTAPL stosunkowo delikatnie wprowadza typy zależne. Następnie możesz przeczytać rozdział 4 podręcznika Coq, który zawiera zasady pisania na klawiaturze (musisz sprawdzić bibliografię pod kątem niektórych zaawansowanych rzeczy, takich jak dokładne zasady rekurencji). Równolegle książka Coq'Art ma bardziej praktyczne perspektywy. Dodatkowa wskazówka: Show Treew coq.

— Gilles 'SO - przestań być zły'

2

Jestem kimś mniej więcej w tej samej pozycji co OP, choć trochę dalej. Po kilku eksperymentach w końcu znalazłem kolejność 1) Naucz się programowania funkcjonalnego 2) Przeczytaj TAPL 3) Przeczytaj o typach zależnych w ATTAPL, aby działały lepiej niż inne rzeczy. Cieszę się, że jestem na właściwej ścieżce.

— John Salvatier,

1

Ja też tu byłem i kupiłem książkę Coq'Art. Jest absolutnie idealny do zrozumienia, szczegółowo omawiają każdą taktykę i wyjaśniają, kiedy i jak z niej korzystać. Książka prowadzi także szybko przez wszystkie podstawowe zasady teorii typów, ucząc notacji i jak używać jej w Coq. Kocham tę książkę.

— Lance Pollard,

15

Jeśli chodzi o typowy rachunek lambda, logikę intuicyjną, różne systemy dowodowe i izomorfizm Curry'ego-Howarda, które są częściami matematyki Coq, zdecydowanie polecam „Wykłady na temat izomorfizmu Curry-Howarda” (autor: P. Urzyczyn i M. Sørensen).

— Marcin Kotowski
źródło

Wydaje się, że jesteśmy dzisiaj na tej samej długości fali . ;-)

— Marc Hamann

Wydaje się być Curry-Howard dzień: cstheory.stackexchange.com/questions/5848/...

— Dave Clarke

6

Książka Luo o rozszerzonym rachunku konstrukcji jest również dobrym odniesieniem. ECC wywarło duży wpływ na projekt teorii typów Coqa.

— Dominic Mulligan
źródło

4

Obecna książka Software Foundations wyjaśnia to wszystko później: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html

Jeśli więc śledzisz książkę, czytaj dalej :)

— Catalin Hritcu
źródło