Stream: Coq users

Topic: ✔ Ltac: push internal subgoal to the user

Julien Puydt (Jan 03 2023 at 14:07):

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.

Ana de Almeida Borges (Jan 03 2023 at 14:22):

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?

Ana de Almeida Borges (Jan 03 2023 at 14:22):

Oh, or perhaps last <cleaning stuff> suffices

Julien Puydt (Jan 03 2023 at 14:30):

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>

Paolo Giarrusso (Jan 03 2023 at 17:06):

You can still use what the user proves before the proof is done, unless evars are involved

Paolo Giarrusso (Jan 03 2023 at 17:10):

"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.

Julien Puydt (Jan 04 2023 at 07:52):

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:

• either there's a way for me to make the user solve it already (how?);
• or I need to be able to push that subgoal aside (how?), do my cleaning stuff, and then push it forward again (how?).

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.

Paolo Giarrusso (Jan 04 2023 at 08:31):

ah, there is a way. You can write

Tactic Notation foo <arguments> ... :=
  <preparation>;
  assert whatever as H0;
  [apply: some_th | <cleaning stuff using H0>].

Paolo Giarrusso (Jan 04 2023 at 08:32):

basically, if tactic1 produces two goals, tactic1; [tactic2 | tactic3 ] will run tactic2 on the first and tactic3 on the second

Paolo Giarrusso (Jan 04 2023 at 08:33):

and in principle you can use have H0: whatever instead of assert whatever as H0...

Julien Puydt (Jan 04 2023 at 08:38):

Ha! That's it! Thanks!

Notification Bot (Jan 04 2023 at 08:38):

Julien Puydt has marked this topic as resolved.

Paolo Giarrusso (Jan 04 2023 at 08:40):

... 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).

Paolo Giarrusso (Jan 04 2023 at 08:41):

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 13 2024 at 01:02 UTC