Hi,
Post by Christian Doczkal(...)
Indeed, teaching is one reason why it might be good if Coq where to ship
with some easy to use reflection mechanism supporting, like quote does,
simple data types and foreign subterms.
When I am teaching reflection, I usually show (and ask in related exercises) a
small Ltac function performing the reification phase. I think it is helpful to
see the pattern matching at work, and possibly also the construction of the
varmap, as opposed to having a "black box" command like Quote. Plus on a simple
toy example, it is really not that difficult to implement.
Post by Christian DoczkalSo keeping quote and developing it to the point where the reflective
tactics shipped with Coq (can) make use of it, might be worthwhile.
When implementing the ring tactic a while ago, we briefly considered using it,
but eventually fall back to some specific OCaml code. I do not remember the details.
I wholeheartedly agree that the lack of code sharing among Coq reflexive tactics
is very unfortunate. Performance and customization are a delicate issue though.
On the other hand, I do not know what is the best candidate for the purpose of a
"generic and efficient refication toolkit". Maybe not the Quote plugin I would say.
If I understand correctly the survey by Jason and his co-authors, the
pattern-based technique they propose does not deal with variable maps. Thus it
cannot be used for reflective tactics à la ring.
And therefore the problem of constructing a variable map is out of the scope of
their benchamrk.
Some of the meta programming solution they benchmark can be used in this case
(canonical structures, type classes, etc.) and could in principle be used for
this purpose. But performance is an issue on large terms, in particular in the
variable map building phase.
Post by Christian Doczkal(...)
The, closely related, question that got me interested in this is: What
is currently the simplest way to do reification into ones own
inductively defined data type (with variables) in such a way that the
variable map containing the foreign subterms is injective not just with
respect to syntactic equality but with respect to conversion.
I am also interested, and I do not know the answer.
For instance, this would help interfacing automation tactics with a
canonical-structure based hierarchy of structures. But again, building a
variable map up to conversion too naively can trigger massive performance
problems. A while ago, we ran into this nature of problems when trying to prove
identities on rational numbers represented as a pair of unary integers with a
proof. The solution involves using an opaque cast as a head symbol on constant,
and a specific tactic parameter to deal with the leaves of a given expression.
Best,
assia
Post by Christian DoczkalBest,
Christian
Post by Hugo HerbelinHi,
Somehow, a question is also whether it would be worth that someone
eventually provides a generic-enough quote function in Coq, for use at
both the vernac level or the plugin level.
My understanding of the Gross-Erbsen-Chlipala ITP 2018
reification-by-parametricity paper is that this quote function almost
already exists, it is "pattern". Then, what about going in the
direction of providing a variant of "pattern" which encapsulates the
boilerplate of the technique and which, maybe, also abstracts over the
foreign subterms?
Idem at the plugin level. Already e.g. ring, micromega, btauto have
their own reification mechanisms (sometimes even in Ltac) and this
seems suboptimal.
Best,
Hugo
Post by John WiegleyI would also support dropping Quote; each time I've been able to use it, I
ended up just copying Ltac macros from existing templates so I would have the
configurability needed for future changes.
I definitely support getting rid of Quote. I used it once and then ran into an
issue: my unquote function took a type parameter, which is unsupported, even if
you try specializing it. I talked to Jason Gross, copied some code from their
reification-by-parametricity paper, and got it working fairly easily in pure
Ltac.
It would be great to have some examples from that paper coped into the Coq test
suite and try to give it visibility, instead of maintaining Quote. It's a more
powerful technique and I believe with just a little boilerplate can replace
uses of Quote (if anybody actually weighs in and is using it).
Dear Coq-clubbers,
I'm trying to clean up the set of plugins shipped with Coq, so that we
can make the maintenance done by the development team more focused and
effective.
I was wondering if anybody was using the Quote plugin in real-world
developments. See https://github.com/coq/coq/pull/7894 for more context.
Thank you in advance for your feedback!
Maxime.