The Coq mailing list

[周晓宇 <101005198 AT seu.edu.cn>]

Descriptions of the tactics in reference manual are informal. Even after 
reading the refman, I am not sure that I undersand the tatics thoroughly. I 
am not sure what I will get after applying a tactic in variant circumstances. 

So, if I want to define some domain specific tactics, I am not sure of the 
circumstances that it works.

So, I think a formal semantic of the tactics will help.

Zhou Xiaoyu


> -----原始邮件-----
> 发件人: "Jonathan Leivent" 
> <jonikelee AT gmail.com>
> 发送时间: 2016-03-07 00:34:02 (星期一)
> 收件人: 
> coq-club AT inria.fr
> 抄送: 
> 主题: Re: [Coq-Club] are there any formal descriptions of the tatics of Coq?
> 
> 
> 
> 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
> 
>