Interactive typed tactic programming in the Coq proof assistant

Abstract

In order to allow for the verification of realistic problems, Coq provides a languagefor tactic programming, therefore enabling general-purpose scripting of automation routines. However, this language is untyped, and as a result, tactics are known to be difficult to compose, debug, and maintain. In this thesis, I develop two different approaches to typed tactic programming in the context of Coq: Lemma Overloading and Mtac. The first one utilizes the existing mechanism of overloading, already incorporated into Coq, to build typed tactics in a style that resembles that of dependently typed logic programming. The second one, Mtac, is a lightweight yet powerful extension to Coq that supports dependently typed functional tactic programming, with additional imperative features. I motivate the different characteristics of Lemma Overloading and Mtac through a wide range of examples, mainly coming from program verification. I also show how to combine these approaches in order to obtain the best of both worlds, resulting in extensible, typed tactics that can be programmed interactively. Both approaches rely heavily on the unification algorithm of Coq, which currently suffers from two main drawbacks: it incorporates heuristics not appropriate for tactic programming, and it is undocumented. In this dissertation, in addition to the aforementioned approaches to tactic programming, I build and describe a new unification algorithm better suited for tactic programming in Coq.

Um realistische Programme zu verifizieren, bietet Coq eine Sprache zum Programmieren von Taktiken. Sie ermöglicht das Schreiben universeller Automatisierungsroutinen. Diese Sprache ist allerdings ungetypt. Die resultierenden Taktiken sind daher bekannt dafür, schwer zusammensetzbar, testbar und wartbar zu sein. Ich entwickle in dieser Doktorarbeit zwei Ansätze für getypte Taktiken im Kontext von Coq: Das Überladen von Lemmata und Mtac. Ersteres benutzt den in Coq vorhandenen Überladungsmechanismus um Taktiken im Stil von Dependently Typed Logic Programming zu erstellen.Letzeres, Mtac, ist eine leichtgewichtige, aber mächtige Erweiterung zu Coq, die das Erstellen von funktionalen, Dependently Typed Taktiken mit imperativen Features erlaubt. Ich motiviere die verschiedenen Charakteristika der beiden Ansätze durch eine große Auswahl an Beispielen, die hauptsächlich aus der Programm-Verifizierung kommen. Ich demonstriere außerdem, wie man die Ansätze kombinieren kann, um das Beste aus beiden Welten zu bekommen: erweiterbare, getypte Taktiken die interaktiv programmiert werden können. Beide Ansätze sind stark abhängig vom Unifizierungs-Algorithmus in Coq. Dieser leidet momentan unter zwei Nachteilen. Einerseits sind die Heuristiken nicht auf das Programmieren von Taktiken abgestimmt. Andererseits ist der Algorithmus undokumentiert. Zusätzlich zu den oben genannten Ansätzen zur Programmierung von Taktiken, entwickle und beschreibe ich in dieser Dissertation einen neuen Unifizierungs-Algorithmus, der besser für die Programmierung von Taktiken geeignet ist.