Is it expected that
assert False by shelve succeeds?
The doc says "This tactic behaves like assert but applies tactic to solve the subgoals generated by assert."
shelve "solve" a goal? I thought it didn't
I guess its postponed. I guess the interaction of
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
I'm precisely trying to have only one shelf
I thought postponing was done by
let's forget about the implementation
solve to fail if the underlying tactic has generated subgoals, even if they were shelved, wouldn't you?
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.
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.
I think of
solve foo like
foo; fail which succeeds if
Gaëtan Gilbert said:
I think of
foo; failwhich succeeds if
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.
I see, makes sense!
In math-comp analysis, I think it would completely break uses of the tactics
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.
I infer that
unshelve tac only unshelves goals shelved by
tac right? (and not pre-existing ones)
Last updated: Oct 16 2021 at 02:03 UTC