Théo Winterhalter (Jul 04 2020 at 16:13): Théo Winterhalter (Jul 04 2020 at 16:13):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?
Paolo Giarrusso (Jul 04 2020 at 16:19):Idea: Does Set Default Proof Using have an effect?
Théo Winterhalter (Jul 04 2020 at 16:24):Good idea but
Warning: There is no option Default Proof Using
Thanks, it was worth a try.
Paolo Giarrusso (Jul 04 2020 at 16:26):hm, I didn't give the full syntax; try Set Default Proof Using "Type".
Paolo Giarrusso (Jul 04 2020 at 16:27):that _is_ a valid command, which makes Proof mean Proof using Type.
Paolo Giarrusso (Jul 04 2020 at 16:27):the question is whether it affects obligations.
Théo Winterhalter (Jul 04 2020 at 16:57):I did not use the quotations I see!
Théo Winterhalter (Jul 04 2020 at 17:02):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).
Théo Winterhalter (Jul 04 2020 at 17:13):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.
Théo Winterhalter (Jul 04 2020 at 17:16):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).
Paolo Giarrusso (Jul 04 2020 at 17:54):Just for debugging, can you throw in Obligation Tactic := idtac. ?
Paolo Giarrusso (Jul 04 2020 at 17:55):(You then need to call by hand the default one, shown with Show Obligation Tactic.)
Paolo Giarrusso (Jul 04 2020 at 17:56):Otherwise, there might be obligations that you don’t see.
Paolo Giarrusso (Jul 04 2020 at 17:56):Actually, before that:
Paolo Giarrusso (Jul 04 2020 at 17:57):I wonder which of the obligations have the spurious dependencies - all of them, or just some ones (say, ones not solved in proof mode).
Paolo Giarrusso (Jul 04 2020 at 17:58):But I’ll stop now, and leave this to people who understand more details
Emilio Jesús Gallego Arias (Jul 04 2020 at 18:14):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
Emilio Jesús Gallego Arias (Jul 04 2020 at 18:15):Still equations does deviate quite a bit, but should be easy to fix if you wanna have a look.
Emilio Jesús Gallego Arias (Jul 04 2020 at 18:17):I will be happy to help.
Théo Winterhalter (Jul 04 2020 at 19:07):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.
Théo Winterhalter (Jul 04 2020 at 19:09):Thanks guys in any case! :)
Paolo Giarrusso (Jul 04 2020 at 20:42):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?
Théo Winterhalter (Jul 04 2020 at 21:37):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: Sep 25 2023 at 12:01 UTC