The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

Another complementary document is

  An Operational Foundation for the Tactic Language of Coq
  Wojciech Jedynak, Małgorzata Biernacka, Dariusz Biernacki
  2013
  http://www.ii.uni.wroc.pl/~mabi/papers/PPDP13.pdf

It describes the dynamic semantics of a small fragment of Ltac, focusing in particular on the subtle backtracking semantics of pattern-matching.

On Sun, Mar 6, 2016 at 11:34 AM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 03/06/2016 09:52 AM, Matej Kosik 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".

I also don't understand what is meant here.  Is it to facilitate wider direct use of tactics by humans?  Or is it about creating some new type of proof automation based on formal descriptions of tactics?  Or is it somehow about the existing proof automation tactics, such as auto and eauto?

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.

That's an interesting question in itself: What would be a useful presentation of tactics beyond Chapter 8 of the refman?  Do people want such a thing?

IMHO, refman chapter 8 is pretty good, but could be better.  For instance, why are there so many case analysis tactics, and how do they differ?  The only way to find out currently is by experimenting.

-- Jonathan