tactic questions

Stream: general

[Kayla Thomas]

Is there a command to repeatedly try a set of tactics until none of them make progress or all of the goals are finished? For example, could I prove the following with a tactic after induction P that repeatedly trys each of simp and tauto?

example
  (v : variable_)
  (P : formula) :
  occurs_in v P ↔ v ∈ P.var_set :=
begin
  induction P,
  case formula.true_
  {
    refl,
  },
  case formula.pred_ : name args
  {
    refl,
  },
  case formula.eq_ : x y
  {
    unfold occurs_in,
    unfold formula.var_set,
    simp only [finset.mem_insert, finset.mem_singleton],
  },
  case formula.not_ : P P_ih
  {
    tauto,
  },
  case formula.imp_ : P Q P_ih Q_ih
  {
    unfold occurs_in,
    unfold formula.var_set,
    simp only [finset.mem_union],
    tauto,
  },
  case formula.forall_ : x P P_ih
  {
    unfold occurs_in,
    unfold formula.var_set,
    simp only [finset.mem_union, finset.mem_singleton],
    tauto,
  },
end

[Kayla Thomas]

I tried it with the any_goals tactic, but I couldn't figure how to make it try all of a set of tactics.

[Eric Wieser]

tactic#tidy does some version of this

[Kayla Thomas]

Thank you.

[Kayla Thomas]

Is there a way to dunfold all of the definitions without giving the name of each definition to unfold?

[Kayla Thomas]

Or maybe, why does the any_goals here change each case to anonymous? Is there a way to avoid that?

  induction P generalizing binders,
  any_goals { dunfold fast_admits_aux, dunfold admits_alt, },

[Kayla Thomas]

Is there a way to apply a set of tactics to each of a named list of induction cases, and that leaves the remaining cases named?

[Kayla Thomas]

That is, some way to take care of a bunch of cases that are all handled the same way, and then handle the remaining separately.

[Eric Wieser]

yes, you can use case [foo, bar] { all_goals {tac } }

[Eric Wieser]

tactic#case

[Kayla Thomas]

Nice! Thank you!