The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Dear Coq Club,

I am experimenting with using dependently typed records (and canonical 
structures) to axiomatize a small hierarchy of logics (logic of bunched 
implications, with some extensions, like step-indexing via the later 
modality). The purpose of this hierarchy is to abstractly prove results 
about arbitrary logics and build tactics/proof automation for said logics.

I tried to represent my little hierarchy using a couple of approaches, 
namely:

1. Packed classes using mixins (as in Ssreflect)
2. Telescopes (as in CORN)
3. Packed classes without mixins

Unfortunately, using each of these approaches, I ran into issues with 
the apply tactic becoming very slow (exponential, or worse, in the size 
of the goal).

I have included simplified versions of all approaches as attachments. As 
you see, the third approach (file apply_bug.v) is the worst in terms of 
performance, but whenever I make the term big enough (but still much 
smaller than the kind of goals you will see in practice), the 
performance of all approaches becomes totally useless at some point.

Does anyone have an idea whether I am running into an actual efficiency 
bug of records in combination with the apply tactic or unification here, 
or whether I am in fact doing something very inefficient.

I noticed that when enabling primitive projections the performance 
programs go away entirely in my small examples (all uses of apply will 
fail within ~0.00 seconds). Unfortunately, in my actual development, 
primitive projections seem to cause other problems: canonical structure 
inference no longer works when they are enabled, and the Ssreflect 
rewrite tactic to fail unexpectedly. Are these problems known?

Suggestions on avoiding this issue are very welcome!

Thanks,

Robbert

Attachment: apply_bug.v
Description: application/coq

Attachment: apply_bug_mixins.v
Description: application/coq

Attachment: apply_bug_telescopes.v
Description: application/coq