The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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