The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello Xavier,

You're raising an important issue, and I guess most users and developers 
agree that basic Coq tactics desperately need some love.

I see two main reasons why this is not happening more:
- The usual argument: the academic system does not reward such work as 
it is very hard to publish. So spending time on it, at least for young 
researchers, is very risky due to peer pressure to publish, and the low 
number of positions.
- Some well thought design decisions were already taken and implemented 
in ssreflect's tactics, which leaves little incentive to re-implement them.

Rewrite illustrates very well this second point. As others were saying, 
for efficiency reasons you don't always want to work up to full 
conversion (conversion of the rewrite statement, conversion in the 
goal). Careful design made it possible to retain efficiency, locality of 
failure and predictability. It's fully implemented and documented in 
ssr's manual and in a paper : "A Language of Patterns for Subterm 
Selection", Georges Gonthier and Enrico Tassi, ITP 2012.

What is there more to do on Coq's side, which will not consists in 
plagiarizing the code, importing incomplete sets of features incrementally?

My personal way of minimizing pain is to use ssreflect's tactics in 
combination with some of Coq's higher level ones when required.

Omega's example is of a very different nature, because an easy fix is 
probably indeed doable. In the long term though, it would also deserve 
an abstract interface à la ring instead of hard-coding the type of integers.

Maxime.

On 07/31/2014 12:48 PM, Xavier Leroy wrote:
> Apologies for being probably naive and definitely heavy-handed with 
> this issue, but I strongly feel that a number of basic tactics of Coq 
> could use some love. That they have been clunky for the last two 
> decades and that power users learned to work around this clunkiness is 
> no reason for status quo. - Xavier