"Pełne" auto w Coq

Question

Uczę się Coqa i książki, z której się uczę, (CPDT) intensywnie używa auto w dowodach.

Odkąd się uczę, myślę, że może mi się przydać zobaczenie, co dokładnie robi auto pod maską (im mniej magii na początku tym lepiej). Czy istnieje sposób, aby zmusić go do wyświetlania dokładnie jakich taktyk lub technik używa do obliczenia dowodu?

Jeśli nie, czy istnieje miejsce, które dokładnie określa, co robi auto?

Answer 1

Istnieje wiele sposobów, aby rzucić okiem na to, co dzieje się pod maską.

TLDR: Podaj info przed swoją taktyką lub użyj Show Proof. przed i po wywołaniu taktyki i zauważ różnice.

---

Aby zobaczyć co dana taktyka inwokacja została robi, można poprzedzić to z info, tak aby pokazać konkretny dowód kroki podjęła.

(To może być przełamany Coq 8,4, widzę, że zapewniają one info_ wersje niektórych taktyk, przeczytaj komunikat o błędzie, jeśli trzeba).

To jest chyba to, co chcesz na poziomie początkującym, to może już być dość lakoniczne.

---

Innym sposobem, aby zobaczyć, co się obecnie dzieje w dowodzie jest użycie polecenia Show Proof.. Pokaże ci obecnie zbudowany termin z dziurami i pokazuje, którą dziurę ma wypełnić każdy z obecnych celów.

Jest to prawdopodobnie bardziej zaawansowany proces, szczególnie w przypadku użycia taktyki, jak induction lub inversion, ponieważ budowany termin będzie dość zaangażowany i wymagać będzie zrozumienia podstawowej natury schematów indukcyjnych lub zależnego dopasowywania wzorców (który CPDT powinien cię wkrótce nauczyć).

---

Po zakończeniu dowodu z Qed. (lub Defined.), można też poprosić, by spojrzeć na termin, który został zbudowany przy użyciu Print term. gdzie term to nazwa twierdzenia/term.

To często będzie wielki i brzydki termin i wymaga pewnego szkolenia, aby móc je przeczytać w odniesieniu do zaangażowanych terminów. W szczególności, jeśli termin został zbudowany za pomocą potężnych taktyk (takich jak omega, crush, itp.), Prawdopodobnie będzie nieczytelny. Zasadniczo używałbyś tego tylko do skanowania w określonym miejscu, w którym jesteś zainteresowany. Jeśli ma więcej niż 10 linii, nie przejmuj się czytaniem go w tak surowym formacie! :)

---

Z wszystkich poprzednich, można użyć Set Printing All. wcześniej, tak że Coq drukuje rozłożeniu, jawne wersje wszystkiego. Jest dodatkowo gadatliwy, ale może pomóc, gdy zastanawiasz się, jakie są wartości niejawnych parametrów.

Są to wszystkie te, które mogę myśleć na czubku mojej głowy, może być jednak więcej.

---

chodzi o to, co robi taktyka, zwykle najlepsza odpowiedź można znaleźć w dokumentacji:

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic155

Zasadniczo auto stara się wykorzystać wszystkie wskazówki dostarczone (w zależności od bazy danych używanej) i rozwiązać swój cel, łącząc je do pewnej głębi (którą można określić). Domyślnie baza danych to core, a głębokość to 5.

Więcej informacji na ten temat można znaleźć tutaj:

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#Hints-databases