Stream: Coq users

Topic: ✔ Ltac: push internal subgoal to the user


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Ana de Almeida Borges (Jan 03 2023 at 14:22):

Oh, or perhaps last <cleaning stuff> suffices

view this post on Zulip 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>

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:

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.

view this post on Zulip 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>].

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 08:33):

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

view this post on Zulip Julien Puydt (Jan 04 2023 at 08:38):

Ha! That's it! Thanks!

view this post on Zulip Notification Bot (Jan 04 2023 at 08:38):

Julien Puydt has marked this topic as resolved.

view this post on Zulip 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).

view this post on Zulip 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: Jun 23 2024 at 23:01 UTC