Hello. I have an Equations?
definition inside a section, and it generates an obligation that is solved without relying on all of the section variables, but the obligation still abstracts over it for some reason.
I end up with some fun (_ : some type) =>
at the head of the obligation which is unfortunate, especially since I would like to avoid my definition to depend on this argument.
Is there something similar to the trick used with Proof
to limit which section variables my Equations definition can use?
Idea: Does Set Default Proof Using
have an effect?
Good idea but
Warning: There is no option Default Proof Using
Thanks, it was worth a try.
hm, I didn't give the full syntax; try Set Default Proof Using "Type".
that _is_ a valid command, which makes Proof
mean Proof using Type.
the question is whether it affects obligations.
I did not use the quotations I see!
I tried using Equations?
in combination with Proof using
but for some reason, it sill depends on stuff I do not mention (and which is not added by a dependency).
I can't manage to make it work with Set Default Proof Using
. I restrict it, the unrestrict it by using Set Default Proof Using
again with all the section variables, but then all definitions the depend on the extra ones fail…
In any case, if I close the section after my definition, it still depends on the section variables it should not.
It might have to do that, even when using Equations?
the goals are still obligations under the hood (at least, they are still named as such).
Just for debugging, can you throw in Obligation Tactic := idtac. ?
(You then need to call by hand the default one, shown with Show Obligation Tactic.)
Otherwise, there might be obligations that you don’t see.
Actually, before that:
I wonder which of the obligations have the spurious dependencies - all of them, or just some ones (say, ones not solved in proof mode).
But I’ll stop now, and leave this to people who understand more details
Salut @Théo Winterhalter , indeed there could be several causes for this problem, obligations savings is taken care by Coq these days. In the past there use to be a quite tricky codepath, but in master
you have now a unified declaration path; in vernac/declare.ml
Still equations does deviate quite a bit, but should be easy to fix if you wanna have a look.
I will be happy to help.
The other branches do not depend on the extra variables no. I may in a weird case. I think the easiest would be to refactor to have the variables declared after the definition.
Thanks @Emilio Jesús Gallego Arias, I don't know if I'll have the time to give it a look in the near future. I'm using Coq 8.11 so it's not even the latest version of Equations, maybe this stuff have changed I don't know.
Thanks guys in any case! :)
Only if you have a non-minimized version online, can you maybe post a link/file a brief issue, in case somebody wants/can to take a look?
Yeah I'll try to see if I can minimize it. For now, I will have a direct link to the commit where I have the issue. https://github.com/TheoWinterhalter/template-coq/blob/88050719550ad38ca7a2e13068210bd3a3445f5b/pcuic/theories/PCUICParallelReductionConfluence.v#L1205
Last updated: May 28 2023 at 18:29 UTC