Stream: Coq devs & plugin devs

Topic: Semantics of assert by

Maxime Dénès (Jun 11 2020 at 17:40):

Is it expected that assert False by shelve succeeds?

Maxime Dénès (Jun 11 2020 at 17:40):

The doc says "This tactic behaves like assert but applies tactic to solve the subgoals generated by assert."

Maxime Dénès (Jun 11 2020 at 17:40):

does shelve "solve" a goal? I thought it didn't

Enrico Tassi (Jun 11 2020 at 17:48):

I guess its postponed. I guess the interaction of shelve with solve was not "carefully designed" ;-) In particular I think that at least one shelf is global; I could imagine a semantics of solve + local-shelf (inner shelf must be empty for solve to succeed), but if the shelf is outside solve, then I really don't know what solve means.

Maxime Dénès (Jun 11 2020 at 17:53):

I'm precisely trying to have only one shelf

Maxime Dénès (Jun 11 2020 at 17:53):

I thought postponing was done by give_up

Maxime Dénès (Jun 11 2020 at 17:53):

let's forget about the implementation

Maxime Dénès (Jun 11 2020 at 17:54):

you'd expect solve to fail if the underlying tactic has generated subgoals, even if they were shelved, wouldn't you?

Enrico Tassi (Jun 11 2020 at 18:07):

give_up is like admit, you cannot resume proving the goal. My understanding of the shelf can be explained in the LCF type of tactics goal -> goal list. There you have no choice, either you declare your subgoal or it becomes dangling. Here we have goal * goal list -> goal list * goal list where the second list is the shelf. Given that solve was there before the shelf, solve tac g checks for the fist list returned by tac g to be empty. You may as well check that the second list did not change, or got shorter.

Enrico Tassi (Jun 11 2020 at 18:09):

But "not change" is hard to test, since one may for example prune a shelved goal, and that may (or may not) update the shelf is a syntactic way (the semantic would be the same, it is still the same proof hole, but may be hard to recognize as such). I hope it helps.

Gaëtan Gilbert (Jun 11 2020 at 18:16):

I think of solve foo like foo; fail which succeeds if foo shelves

Matthieu Sozeau (Jun 12 2020 at 12:30):

Gaëtan Gilbert said:

I think of solve foo like foo; fail which succeeds if foo shelves

Same here. I would think [solve] does not look at the shelved subgoals by default. Of course solve [unshelve tac] should fail if tac shelved something on its own.

Maxime Dénès (Jun 12 2020 at 12:31):

I see, makes sense!

Cyril Cohen (Jun 12 2020 at 12:48):

In math-comp analysis, I think it would completely break uses of the tactics near if by (which uses solve) did not succeed even when goals are shelved.
Thanks @Matthieu Sozeau for giving the solve [unshelve tac] alternative if we want to assert no goals were shelved in the process, I was going to ask how to do this nicely.

Enrico Tassi (Jun 12 2020 at 13:19):

I infer that unshelve tac only unshelves goals shelved by tac right? (and not pre-existing ones)

Théo Zimmermann (Jun 12 2020 at 13:20):

That's correct.

Last updated: Oct 13 2024 at 01:02 UTC