Jan-Oliver Kaiser
Abstract
Coq supports a range of built-in tactics, which are engineered primarily to support backward reasoning. Starting from a desired goal, the Coq programmer can use these tactics to manipulate the proof state interactively, applying axioms or lemmas to break the goal into subgoals until all subgoals have been solved. Additionally, it provides support for tactic programming via OCaml and Ltac, so that users can roll their own custom proof automation routines.
Unfortunately, though, these tactic languages share a significant weakness. They do not offer the tactic programmer any static guarantees about the soundness of their custom tactics, making large tactic developments difficult to maintain. To address this limitation, Ziliani et al. previously proposed Mtac, a new typed approach to custom proof automation in Coq which provides the static guarantees that OCaml and Ltac are missing. However, despite its name, Mtac is really more of a metaprogramming language than it is a full-blown tactic language: it misses an essential feature of tactic programming, namely the ability to directly manipulate Coq’s proof state and perform backward reasoning on it.
In this paper, we present Mtac2, a next-generation version of Mtac that combines its support for typed metaprogramming with additional support for the programming of backward-reasoning tactics in the style of Ltac. In so doing, Mtac2 introduces a novel feature in tactic programming languages—what we call typed backward reasoning. With this feature, Mtac2 is capable of statically ruling out several classes of errors that would otherwise remain undetected at tactic definition time. We demonstrate the utility of Mtac2’s typed tactics by porting several tactics from a large Coq development, the Iris Proof Mode, from Ltac to Mtac2.
Supplemental Material
- The Agda Development Team. 2018. Reflection. Retrieved March 16, 2018 from https://agda.readthedocs.io/en/v2.5.3/ language/reflection.htmlGoogle Scholar
- Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. 2009. A new type for tactics. PLMMS (2009), 22.Google Scholar
- Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant, and Ronan Saillard. 2012. Dedukti: A universal proof checker. In Journées communes LTP - LAC. https://hal-mines-paristech.archives-ouvertes.fr/hal-01537578Google Scholar
- Raphaël Cauderlier. 2018. Tactics and certificates in Meta Dedukti. In ITP (ITP ‘18).Google Scholar
- Raphaël Cauderlier and François Thiré. {n. d.}. Meta Dedukti. http://deducteam.gforge.inria.fr/metadedukti/Google Scholar
- David Christiansen and Edwin Brady. 2016. Elaborator reflection: Extending Idris in Idris. In ICFP. 284–297. Google ScholarDigital Library
- Guillaume Claret, Lourdes del Carmen González Huesca, Yann Régis-Gianas, and Beta Ziliani. 2013. Lightweight proof by reflection using a posteriori simulation of effectful computation. In ITP (LNCS), Vol. 7998. 67–83. Google ScholarDigital Library
- Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. 2017. A metaprogramming framework for formal verification. PACMPL 1, ICFP (2017), 34:1–34:29. Google ScholarDigital Library
- Matthias Felleisen and Robert Hieb. 1992. The revised report on the syntactic theories of sequential control and state. TCS 103, 2 (1992), 235–271. Google ScholarDigital Library
- M. J. C. Gordon. 2015. Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences 373, 2039 (2015).Google Scholar
- Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. 1979. Edinburgh LCF. LNCS, Vol. 78.Google Scholar
- Jason Gross, Andres Erbsen, and Adam Chlipala. 2018. Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac. In ITP (ITP ‘18).Google Scholar
- Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018. RustBelt: Securing the foundations of the Rust programming language. PACMPL 2, POPL, 66:1–66:34. Google ScholarDigital Library
- Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2017. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Submitted for publication (2017).Google Scholar
- Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP (LIPIcs), Vol. 74. 17:1–17:29.Google Scholar
- Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, and Derek Dreyer. 2018. Coq repository for Mtac2. https://github.com/Mtac2/Mtac2/ .Google Scholar
- Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive Proofs in Higher-Order Concurrent Separation Logic. In POPL. 205–217. Google ScholarDigital Library
- Gregory Malecha, Abhishek Anand, Simon Boulier, and Matthieu Sozeau. 2018. Reflection library for Coq. Retrieved March 16, 2018 from https://github.com/Template-Coq/template-coqGoogle Scholar
- Gregory Malecha and Jesper Bengtson. 2016. Extensible and efficient automation through reflective tactics. In ESOP (LNCS), Vol. 9632. 532–559.Google Scholar
- Conor McBride and Ross Paterson. 2008. Applicative programming with effects. JFP 18, 1 (2008), 1–13. Google ScholarDigital Library
- Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory. TOCL 9, 3 (2008), 23:1–23:49. Google ScholarDigital Library
- Pierre-Marie Pédrot. 2016. The Coq tactic engine. Retrieved March 16, 2018 from http://coqhott.gforge.inria.fr/blog/ coq-tactic-engine/Google Scholar
- Pierre-Marie Pédrot. 2018. A standalone implementation of Ltac2 as a Coq plugin. Retrieved March 16, 2018 from https://github.com/ppedrot/ltac2/Google Scholar
- Brigitte Pientka. 2008. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In POPL. 371–382. Google ScholarDigital Library
- Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In TPHOLs (LNCS), Vol. 5170. 278–293. Google ScholarDigital Library
- Matthieu Sozeau and Nicolas Tabareau. 2014. Universe Polymorphism in Coq. In ITP (LNCS), Vol. 8558. 499–514.Google Scholar
- Arnaud Spiwack. 2010. An abstract type for constructing tactics in Coq. In Proof Search in Type Theory.Google Scholar
- Antonis Stampoulis and Zhong Shao. 2010. VeriML: Typed computation of logical terms inside a language with effects. In ICFP. 333–344. Google ScholarDigital Library
- David Swasey, Deepak Garg, and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. PACMPL 1, OOPSLA (2017), 89:1–89:26. Google ScholarDigital Library
- Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal. 2018. A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runST. PACMPL 2, POPL, 64:1–64:28. Google ScholarDigital Library
- Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, and Viktor Vafeiadis. 2013. Mtac: A monad for typed tactic programming in Coq. In ICFP. 87–100. Google ScholarDigital Library
- Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, and Viktor Vafeiadis. 2015. Mtac: A monad for typed tactic programming in Coq. JFP 25 (2015).Google Scholar
Index Terms
- Mtac2: typed tactics for backward reasoning in Coq
Recommendations
LOGIC: A Coq Library for Logics
Dependable Software Engineering. Theories, Tools, and ApplicationsAbstractLOGIC is a Coq library for formalizing logic studies, concerning both logics’ applications and logics themselves (meta-theories). For applications, users can port derived rules and efficient proof automation tactics from LOGIC to their own program-...
Nominal Reasoning Techniques in Coq
We explore an axiomatized nominal approach to variable binding in Coq, using an untyped lambda-calculus as our test case. In our nominal approach, alpha-equality of lambda terms coincides with Coq's built-in equality. Our axiomatization includes a ...
Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and ProofsThe completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
Comments