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?
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 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
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