Stream: Equations devs & users

Topic: Obligation abstracting over unnecessary section variables


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

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 16:19):

Idea: Does Set Default Proof Using have an effect?

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

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 16:26):

hm, I didn't give the full syntax; try Set Default Proof Using "Type".

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 16:27):

that _is_ a valid command, which makes Proof mean Proof using Type.

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 16:27):

the question is whether it affects obligations.

view this post on Zulip Théo Winterhalter (Jul 04 2020 at 16:57):

I did not use the quotations I see!

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

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

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

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 17:54):

Just for debugging, can you throw in Obligation Tactic := idtac. ?

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 17:55):

(You then need to call by hand the default one, shown with Show Obligation Tactic.)

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 17:56):

Otherwise, there might be obligations that you don’t see.

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 17:56):

Actually, before that:

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

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 17:58):

But I’ll stop now, and leave this to people who understand more details

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2020 at 18:17):

I will be happy to help.

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

view this post on Zulip Théo Winterhalter (Jul 04 2020 at 19:09):

Thanks guys in any case! :)

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

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