Yannick Zakowski (Oct 14 2021 at 11:34): Yannick Zakowski (Oct 14 2021 at 11:34):Hello,
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)Equivalence rel2So 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.
Janno (Oct 14 2021 at 13:43):Try Set Debug Tactic Unification to see if the problem is with unification instead of TC search itself.
Yannick Zakowski (Oct 14 2021 at 13:54):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.
Paolo Giarrusso (Oct 14 2021 at 20:16):Agree with Janno; but also, what about Typeclasses Opaque rel2?
Paolo Giarrusso (Oct 14 2021 at 20:18):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:
Janno (Oct 15 2021 at 06:39):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.
Yannick Zakowski (Oct 26 2021 at 11:00):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?
Janno (Oct 26 2021 at 11:00):Does the unification succeed?
Janno (Oct 26 2021 at 11:00):Oh, sorry, just saw "fail"
Janno (Oct 26 2021 at 11:02):It depends on the exact unification problem
Janno (Oct 26 2021 at 11:02):I would be interested in seeing what terms take so long to be (not) unified.
Yannick Zakowski (Oct 26 2021 at 11:05):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)
Yannick Zakowski (Oct 26 2021 at 11:38):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
Compiling requires coq-coinduction and 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 :)
Yannick Zakowski (Oct 26 2021 at 16:09):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.
Yannick Zakowski (Oct 26 2021 at 16:09):The new question would then be: is there a better way to prevent unification from going under a definition that cannot be Qeded?
Li-yao (Oct 26 2021 at 16:28):if it's a type/proposition you can wrap it in a record instead of identity
Yannick Zakowski (Oct 26 2021 at 16:49):Ah interesting I'll give it a try, thanks!
Yannick Zakowski (Oct 26 2021 at 17:20):Although stopping to think about it, it is not a type/prop so that cannot work there
Pierre-Marie Pédrot (Oct 26 2021 at 17:27):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.
Paolo Giarrusso (Oct 26 2021 at 20:49):Stdpp and math-comp both have general sealing constructions
Paolo Giarrusso (Oct 26 2021 at 20:50):Those give you a propositional equality without the definitional one, and can be placed at abstraction boundaries somewhat eagerly.
Paolo Giarrusso (Oct 26 2021 at 20:51):that is, at least, more eagerly than "after debugging a concrete problem". OTOH, choosing the right boundaries is hard.
Yannick Zakowski (Oct 26 2021 at 20:52):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?
Yannick Zakowski (Oct 26 2021 at 20:53):Oh it was easy to find, sorry for the bother: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/base.v#L53
Yannick Zakowski (Oct 26 2021 at 20:53):Thanks for the pointer!
Paolo Giarrusso (Oct 26 2021 at 20:53):On picking boundaries I'll quote @Jason Gross :
https://stackoverflow.com/a/46138499/53974
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.")
Paolo Giarrusso (Oct 26 2021 at 20:54):For math-comp the keyword is "locked" but I'm less familiar with it.
Paolo Giarrusso (Oct 26 2021 at 20:54):For stdpp, you'll want to see and copy the "sealing dance"...
Paolo Giarrusso (Oct 26 2021 at 20:56):Basically, 4 lines like these: https://gitlab.mpi-sws.org/iris/iris/-/blob/fb763c47054ce8493606d7965000796858bbd990/iris/algebra/ofe.v#L333
Paolo Giarrusso (Oct 26 2021 at 20:57):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.
Yannick Zakowski (Oct 26 2021 at 20:58):Ah, I see. Thanks a lot, that looks like a great solution, I'll test that Tomorrow!
Paolo Giarrusso (Oct 26 2021 at 21:07):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.
Enrico Tassi (Oct 27 2021 at 05:30):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.
Paolo Giarrusso (Oct 27 2021 at 06:15):That looks cool! But I guess it would not work in sections, right?
Paolo Giarrusso (Oct 27 2021 at 06:16):OTOH, that's unavoidable if you truly want "no body at all", as opposed to a body in hnf.
Enrico Tassi (Oct 27 2021 at 06:19):Indeed, that is why other locking mechanisms exist. For reference https://github.com/coq/coq/blob/e9c122360362d12a06897d038450544ad3efdc1f/theories/ssr/ssreflect.v#L373
Paolo Giarrusso (Oct 27 2021 at 06:26):Oh, had forgotten about those problems...
Paolo Giarrusso (Oct 27 2021 at 06:27):Wonder if @Ralf Jung / @Robbert Krebbers would also be interested in using your locking.
MackieLoeffel (Oct 27 2021 at 07:12):@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.
Yannick Zakowski (Oct 27 2021 at 07:22):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
Yannick Zakowski (Oct 27 2021 at 07:41):After a quick try, Typeclasses Opaque appears to do the trick! I need to test it further, but that sounds great.
Paolo Giarrusso (Oct 27 2021 at 07:51):TC opaque should work well for TC resolution, the rest can matter for (failing) attempts like apply.
Robbert Krebbers (Oct 27 2021 at 08:31):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 Arguments nosimpl suffices.Typeclasses Opaque or our tc_opaque trick (https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/base.v#L93) suffices.seal trick (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 usingHB.lock; we should look into that. Ralf Jung (Oct 27 2021 at 18:15):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.
Ralf Jung (Oct 27 2021 at 18:16):ah I guess it uses elpi for metaprogramming. nice. unfortunately I cannot make heads or tails of the implementation^^
Enrico Tassi (Oct 27 2021 at 19:43):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.
Ralf Jung (Oct 27 2021 at 20:06):yeah the syntax of using it looks very nice
Ralf Jung (Oct 27 2021 at 20:07):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.
Ralf Jung (Oct 27 2021 at 20:08):I am surprised that something as imperative as extending coq with more definitions can be expressed as a logic program
Enrico Tassi (Oct 27 2021 at 20:42):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!
Paolo Giarrusso (Oct 27 2021 at 23:07)::+1: on the upstreaming, unsurprisingly we'd also like this.
Last updated: Oct 13 2024 at 01:02 UTC