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.
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.
Ł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).
Show Tree
w coq.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).
źródło
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.
źródło
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 :)
źródło