Coq has two "modes": - Gallina, which is a pure functional programming language a lot like Idris, which is used in 'straightforward' definitions. - Ltac, whic

Coq has two "modes": - Gallina, which is a pure functional programming language a lot like Idris, which is used in 'straightforward' definitions. - Ltac, which is an awkward imperative language for incrementally building up proof objects using a variety of "tactic" primitives. Ltac is executed at compile time to generate values which would be cumbersome or impossible to write directly in Gallina (a bit like Lisp macros). Most of Coq's power is exposed via Ltac, e.g. most of the proofs in http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ are generalised into powerful Ltac functions; the reason for this is explained at http://adam.chlipala.net/cpdt/html/Cpdt.Large.html http://adam.chlipala.net/cpdt/html/Cpdt.Large.html Unfortunately, this focus on Ltac has left Gallina a little impoverished. For example, dependent matching in Gallina is pretty horrible (compared to, say, Agda; although there are complications there e.g. with the K axiom), whereas in Ltac we can simply use a tactic like `destruct`. Personally, I'm a fan of http://plv.mpi-sws.org/mtac/ http://plv.mpi-sws.org/mtac/ which allows regular Gallina, along with a few extensions, to be used instead of Ltac. Basically, any 'unsafe' action which we might have done in Ltac, like general recursion, gets wrapped up in a monadic datatype "M". During compilation, "M foo" values can be forced to get the "foo" value they wrap, which are inserted into the output just like Ltac results. If that forcing fails, or loops forever, so does the compilation (again, like Ltac). Mtac feels a lot like using Idris IMHO.