A typed tactic language for Coq.
Distributed under the terms of the MIT License, see LICENSE for details. Accepted contributions will be held under scrutiny to ensure they do not incur in a copyright infringement.
This repository contains a plugin for Coq with the tactic language described in the paper Mtac2: Typed Tactics for Backward Reasoning in Coq.
The project has 3 subdirectories:
srccontains the code of the plugin.
run.mlis the interpreter.
theoriescontains support Coq files for the plugin.
Mtac2.vdeclares the plugin on the Coq side and imports all the required theories.
intffolder contains the basics: the
Mmonad with its operations documented, exceptions, etc.
- The folder
tacticscontains everything relating to tactics:
Tactics.vdefines the tactic type and several tactics and combinators.
Ttactics.vdefines the type for typed tactics and combinators.
IntroPatt.vdefines intro patterns.
ConstrSelector.vdefines a selector based on the indices of an inductive type's constructors.
examplescontains simple examples to show the different features of Mtac2.
tactics.vshows how to standard, Ltac's like, proving. But with some interesting features not present in Ltac.
tauto.vshows many different ways to code a simple tautology prover, with different degrees of certainty and verboseness.
test-suitecontains several tests, including some uses of the plugin.
The plugin works currently with Coq v8.7 (and any minor version). It requires UniCoq to be installed. Mtac2 will be available in OPAM soon. For the moment you should have coqc, ocamlc and make in your path. Then simply do:
coq_makefile -f _CoqProject -o Makefile
To generate a makefile from the description in
This will consecutively build the plugin and the supporting
You can then either
make install the plugin or leave it in its
current directory. To be able to import it from anywhere in Coq,
simply add the following to
Add LoadPath "path_to_mtac2/theories" as Mtac2. Add ML Path "path_to_mtac2/src".
Once installed, you can
Require Import Mtac2.Mtac2 to load the
plugin. The plugin defines a tactic
mrun t to execute code
t and a proof
MProof where Mtac2's tactic can be executed directly.