Apply different tactics to different goals?

Stream: metaprogramming / tactics

[Richard Zhang]

Is there a tactic combinator which does the equivalent of Rocq's [> tac1 | tac2 | tac3 | ...] tactic combinator which applies the i-th tactic to the i-th focused goal? (See: https://rocq-prover.org/doc/master/refman/proof-engine/ltac.html#local-application-of-tactics)

[Aaron Liu]

IIRC it's tac <;> [tac1; tac2; tac3; ...]

[Aaron Liu]

yup just checked it's defined in batteries/tactic

[Aaron Liu]

but you need to start out with a tactic which generates the correct number of goals you want (maybe you can just use skip?)

[Aaron Liu]

of course, usually you want to collect the goals from specifically just the previous tactic in which case this is fine

[Richard Zhang]

yeah, usually this form is the more useful version (and it was indeed the version I actually needed). But just out of curiosity, I just checked and skip <;> [tac1; tac2; ...] doesn't seem to provide the right behaviour for just applying tactics to all goals in scope.

[Kim Morrison]

For human written/read code, personally I would request not using these syntaxes. Just use focusing dots and in extremity pick_goal/work_on_goal or whatever they are called now.

[Richard Zhang]

@Kim Morrison I find that syntax of this form is very useful if you want to unify two extremely-similar looking proofs with only minor differences (such as left vs. right), and in this case explicitly bulleting and duplicating code can serve to obfuscate rather than clarify.

[Kim Morrison]

Yes. I agree it can be useful. But most of the uses I encounter when fixing broken things tend to be obfuscatory, so I'm just asking that it is only used when it really really clearly improves readability. (And even then, perhaps a comment is in order...)