I am a little bit perplex by the following. I have a case of the
reflexivity tactic, over a user-defined relation, that loops.
So far this is not so surprising, but if I sketch the situation, it goes as follow:
rel1 rel2 x x.
Reflexive rel2 -> Reflexive (rel1 rel2)
So surely it should not be an issue and yet it loops. And indeed, if instead of my
Equivalence instance for
rel2 I explicitly define a
Reflexive instance, the tactic works instantaneously.
This got me confused, so as usually I fired up the debug mode for typeclasses to see where the resolution gets stuck. But if I trace it after a couple of second of search, I have the extremely short trees that leads it to searching for
Reflexive rel2, at which point it should be able to conclude by deriving from the
Equivalence but instead, as far as I can see, it hangs in there, computing very hard, but without exploring anything else.
I am unsure how to proceed from there. Would anyone have an idea? It is a bit tricky to extract a minimal example from my context unfortunately.
Set Debug Tactic Unification to see if the problem is with unification instead of TC search itself.
Thanks for the suggestion, this seems promising indeed! I'm gonna stare a bit at this output to try to understand what's going on now.
Agree with Janno; but also, what about Typeclasses Opaque rel2?
I'd suspect @Janno thought of that and discarded the idea for some clever reason but not sure why. And it's probably quick to try:
No, I hadn't thought that far. I would need to see the debug output to come up with the next step. If
Typeclass Opaque helps I would suspect it only hides a problem somewhere in unification.
Sorry for getting back to this so late, but as @Janno suggested, it is indeed an issue of unification: an Equivalence instance for another relation leads to a unification problem that takes close to a full minute to fail...
Is there any trick to work around such issue?
Does the unification succeed?
Oh, sorry, just saw "fail"
It depends on the exact unification problem
I would be interested in seeing what terms take so long to be (not) unified.
I can clean up a bit and point you to it if you are interested, but beware that it is in the middle of an ongoing development (recent though so it's quite small right now)
Alright, the original repo is currently private (we'll open it as soon as we're somewhat stable), so I extracted as minimally as possible the issue over here: https://gitlab.inria.fr/yzakowsk/ctrees/-/tree/master/theories
coq-itree from opam if I have not forgotten anything. Then
dune build from root will do the trick.
The issue with unification is minimally explained and illustrated in the file
Unification_issue.v. Any advice is warmly welcome :)
Alright it appears that the unification gets completely lost in the lattices parameterizing the greatest fixed-point construction (the "companion") from the
coq-coinduction library. Damien Pous, author of the library, gave a shot at hiding aggressively this companion (
t in the library) by wrapping it under an identity made opaque in a module, and it completely solves the problem, unification and hence type class resolution is instantaneous again.
The new question would then be: is there a better way to prevent unification from going under a definition that cannot be Qeded?
if it's a type/proposition you can wrap it in a record instead of identity
Ah interesting I'll give it a try, thanks!
Although stopping to think about it, it is not a type/prop so that cannot work there
You can still wrap it into an inductive box though, à la
Inductive box (A : Type) := Box : A -> box A. You'll get a isomorphism that is definitional in only one direction, and you can leverage that to block unification.
Stdpp and math-comp both have general sealing constructions
Those give you a propositional equality without the definitional one, and can be placed at abstraction boundaries somewhat eagerly.
that is, at least, more eagerly than "after debugging a concrete problem". OTOH, choosing the right boundaries is hard.
Ah thanks for the remark Pierre-Marie !
@Paolo Giarrusso Would you have a pointer at hand to this mechanism in either of the libraries by any chance?
Oh it was easy to find, sorry for the bother: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/base.v#L53
Thanks for the pointer!
On picking boundaries I'll quote @Jason Gross :
Pick good abstraction barriers, and respect them religiously. You will pay in sweat and tears every single time you break an abstraction barrier. (Picking good abstraction barriers is incredibly hard. Usually I do this by copying existing mathematical abstractions or published papers. I've managed to generate a good abstraction barrier entirely from scratch, in some sense, exactly once in the past five years. The abstraction barrier, in hindsight, can be described with the "insight" that "when writing C-like code, every function takes one tuple as an argument and returns one tuple as a result.")
For math-comp the keyword is "locked" but I'm less familiar with it.
For stdpp, you'll want to see and copy the "sealing dance"...
Basically, 4 lines like these: https://gitlab.mpi-sws.org/iris/iris/-/blob/fb763c47054ce8493606d7965000796858bbd990/iris/algebra/ofe.v#L333
that’s not actually easy, but the pattern is regular enough that we treat it as a language construct. Somebody less patient could probably implement that as an elpi command.
Ah, I see. Thanks a lot, that looks like a great solution, I'll test that Tomorrow!
FWIW: sometimes the math-comp thing looks less verbose to define, and I’m not really sure of the tradeoffs. You’ll have to tag somebody else for that. But I can say from experience that the stdpp one works well.
Here an example of module based locking https://github.com/math-comp/hierarchy-builder/wiki/Locking
It is not specific to HB so I can move it to elpi proper if there is user request.
Matchomp has other mechanisms as well, shorter but less robust.
That looks cool! But I guess it would not work in sections, right?
OTOH, that's unavoidable if you truly want "no body at all", as opposed to a body in hnf.
Indeed, that is why other locking mechanisms exist. For reference https://github.com/coq/coq/blob/e9c122360362d12a06897d038450544ad3efdc1f/theories/ssr/ssreflect.v#L373
Oh, had forgotten about those problems...
Wonder if @Ralf Jung / @Robbert Krebbers would also be interested in using your locking.
@Yannick Zakowski have you tried using
Typeclasses Opaque instead of the module based locking? In my experience the first suffices to block typeclass search from unfolding the definition and is more lightweight. But I would be interested in cases where one actually needs to use module based locking.
I haven't tried no, but that sounds like the lightest solution if it works indeed! Thanks everyone, I'm gonna experiment with these various options
After a quick try,
Typeclasses Opaque appears to do the trick! I need to test it further, but that sounds great.
TC opaque should work well for TC resolution, the rest can matter for (failing) attempts like apply.
Paolo Giarrusso said:
Wonder if Ralf Jung / Robbert Krebbers would also be interested in using your locking.
We've looked at these methods in the distant past, but it seemed that we typically need:
simpl. For that
Typeclasses Opaqueor our
tc_opaquetrick (https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/base.v#L93) suffices.
sealtrick (https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/base.v#L52). At https://github.com/math-comp/hierarchy-builder/wiki/Locking I see that module based locking can now be done compactly using
HB.lock; we should look into that.
HB.lock looks amazing! I have no idea how
HB.lock Definition new_concept := 999999 even parses, but this looks like exactly the interface I always wanted for this.
ah I guess it uses elpi for metaprogramming. nice. unfortunately I cannot make heads or tails of the implementation^^
OK, let me move it to elpi proper and document it (both internally and externally), it won't hurt and after all it has nothing to do with HB.
APIs are simple, the ones used here imitate vernacular commands, so once I remove the HB boilerplate (the logging) I'm sure the code will be trivial to follow.
About the syntax, elpi commands can take in input Coq declarations:
HB.lock is the command name, while
Definition ... is an argument the command received and elaborates to modules (signature and body) and a definition in there plus a notation. This is key to HB, since most commands receive records in input, and there was little point in reinventing a syntax for it.
yeah the syntax of using it looks very nice
but for elpi I clearly need to read some kind of tutorial.
lock-def Name AritySkel BoSkel :- std.do! [ is gibberish to me^^. probably this is because I never used prolog or any language of that family.
I am surprised that something as imperative as extending coq with more definitions can be expressed as a logic program
I wrote a few tutorials and examples, but it takes some time to read them.
Logic programming plays little role in the
HB.lock program. Logic programming is key to manipulate syntax trees with binders and holes (evars) concisely, while in
HB.lock the only thing you see is a bunch of APIs and a few combinators like
std.do! which literally says: I'm not interested in backtracking and the like, do this and never look back!
:+1: on the upstreaming, unsurprisingly we'd also like this.
Last updated: Sep 30 2023 at 05:01 UTC