The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/11/2016 03:58 PM, Arnaud Spiwack wrote:
> I believe having the pretyper "in the tactic monad" is indeed the right way
> to go for increased modularity and expressiveness. Things like what
> Jonathan is looking at are validating this view, though it would seem that
> among the many Coq programmers, he is the sole customer for this type of
> things. On the other hand, if it helps tactic makers, I don't think most
> users need to be concerned about this sort of things.

I am not trying to be avant-garde.  It's just that once one has begun to 
rely on backtracking in 8.5, the various things that don't backtrack 
become somewhat annoying.  In this case, the real issue is that 
typeclass instance search only backtracks within each invocation of 
typeclasses eauto.  Hence, one cannot backtrack into an already solved 
instance search multimatch-style to provoke it into finding other 
instances.  I should have realized this before Jason pointed it out, as 
I had hit this limitation before with explicit invocations of the 
various auto tactics.  The ability to create a list of successes using 
the trick Jason shared is nice, but of limited usefulness with 
typeclasses because the trick requires an explicit tactic to turn the 
list into a "+" tactical expression.

Another case I hit frequently that doesn't backtrack to produce multiple 
successes is tactic-in-term, which was of course just introduced in 8.5.

So, the comparison of Coq's proof mode to logic programming is still not 
as strong as one would like.

-- Jonathan