use a tactic only if it is in environment

Stream: general

[Jason Rute]

This is probably asking too much, but I want to check if this is possible. Is it possible (in a tactic monad) to automatically check if a tactic like norm_num is in the environment, and if so use it, otherwise don't. My idea is a tactic which applies certain other tactics, but only if they are already imported. In most compiled programming languages this would be a silly request (and in python everything is possible if you are willing to live with crazy hacks). However, in Lean it might be doable since I can already inspect the environment for declarations.

[Scott Morrison]

Yes, certainly. I don't think there's an example currently in mathlib. I'll try to dig one up, or hopefully one of the tactic programming experts can tell you.

[Scott Morrison]

Maybe just resolve_name?

[Scott Morrison]

You can get what you want from a slight tweak to name_to_tactic in tactics/core.lean.

[Scott Morrison]

Something like:

[Scott Morrison]

meta def run_tactic (n : name) : tactic unit :=
do d ← get_decl n,
   e ← mk_const n,
   let t := d.type,
   if (t =ₐ `(tactic unit)) then
     (eval_expr (tactic unit) e) >>= (λ t, t)
   else fail

[Scott Morrison]

That isn't ideal, as you won't be able to distinguish easily between the tactic not being in the environment, and the tactic failing.

[Scott Morrison]

But that should be easy to fix.

[Jason Rute]

Thanks so much!

[Keeley Hoek]

But to be clear, it's not hard to distinguish that either:

-- Returns whether the tactic was found.
-- Fails only if the tactic fails, or a declaration with the
-- given name exists but it is not a tactic program.
meta def run_tactic_if_present (n : name) : tactic bool :=
do d ← get_decl n,
   e ← mk_const n,
   let t := d.type,
   if (t =ₐ `(tactic unit)) then do {
     tac ← some <$> eval_expr (tactic unit) e <|> pure none,
     match tac with -- or use `option.mmap` if you want to import it
     | some tac := tac >> return true
     | none := return false
     end
   }
   else failed