Tactic combinator to affect all goals except first

Stream: new members

[Lorenz Leutgeb]

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]

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

[Kyle Miller]

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?)

[Lorenz Leutgeb]

I think so, yes.

[Kyle Miller]

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]

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

[Lorenz Leutgeb]

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

[Kyle Miller]

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]

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

[Lorenz Leutgeb]

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]

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]

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]

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

[Kyle Miller]

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]

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]

(@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]

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]

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

[Mario Carneiro]

I was thinking of t1; rest => t2

[Mario Carneiro]

or case -foo => t2

[Mario Carneiro]

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