The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Very cool!  I read the recent MTac papers and have awaited it's
upcoming release just so I could play around with it.

Kris

On Wed, Apr 3, 2013 at 10:49 AM, Beta Ziliani 
<beta AT mpi-sws.org>
 wrote:
> 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