The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

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.