The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Dear members of the coq-club list:

We are proud to announce the first version of Mtac, a monad for typed
tactic programming in Coq. You can read the tutorial, and download the
patch and examples from the Mtac's homepage:

http://www.mpi-sws.org/~beta/mtac/

Mtac is a lightweight but powerful extension to Coq that supports
dependently-typed tactic programming. Mtac tactics have access to all
the features of ordinary Coq programming, as well as a new set of
typed tactical primitives. We avoid the need to touch the trusted
kernel typechecker of Coq by encapsulating uses of these new tactical
primitives in a monad, and instrumenting Coq so that it executes
monadic tactics during type inference.

As a sneak peek, this is what a simple propositional tautology prover
looks like in Mtac:

Definition simpl_prop_auto :=
  mfix f [p : Prop] : T p :=
    mmatch p with
    | True => ret I
    | [ p1 p2 ] p1 /\ p2 =>
         r1 <- f p1 ;
         r2 <- f p2 ;
         ret (conj r1 r2)
    | [p1 p2] p1 \/ p2 =>
         mtry
           r1 <- f p1 ;
           ret (or_introl r1)
         with _ =>
           r2 <- f p2 ;
           ret (or_intror r2)
         end
    | _ => raise NotFound
    end.

But, of course, there's much more than this, check it out!

The Mtac team