Zulip Chat Archive

Stream: Is there code for X?

Topic: work_on_goals


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 17 2020 at 21:51):

work_on_goal is that one

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 17 2020 at 22:01):

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

view this post on Zulip 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