Zulip Chat Archive

Stream: general

Topic: use a tactic only if it is in environment


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

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

view this post on Zulip Scott Morrison (May 28 2020 at 14:01):

Maybe just resolve_name?

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

view this post on Zulip Scott Morrison (May 28 2020 at 14:03):

Something like:

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

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

view this post on Zulip Scott Morrison (May 28 2020 at 14:05):

But that should be easy to fix.

view this post on Zulip Jason Rute (May 28 2020 at 23:56):

Thanks so much!

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