## Stream: general

### Topic: use a tactic only if it is in environment

#### Jason Rute (May 28 2020 at 13:36):

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 (May 28 2020 at 14:00):

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 (May 28 2020 at 14:01):

Maybe just resolve_name?

#### Scott Morrison (May 28 2020 at 14:03):

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

Something like:

#### Scott Morrison (May 28 2020 at 14:05):

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 (May 28 2020 at 14:05):

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 (May 28 2020 at 14:05):

But that should be easy to fix.

Thanks so much!

#### Keeley Hoek (May 29 2020 at 04:01):

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


Last updated: May 12 2021 at 23:13 UTC