I have some proof steps looking like this:
<preparation stuff, triggering a subgoal> <subgoal solving> <cleaning stuff>
and I would like to make it a new tactic ; unfortunately, I don't get how to turn to the user right in the middle of a tactic:
Tactic Notation foo <arguments> := match goal with | |- <whatever> => <preparation stuff> <ask to the user!> <cleaning stuff>
I don't want to pass the tactics to use to solve the subgoal as an argument: the user should solve the new subgoal interactively.
Can you do something like
<preparation stuff that creates a new subgoal>; last first; <cleaning stuff>; <somehow go back to the first subgoal>? Admittedly I'm not sure how to go back to the first subgoal, maybe something with goal selectors?
Oh, or perhaps
last <cleaning stuff> suffices
Hmmm... the cleaning step is using what the user has to prove ; and it's not a tactic to solve the goal but to advance it:
<start of preparation stuff> have H0: whatever. (* still preparation *) apply: some_th. (* still preparation *) idtac; (* here the user should work *) <cleaning stuff using H0>
You can still use what the user proves before the proof is done, unless evars are involved
"evar involved" = the statement of H0 contains evars so it isn't actually known until the user's done (ditto if you project info from
H0's proof, but
have doesn't support that). If that is the case, then you'll need to provide _two_ tactics to the user.
I don't understand how things would go.
I have a main goal, which my tactic will turn into an improved main goal, if the user treats some subgoal. So my tactic starts with the main goal, prepares things, applies a theorem and that makes the subgoal appear -- so far so good. It's at that point that I'm at a loss.
Indeed there are only two possibilities when the subgoal appears:
My tactic doesn't solve any goal ; it just pushes things around, and the user gets to solve a simple subgoal to improve the main goal.
ah, there is a way. You can write
Tactic Notation foo <arguments> ... := <preparation>; assert whatever as H0; [apply: some_th | <cleaning stuff using H0>].
tactic1 produces two goals,
tactic1; [tactic2 | tactic3 ] will run
tactic2 on the first and
tactic3 on the second
and in principle you can use
have H0: whatever instead of
assert whatever as H0...
Ha! That's it! Thanks!
Julien Puydt has marked this topic as resolved.
... found it: using ssreflect
have in automation risks running into https://github.com/coq/coq/issues/6687
(more examples in https://github.com/coq/coq/issues/10928).
especially since you'll likely want this to work even if
H0 exists, so you'd want
let H := fresh in assert ... as H; [ ... | ... H ... ].
Last updated: Oct 04 2023 at 18:01 UTC