Gibt es eine minimale vollständige Taktik in Coq?

Question

Ich habe viele Coq-Taktiken gesehen, die sich in der Funktion überlappen.

Zum Beispiel, wenn Sie den genauen Abschluss in der Hypothese haben, können Sie assumption, apply, exact, trivial, und vielleicht andere. Andere Beispiele sind destruct und induction für nicht induktive Typen (??).

Meine Frage ist:

Gibt es einen minimal Satz von Grunde Taktik (das schließt auto und seine dergleichen), die abgeschlossen ist, in dem Sinne, dass dieser Satz jede Coq beweisen verwendet werden kann, -beweisbare Sätze über Funktionen von natürlichen Zahlen?

Die Taktik in diesem minimalen vollständigen Satz wäre ideal grundlegend, so dass jeder nur eine (oder zwei) Funktion ausführt und man leicht verstehen kann, was er tut.

Answer 1

Ein Beweis in Coq ist nur ein Begriff des richtigen Typs. Taktiken helfen Ihnen, diese Begriffe zu bilden, indem Sie kleinere Unterbegriffe in komplexere unterteilen. Daher würde der minimale Satz von grundlegenden Taktiken nur die Taktik exact enthalten, wie Konstantin erwähnte.

Die Taktik refine ermöglicht es Ihnen, direkt Proofterme zu geben, aber mit Löchern, die zu Unterzielen führen. Grundsätzlich ist jede Taktik nur ein Beispiel für die refine Taktik.

Wenn Sie jedoch zunächst nur eine minimale Menge von Taktik betrachten wollen, würde ich intro{s}, exists, reflexivity, symmetry, apply, rewrite, revert, destruct und induction betrachtet. inversion könnte auch ziemlich schnell nützlich sein.