MtacAR: Monadic typed tactic programming in Agda by Reflection

Introduction

Screenshots

Note that the above is a simple tautolgogy solver from [2], not tauto in Coq.

Requirements

• Agda 2.6.1
• Agda Standard Library v1.0 or above
• My Prelude

Usage

Reference

Ordered by relevance

1. D. Christiansen and E. Brady, “Elaborator reflection: extending Idris in Idris,” ACM SIGPLAN Not., vol. 51, no. 9, pp. 284–297, Sep. 2016. https://doi.org/10.1145/3022670.2951932

2. B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, and V. Vafeiadis, “Mtac: A monad for typed tactic programming in Coq,” J. Funct. Program., vol. 25, p. e12, 2015. https://doi.org/10.1017/S0956796815000118

3. J.-O. Kaiser, B. Ziliani, R. Krebbers, Y. Régis-Gianas, and D. Dreyer, “Mtac2: typed tactics for backward reasoning in Coq,” Proc. ACM Program. Lang., vol. 2, no. ICFP, pp. 1–31, 2018. https://doi.org/10.1145/3236773

TO-DO

• Support backward reasoning
• Improve performance
• Add more examples
• Write a paper