## Stream: new members

### Topic: Tactic combinator to affect all goals except first

#### Lorenz Leutgeb (Dec 19 2023 at 17:34):

Say I have one goal. After t1 there are now many goals. I think that t2 should be able to solve all goals except the first. In these scenarios I often do t1 <;> try t2. Even though I think that t2should be able to deal with all goals except the first, it might not. Since I use try, the tactic won't fail. I am looking for a cleaner way to compose tactics (including failure if not all but the first goal could be solved) but couldn't find any. Is there one? Thanks!

#### Eric Rodriguez (Dec 19 2023 at 17:37):

I think this would be really nice, I'm not aware of such a combinator existing

#### Kyle Miller (Dec 19 2023 at 17:41):

Just to nail down the specification, are you saying you want some combinator that runs a tactic on all the "side goals" produced by the first tactic? (And which will fail if the tactic fails on any of the side goals?)

I think so, yes.

#### Kyle Miller (Dec 19 2023 at 17:43):

It seems like there ought to be a dual to focus, where it focuses on all goals but the first. Let's call it defocus. Then you could write

t1
defocus all_goals t2


#### Kyle Miller (Dec 19 2023 at 17:44):

That's assuming you're starting with just one goal.

#### Lorenz Leutgeb (Dec 19 2023 at 17:44):

Yes, I found out about focus and had a similar idea. But that turned out to be a dead end.

#### Kyle Miller (Dec 19 2023 at 17:44):

A missing combinator is a version of <;> that makes it so that the goal state is all the goals produced by the first tactic, rather than running the second tactic on each goal.

#### Kyle Miller (Dec 19 2023 at 17:45):

Which part is the dead end? That it's missing, or that there's a reason it can't be implemented?

#### Lorenz Leutgeb (Dec 19 2023 at 17:46):

Ideally, I'd also hope the syntax to be shorter. I'm thinking of <1> or something similar. For the "version of <;>" that you are describing.

#### Lorenz Leutgeb (Dec 19 2023 at 17:46):

Kyle Miller said:

Which part is the dead end? That it's missing, or that there's a reason it can't be implemented?

That it's missing. I would be very surprised if it couldn't be implemented.

#### Kyle Miller (Dec 19 2023 at 17:49):

I wonder what a good syntax would be for "run this on all but the first." The strongest I've come up with so far is <-;>, where the - is supposed to hint that it's without one of the goals. I think the ; hints that it's like <;>.

#### Lorenz Leutgeb (Dec 19 2023 at 17:51):

Yeah, I do see the argument for keeping ; around. But we're bikeshedding :)

#### Kyle Miller (Dec 19 2023 at 17:51):

The only real question here is what color should the bike shed be, and we're stuck with its color once it's chosen.

#### Lorenz Leutgeb (Dec 19 2023 at 17:53):

Well, if that tactic combinator gets released as part of Lean/mathlib, then we'd be stuck. But I'd also be happy to just copy someone else's implementation into my project and enjoy that while someone else does the bikeshedding :)

#### Kyle Miller (Dec 19 2023 at 17:54):

(@Mario Carneiro Would this t1 <-;> t2 combinator (specific notation pending) be crazy to add to std? I know I've written things like apply foo <;> try assumption when apply foo <-;> assumption would be more accurate. The assumption is that tactics tend to put side goals after the "main" goal, so the purpose of this combinator is to run the tactic on all generated goals but the first.)

#### Kyle Miller (Dec 19 2023 at 17:55):

It might be nice if this were part of some set of more composable combinators. My reservation is that this one seems like it is too specific, but on the other hand if the combinators are too expressive it could get difficult to follow proofs that use them.

#### Eric Wieser (Dec 19 2023 at 18:29):

t1 <;> (?_ :: t2) maybe, to match t1 <;> [?_, t2, t2, t2]?

#### Mario Carneiro (Dec 19 2023 at 19:38):

I was thinking of t1; rest => t2

#### Mario Carneiro (Dec 19 2023 at 19:38):

or case -foo => t2

#### Mario Carneiro (Dec 19 2023 at 19:39):

because I think you sometimes also want to exclude a non-first goal, e.g. in an induction where almost all the cases are trivial

Last updated: Dec 20 2023 at 11:08 UTC