Tactic for repetetive cases

Stream: lean4

[Henrik Böving]

When I'm doing a tactic proof like:

cases foo with
| a => tac1; BigTacBlob
| b => tc2; BigTacBlob

So a case split followed by some preparator argument followed both times by the same large tactic blob to close the remaining goal. Do we have a tactic that makes me not copy paste the big tactic blob?

[Eric Rodriguez]

I think you can do [a; b] <;> BigTacBlob

[Henrik Böving]

How do those [] work?

[Arthur Adjedj]

According to the docs:

t <;> [t1; t2; ...; tn] focuses on the first goal and applies t, which should result in n subgoals. It then applies each ti to the corresponding goal and collects the resulting subgoals.

[Henrik Böving]

Aha I see it doesn't work just like that it needs a leading <;> :thumbs_up:

[Ruben Van de Velde]

I think there's also case' which doesn't require that you solve the case

[Kyle Miller]

Ruben's suggestion would be

cases foo
case' a => tac1
case' b => tac2
all_goals BigTacBlob

[Kyle Miller]

I think cases (and induction) has syntax for running tactics at the start of each case, like

cases foo with PreTacBlob
| a => tac1
| b => tac2

I wonder if there could be some nice syntax for tactics and the end of each case? This question of how to run some tactics at the end of each remaining case has come up before.

[Mario Carneiro]

The syntax I have been hoping for here is to allow ?_ at the end of a tactic block to "escape" it and send the subgoal out into the parent context. Currently cases and induction already support this but only if ?_ is the only thing in the tactic block, cases foo with | a => tac; ?_ doesn't work

[Mario Carneiro]

I think it would be useful to have that as a general mechanism in tactics though, including combinators like . tac

[Yaël Dillies]

I have been wanting this too!

[Kyle Miller]

Here's a small proposal for this:

The defer or defer foo tactic discards the main goal and defers solving for it to an outer context. The first preserves the goal tag, and the second changes the goal tag to foo.

Implementation idea 1: this ensures the goal is a synthetic opaque metavariable and then simply drops it off the goal list. Each tactic that can handle this situation (like refine and have) is responsible for looking through the proof term at the end of the block, collecting unsolved such variables, and adding them to the goal list.

Implementation idea 1.5: add a table of deferred goals to the elaborator state (like other tables of synthetic metavariables) to register which goals have been deferred. This way, at the end of elaboration, nicer error messages can be created than a generic "expression contains metavariables".

Implementation idea 2: have the tactic framework manage a list of pending deferred metavariables, and having scoping constructs similar to withSynthesize to collect newly created ones. Make all ?foo variables register themselves as deferred metavariables, and have refine work with this, rather than scouring the expression for new synthetic opaque metavariables.

[Patrick Massot]

Kyle, is this related to the discussion at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/An.20.60exists_intro.60.20tactic.3F/near/411262030?

[Kyle Miller]

It looks like I should read the Procrastination manual

[Mario Carneiro]

Note that the ?_ idea is not the same as procrastination / defer, it is less powerful and in particular structurally cannot drop goals, it only transfers goals from a block to its direct parent. I think you can use it for defer-like behavior but you may need to pull a goal out of several nested blocks for that, and you wouldn't be able to move a goal out of a nested by block at all. That all means that ?_ has a much more local behavior than defer, but also makes it less suitable for the procrastination use-cases

[Kyle Miller]

The defer I was proposing was just for deferring to direct parents too, as a sort of generalization of how refine collects goals "deferred" by using ?foo notation, but it could also work for deferring out of a nested by.

[Kyle Miller]

I'm guessing the implementation of your suggestion that you had in mind would be that tacticSeq could end with a ?_, and tactics could be aware of this?

[Mario Carneiro]

yes, basically runTacticSeq would be aware of it and any tactics using it would change to accomodate it

[Mario Carneiro]

refine doesn't collect ?foo from direct subterms only though, it will pull them anywhere in the term

[Mario Carneiro]

procrastination seems to have a much more goto-like behavior where you can just make goals disappear wherever you want and rescue them at any later point before the end of the proof

[Kyle Miller]

I'm not sure what you're correcting about refine

[Mario Carneiro]

what I mean is that the "analogue of refine" would be able to defer goals like this:

defer
  . bla
    case a =>
      cases b with
      | foo => bar; ?jump
with
  jump => ...

[Mario Carneiro]

The variation using ?_ goals would look like this:

. bla
  case a =>
    cases b with
    | foo => bar; ?_
    ?_
  ?jump
case jump => ...

[Mario Carneiro]

which is to say, popping several layers of parents is cumbersome and really visible

[Kyle Miller]

What I was suggesting is that tactics like cases could evaluate their tactic blocks then use the refine-like algorithm for collecting metavariables from the resulting proof term, so it would look like your second example

[Kyle Miller]

but of course there could be some sort of scoping tactic that could do refine for a whole tactic block, and have a mechanism to drop goals that will definitely be recovered by that scoping tactic (let's assume there's a flag that the dropping-a-goal tactic could check to see if inside such a scoping tactic). It could create new goals you handle with case, rather than needing a with clause.

[Mario Carneiro]

sure, I was making up syntax

[Mario Carneiro]

and option number 3 is full procrastination, what I called "goto-like":

. bla
  case a =>
    cases b with
    | foo => bar; shelve ?jump
unshelve jump => ...

with the difference being that the unshelve command can occur anywhere in the proof after shelve, even inside a subproof