coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] multiple typeclass instance question
- Date: Fri, 11 Mar 2016 16:44:36 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f47.google.com
- Ironport-phdr: 9a23:ViX8hhaxZDkNzzEatzK2zsD/LSx+4OfEezUN459isYplN5qZpci7bnLW6fgltlLVR4KTs6sC0LqJ9fCxEjVcud6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDtvc2CKFwU3HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzA0lRxBHwjM6lneU5bvvy3m/r5/3y+bPsDyQL0cVjGr7qMtQxjt3nRUfwUl+X3a35QjxJlQpwis8kRy
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
- Re: [Coq-Club] multiple typeclass instance question, (continued)
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/11/2016
- Re: [Coq-Club] multiple typeclass instance question, Pierre-Marie Pédrot, 03/12/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/16/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/16/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/16/2016
Archive powered by MHonArc 2.6.18.