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."
does shelve
"solve" a goal? I thought it didn't
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.
I'm precisely trying to have only one shelf
I thought postponing was done by give_up
let's forget about the implementation
you'd expect 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 foo
shelves
Gaëtan Gilbert said:
I think of
solve foo
likefoo; fail
which succeeds iffoo
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.
I see, makes sense!
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.
I infer that unshelve tac
only unshelves goals shelved by tac
right? (and not pre-existing ones)
That's correct.
Last updated: Oct 13 2024 at 01:02 UTC