Janno (Dec 07 2020 at 14:15): Janno (Dec 07 2020 at 14:15):Is there a fast way to create an evar in Ltac2? I currently use open_constr:(_ : $type) but that incurs a huge cost if $type is not obviously a Type/Prop.
Pierre-Marie Pédrot (Dec 07 2020 at 14:23):Not that I know of. Note that for safety reason, even if we introduced such a function, it'd have to check that the type of the conclusion you provided it with is a sort.
Pierre-Marie Pédrot (Dec 07 2020 at 14:24):We can always provide also an unsafe function, but it's a bit dangerous.
Janno (Dec 07 2020 at 14:27):Unsafe is what I was hoping for. I already manage my universes manually so I might as well do the same with evars..
Gaëtan Gilbert (Dec 07 2020 at 14:34):open_constr:(_ : ltac:(exact_no_check $type)) or something based on it might work
if $type is obviously a type you probably get significantly more overhead though
Janno (Dec 08 2020 at 13:43):open_constr:(_ : ltac:(exact_no_check $type)) or something based on it might work
This does indeed speed things up. Thanks a lot!
Janno (Dec 08 2020 at 13:45):I have another question. It seems that the open_constr trick is flawed because the evar doesn't actually include the goal's hypotheses. (E.g. making the evar into a goal with Control.new_goal and running typeclasses_eauto on it will fail to select instances from the hypotheses.) But I cannot find another way to get an evar of a given type using the existing Ltac2 primitives. Am I missing something?
Pierre-Marie Pédrot (Dec 08 2020 at 13:46):Ltac2 misses a lot of primitives, so if you find one you deem useful, do not hesitate to open an issue.
Pierre-Marie Pédrot (Dec 08 2020 at 13:46):I shall write a bunch for the next release now that we start to have a consistent base of users.
Janno (Dec 08 2020 at 13:49):I didn't mean it like "this should exist" (although I wish it did exist as a proper primitive) but more like "can anybody think of a workaround?"
Pierre-Marie Pédrot (Dec 08 2020 at 13:52):Are you sure you're calling the open_constr thunk at the right moment?
Pierre-Marie Pédrot (Dec 08 2020 at 13:52):AFAIR it should include all the current variables
Pierre-Marie Pédrot (Dec 08 2020 at 13:54):I am in the middle of a horrible struggle with let-bindings inside inductive arities in a branch of mine so I cannot test, but I'd expect it to be the case.
Janno (Dec 08 2020 at 14:17):I am not so sure any more what is going on. The evar has all hypotheses in its instance. I remembered that I could simply check that by printing it with Printing Existential Instances. The problem must be elsewhere. Sorry for the false alarm!
Janno (Dec 08 2020 at 14:26):(The problem seems to be a bug in typeclasses_eauto.)
Janno (Dec 08 2020 at 14:41):@Pierre-Marie Pédrot you might actually know what's going on here since you worked on this stuff recently: https://github.com/coq/coq/issues/13600
Pierre-Marie Pédrot (Dec 08 2020 at 14:42):Oh, discriminated databases... I had almost managed to forget them.
Janno (Dec 08 2020 at 14:43):Same behavior without discriminated.
Pierre-Marie Pédrot (Dec 08 2020 at 14:45):As already answered in the issue, I think this is normal actually. What other behaviour could you implement?
Pierre-Marie Pédrot (Dec 08 2020 at 14:46):The union of transparent states is not commutative, just as the union of maps is not.
Théo Zimmermann (Dec 08 2020 at 14:49):This is BTW some issue limiting the creation of a Hint Union command.
Pierre-Marie Pédrot (Dec 08 2020 at 14:49):I think we have too much stuff in our hint databases. They grew out of practicality, but that limits the algebraic operations you can perform on them.
Janno (Dec 08 2020 at 14:53):I simply didn't read the documentation thoroughly. I wouldn't mind a more explicit user interface (an extra argument to typeclasses eauto that sets that db apart from the others) but you can only do so much when users don't read the docs :(
Théo Zimmermann (Dec 08 2020 at 14:56):Interestingly enough, the next tactic, autoapply only uses its (unique) database argument for the transparency information.
Last updated: Oct 03 2023 at 20:01 UTC