"Verbose" Auto in Coq

Question

Ich lerne Coq und das Buch, von dem ich lerne, (CPDT) macht schwere Verwendung von auto in Proofs.

Seit ich lerne denke ich könnte es für mich hilfreich sein, genau zu sehen, was tut unter der Haube (je weniger Magie früh, desto besser). Gibt es eine Möglichkeit, sie zu zwingen, genau zu zeigen, welche Taktiken oder Techniken sie zur Berechnung des Beweises verwenden?

Wenn nicht, gibt es einen Ort, der genau angibt, was tut?

Answer 1

Es gibt mehrere Möglichkeiten, um einen Blick darauf zu werfen, was unter der Haube passiert.

TLDR: Setzen Sie info vor Ihre Taktik, oder verwenden Sie Show Proof. vor und nach dem Aufruf der Taktik und erkennen Sie die Unterschiede.

---

Um zu sehen, was eine bestimmte Taktik Aufruf zu tun ist, können Sie das Präfix mit info ist, so wie der besondere Nachweis von ihm unternommenen Schritte zu zeigen.

(Dies könnte mit Coq 8,4 gebrochen werden, ich sehe, dass sie info_ Versionen einiger Taktik bieten, lesen Sie die Fehlermeldung, wenn Sie benötigen.)

Dies ist wahrscheinlich das, was Sie bei einem Anfänger wollen, ist es kann schon ziemlich knapp sein.

---

Ein anderer Weg, um zu sehen, was zur Zeit innerhalb eines Beweises geht, ist der Befehl Show Proof. zu verwenden. Es zeigt Ihnen den aktuell erstellten Begriff mit Löchern und zeigt Ihnen, welches Loch jedes Ihrer aktuellen Ziele füllen soll.

Dies ist wahrscheinlich fortgeschrittener, vor allem wenn Sie Taktik wie induction oder inversion verwenden, da der Begriff gebaut wird ziemlich beteiligt sein, und müssen Sie die zugrunde liegende Natur von Induktionsschemata oder abhängige Muster-Matching zu verstehen (welche CPDT sollte Sie bald genug lehren).

---

Sobald Sie einen Beweis mit Qed. (oder Defined.) abgeschlossen haben, können Sie auch auf den Begriff suchen fragen, die mithilfe von Print term. gebaut wurde, wo term der Name des Satzes/Begriff ist.

Dies wird oft ein großer und hässlicher Begriff sein, und es braucht etwas Training, um diese für die beteiligten Begriffe lesen zu können. Insbesondere, wenn der Begriff durch die Verwendung von mächtigen Taktiken (wie omega, crush, etc.) gebaut wurde, wird es wahrscheinlich unlesbar sein. Sie würden das im Grunde nur verwenden, um an einer bestimmten Stelle des Begriffs zu scannen, an dem Sie interessiert sind. Wenn es mehr als 10 Zeilen lang ist, sollten Sie es nicht einmal in einem so groben Format lesen! :)

---

Mit dem vorherigen alle können Sie Set Printing All. vorher verwenden, so dass Coq die entfaltete, explizite Versionen alles druckt. Es ist auch ausführlich, kann aber helfen, wenn Sie sich fragen, was die Werte der impliziten Parameter sind.

Das sind alles Dinge, die mir in den Sinn kommen, aber es könnte noch mehr geben.

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

Grundsätzlich sind alle zu verwenden auto versucht, die Hinweise zur Verfügung gestellt (auf der Datenbank ab, die Sie verwenden:

---

Als für das, was eine Taktik der Fall ist, ist die übliche beste Antwort in der Dokumentation), und um Ihr Ziel zu lösen, kombinieren Sie sie bis zu einer gewissen Tiefe (die Sie angeben können). Standardmäßig ist die Datenbank core und die Tiefe ist 5.

Weitere Informationen über das finden Sie hier:

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