Is it possible for `first` to remember the tactic it chose?

Stream: general

[Daniel Sainati]

I am writing a macro that looks like the following, where I have some function foo that takes a proof and another argument:

 `(tactic|
      first
        | apply foo (by tactic_1) (arg_1)
        | apply foo (by tactic_2) (arg_2)
        | apply foo (by tactic_3) (arg_3)
        | ...)

Now, tactic_1 and tactic_2 and so on all have some duplicated work; in particular they do a simp step at the beginning of the tactic, and this simplification is getting thrown away after each branch of the first if the branch fails. I'd like to factor this out and do the simplification one time without throwing away the results. In particular, I'd like to refactor this tactic to look like:

 `(tactic | apply foo (by
        simp; first
         | tactic_1
         | tactic_2
         | tactic_3
         | ...
      ) (arg_n))

Where the arg_n is chosen to match the tactic that was applied (e.g. tactic_1 would result in arg_1, etc). This seems to require the ability to "remember" which tactic was chosen by first. Does anybody know if this is feasible at all?

[Kyle Miller]

Can you do apply foo; simp and then write a first that operates on the two goals?

For robustness, you could use named metavariables, like

apply foo ?pf ?arg
case' pf => simp
first
  | case pf => tactic_1
    case arg => exact arg_1
  | case pf => tactic_2
    case arg => exact arg_2
  | ...

[Daniel Sainati]

hmm, this seems like it should work, but for some reason Lean doesn't like it. To be a bit more specific, my args are not always just values, in particular the original tactic often looks something like

apply foo (by tactic_1) (arg_1 _ _)

which generates two subgoals, one for each of the _s.

If I change this to be

apply foo ?pf ?arg
case' pf => simp
case pf => tactic_1
case' arg => apply arg_1 _ _

lean complains that arg_1 does not match the type of the goal

[Kyle Miller]

Two thoughts:

• Maybe you need case' arg => apply arg_1 to come before case pf => tactic_1, since the tactic might be filling in metavariables in an incompatible way
• Maybe refine arg_1 ?_ ?_ would work better, in case there are metavariables in the goal itself. The refine tactic is able to assign them, where apply avoids it.

[Kyle Miller]

It's hard to say much more without a #mwe

[Daniel Sainati]

Applying the arg case first worked! Thanks so much