The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

One source you might also find interesting is Mtac:

http://plv.mpi-sws.org/mtac/

While not a formalization of Ltac itself, it provides a large subset of the functionality, and is written in Gallina itself (though not actually a formal description).

Best,

Cody

This email has been sent from a virus-free computer protected by Avast.
www.avast.com

On Sun, Mar 6, 2016 at 9:52 AM, Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> wrote:

Hi,

On 03/06/2016 02:39 AM, Xiaoyu Zhou wrote:
>
>     I think that formal description will facilitate automatic use of tactics.

I am not sure what you mean by "facilitating automatic use of tactics".

Concerning "formal descriptions of the tactics in Coq",
this is what helped me:

  http://matej-kosik.github.io/www/doc/coq/notes/01__tactics.html

It is just a theory that explaines the behavior of Coq I observed.
The theory is complete and accurate only up to my experience.

There, for higher-level tactics I explain how they can be mapped into
lower-level tactics.

So, for example for the higher-level tactics "reflexivity" I say that it can be translated to lower level tactics "constructor 1"
plus an example that demonstrate what happens if you "unfold" reflexivity.

At the beginning I tried to visualize partial order of what could unfold to what.
(there is one cycle but it is just mutual recursion on subterms and therefore OK)

I haven't tested whether this document is useful to other people yet.