## Stream: Is there code for X?

### Topic: work_on_goals

#### Eric Wieser (Dec 17 2020 at 21:50):

Is there a way to run a tactic against multiple specific goals? To elaborate:

example (α β : Type*) (i j : α ⊕ β) : true :=
begin
cases hi : i; cases hj : j,
rotate,
-- first case: one inr and one inl
-- second case: both inr or both inl
end


I'd like to split the goals into two pairs, as within a pair the approach to solving is almost identical.

#### Adam Topaz (Dec 17 2020 at 21:51):

The two tactics I know of are all_goals and any_goals. There is also one which I can't remember to focus on a specific goal

#### Eric Wieser (Dec 17 2020 at 21:51):

work_on_goal is that one

#### Eric Wieser (Dec 17 2020 at 21:52):

Currently my workaround is to use by_cases h : (∃ il, sum.inl il = i) ↔ (∃ jl, sum.inl jl = j) to generate the split, and then a bunch of messy applications of iff_iff_and_or_not_and_not and not_exists to split up h - but this seems silly given I can directly case-match.

#### Adam Topaz (Dec 17 2020 at 21:57):

My thinking is something like this:

example (P : Prop) (α β : Type*) (i j : α ⊕ β) (h1 : α → P) (h2 : β → P) : P :=
begin
cases hi : i; cases hj : j,
any_goals { apply h1, assumption },
any_goals { apply h2, assumption },
end


#### Eric Wieser (Dec 17 2020 at 22:01):

any_goals feels a bit sloppy if I know exactly which two are going to work

#### Eric Wieser (Dec 17 2020 at 22:15):

This naive attempt doesn't work and I don't know why: seems to work:

namespace tactic
namespace interactive

open lean
open lean.parser
open interactive interactive.types expr

#check conv.interactive.for
#check list.enum

meta def work_on_goals : parse (list_of small_nat) → itactic → tactic unit
| ns t := do
goals ← get_goals,
let ⟨current_goals, later_goals⟩ := goals.enum.partition (λ g, prod.fst g ∈ ns),
let current_goals' := current_goals.map prod.snd,
let later_goals' := later_goals.map prod.snd,
trace current_goals',
trace later_goals',
set_goals current_goals',
t,
new_goals ← get_goals,
set_goals (new_goals ++ later_goals')

end interactive
end tactic


Last updated: May 16 2021 at 05:21 UTC