Zulip Chat Archive

Stream: new members

Topic: Partial ;


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 03 2021 at 10:34):

all_goals { tac1, tac2 } is probably what you want

view this post on Zulip 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

view this post on Zulip Marcus Rossel (Mar 03 2021 at 10:35):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 03 2021 at 10:45):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 03 2021 at 11:40):

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

view this post on Zulip Mario Carneiro (Mar 03 2021 at 11:43):

It's the latter

view this post on Zulip Mario Carneiro (Mar 03 2021 at 11:44):

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

view this post on Zulip Mario Carneiro (Mar 03 2021 at 11:44):

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

view this post on Zulip 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: May 13 2021 at 20:13 UTC