Partial ;

Stream: new members

[Marcus Rossel]

I have a proof that splits into two paths, which differ only in their very last statement. This last statement is a rw that needs to go in different directions, depending on the subgoal.

Is there a way to solve both subgoals using a single rw that magically knows which direction to go?
Or is there a way to apply the same sequence of tactics to two subgoals and then dive in, once they require different statements?

[Johan Commelin]

all_goals { tac1, tac2 } is probably what you want

[Johan Commelin]

Another option is to see if you can postpone the split to a later point in your proof

[Marcus Rossel]

@Johan Commelin all_goals worked like a charm. Thanks :)

[Mario Carneiro]

you can also use id after ; to avoid trying to close the goal as { tacs } would do. That is, split; id { tac1, tac2 }; [rw th1, rw th2] will first split, then apply tac1 then tac2 on each goal, and then apply rw th1 to the first goal and rw th2 on the second

[Mario Carneiro]

this differs slightly from all_goals because that applies to all goals while tac; id { tacs } applies tacs only to the goals produced by tac

[Eric Wieser]

tac; all_goals {tacs} would work too, but is misleading, right?

[Mario Carneiro]

There are actually lots of things that can be used instead of id; I used to use try a lot for this

[Mario Carneiro]

I like id because it is explicitly intended to do nothing other than negate the , done behavior that { tacs } has

[Eric Wieser]

Is that literally just docs#id, or is it some docs#tactic.interactive.id?

[Mario Carneiro]

It's the latter

[Mario Carneiro]

It's really just a carrier for the itactic parser aka tac_name { ... }

[Mario Carneiro]

as you can see from the source it is really the identity function

[Mario Carneiro]

but it has to be in the tactic.interactive namespace to cooperate with other interactive tactics