The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT inria.fr>]

Hi,

Le 31/07/2018 à 14:43, Christian Doczkal a écrit :
> (...)
> 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.

> So 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.

> (...)
> 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

> Best,
> Christian
> 
> On 22/07/18 11:35, Hugo Herbelin wrote:
>> Hi,
>>
>> 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
>>
>> On Fri, Jul 20, 2018 at 11:45:32AM -0700, John Wiegley wrote:
>>> I 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.
>>
>> On Fri, Jul 20, 2018 at 08:41:28AM -0400, Tej Chajed wrote:
>>> 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).
>>>
>>> On Fri, Jul 20, 2018 at 3:20 AM Maxime Dénès 
>>> <mail AT maximedenes.fr>
>>>  wrote:
>>>
>>>     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.
>>>