## Stream: new members

### Topic: Partial ;

#### Marcus Rossel (Mar 03 2021 at 10:33):

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 (Mar 03 2021 at 10:34):

all_goals { tac1, tac2 } is probably what you want

#### Johan Commelin (Mar 03 2021 at 10:34):

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

#### Marcus Rossel (Mar 03 2021 at 10:35):

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

#### Mario Carneiro (Mar 03 2021 at 10:40):

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 (Mar 03 2021 at 10:42):

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 (Mar 03 2021 at 10:45):

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

#### Mario Carneiro (Mar 03 2021 at 11:34):

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

#### Mario Carneiro (Mar 03 2021 at 11:34):

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

#### Eric Wieser (Mar 03 2021 at 11:40):

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

It's the latter

#### Mario Carneiro (Mar 03 2021 at 11:44):

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

#### Mario Carneiro (Mar 03 2021 at 11:44):

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

#### Mario Carneiro (Mar 03 2021 at 11:45):

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

Last updated: Dec 20 2023 at 11:08 UTC