recursive split

Stream: general

[Patrick Massot]

Do we have a recursive split tactic? My goal looks likes a ∧ b ∧ c ∧ d and I would like to write one word and get four non-nested goals.

[Sean Leather]

There's only one “word” in refine ⟨_, _, _, _⟩. :wink:

[Patrick Massot]

Obviously, this is not exactly as readable as I hoped for, but at least this indeed does the trick.

[Sebastian Ullrich]

repeat { any_goals { split } } :)

[Sebastian Ullrich]

...which at least is a bit more general and could be extracted into a new tactic

[Jakob von Raumer]

Isn't ther also a rcases in mathlib that does this?

[Kenny Lau]

that destructs hypotheses

[Sean Leather]

repeat { any_goals { split } } :smiley:

How efficient is that? For g1 ∧ g2 ∧ g3 ∧ g4, I'm guessing that's 4 applications of any_goals, but any_goals would also test all previously split goals each time, right? I suppose it could be improved by “remembering” that split failed for a visited goal.

[Sebastian Ullrich]

How big are your conjunctions that you expect this to be a problem :frowning: ? split isn't exactly an expensive tactic.

[Patrick Massot]

I like that this version seems easy to turn into a new tactic. But, in the case I'm looking at, this creates too many goals, with stupid meta-variables

[Simon Hudon]

Do you have existential quantifications?

[Simon Hudon]

You can also use constructor_matching* _ ∧ _ to make sure it only splits conjunctions

[Patrick Massot]

Yes, hidden in subset image. After much effort, I managed to minimize to:

example (α β : Type) (f : α → β) (s : set α) (s' : set β) (x : β) :
  f '' s ⊆ s' ∧ x ∈ f '' s :=
begin
  -- refine ⟨_, _⟩,
  repeat { all_goals { split } },
end