work_on_goals

Stream: Is there code for X?

[Eric Wieser]

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]

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]

work_on_goal is that one

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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