Benutzerdefinierte Prüfertaktiken in Idris

Question

Wenn ich es richtig verstehe (hauptsächlich aufgrund der Existenz des applyTactic Funktion) ist es möglich, benutzerdefinierte Taktiken für den Theorembeweis in Idris zu schreiben.Welche (oder wo) Beispiele könnte ich verwenden, um zu lernen, wie das geht?

Answer 1

Es gibt zwei Mechanismen zum Schreiben benutzerdefinierter Taktiken in Idris:High-Level- und Low-Level-Reflexion.

Mit High-Level-Reflexion schreiben Sie eine Funktion, die auf der Syntax und nicht auf ausgewerteten Daten ausgeführt wird – ihr Argument wird dabei nicht reduziert.Diese Funktionen geben eine neue Taktik zurück, die anhand der bereits vorhandenen Taktiken in Idris definiert wird.Wenn Sie einen Beweisbegriff direkt zurückgeben möchten, können Sie immer einfach verwenden Exact.Ein Beispiel für diese Art der Reflexion findet sich in die Effektbibliothek.Es werden hochrangige Reflexionstaktiken eingesetzt byReflection im Proof-Modus.

Bei der Low-Level-Reflexion arbeiten Sie direkt mit zitierten Begriffen aus der Kerntypentheorie von Idris.Eine Taktik ist dann eine Funktion in TT -> List (TTName, TT) -> Tactic Dabei ist das erste Argument der Zieltyp, das zweite der lokale Beweiskontext und das Rückgabeergebnis ist dasselbe wie bei der Reflexion auf hoher Ebene.Damit ist Laughadelic verbunden über.Diese werden mit aufgerufen applyTactic im Proof-Modus.