Stream: Coq users

Topic: Creating evars in Ltac2


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Dec 07 2020 at 14:24):

We can always provide also an unsafe function, but it's a bit dangerous.

view this post on Zulip 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..

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?"

view this post on Zulip Pierre-Marie Pédrot (Dec 08 2020 at 13:52):

Are you sure you're calling the open_constr thunk at the right moment?

view this post on Zulip Pierre-Marie Pédrot (Dec 08 2020 at 13:52):

AFAIR it should include all the current variables

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Janno (Dec 08 2020 at 14:26):

(The problem seems to be a bug in typeclasses_eauto.)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Dec 08 2020 at 14:42):

Oh, discriminated databases... I had almost managed to forget them.

view this post on Zulip Janno (Dec 08 2020 at 14:43):

Same behavior without discriminated.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Dec 08 2020 at 14:49):

This is BTW some issue limiting the creation of a Hint Union command.

view this post on Zulip 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.

view this post on Zulip 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 :(

view this post on Zulip 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: Jan 29 2023 at 05:03 UTC