tactics

Stream: general

[Sebastien Gouezel]

I am struggling to write a super-basic tactic (see #1792). Given a string e of the form "simp [-one_div_eq_inv, hx, hy] with field_simps", say, is there a command to convert it to something one can execute? (I tried [``e] and variations of this, to no avail).

It may well be an instance of an XY problem, so here is a little bit more context: I want field_simp [hx] to call simp [-one_eq_div_inv, hx] with field_simps (and I don't want to fiddle with simpparsing options are there are just too many of them). My current attempt looks like

namespace tactic

meta def field_simp (hs : list pexpr) : tactic unit :=
let e := "simp [-one_div_eq_inv, " ++ list.to_string_aux tt hs ++ "] with field_simps" in
trace e; skip

namespace interactive
open interactive interactive.types expr

meta def field_simp (hs : parse pexpr_list_or_texpr) : tactic unit :=
tactic.field_simp hs
end interactive
end tactic

[Gabriel Ebner]

(deleted)

[Gabriel Ebner]

I don't think there's any way to parse a string into an expression inside a tactic. I think you should just call tactic.interactive.simp directly (it's just a regular function after all).

[Rob Lewis]

@Sebastien Gouezel I was hoping to find time to try the field_simp tactic today -- it should only take a few lines of code. Not 100% sure I'll have a chance, but if not, I can do it tomorrow. As Gabriel says, the easiest way to do it is just to put together the right information to give to tactic.interactive.simp, or maybe using the definition of tactic.interactive.simp with very minor changes.

[Rob Lewis]

Okay, here's a sketch of how it would look:

import tactic.core
open tactic tactic.interactive

mk_simp_attribute newattr none
setup_tactic_parser

@[newattr] lemma k (x : ℤ) : x + x = 0 := sorry
@[simp, priority 20000] lemma badsimp (x : ℤ) : x + x = x := sorry

meta def tactic.interactive.simp_with (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
              (locat : parse location) (cfg : simp_config_ext := {}) : tactic unit :=
let attr_names := `newattr :: attr_names,
    hs := simp_arg_type.except `badsimp :: hs in
propagate_tags (simp_core cfg.to_simp_config cfg.discharger ff hs attr_names locat)

-- fail
example (x : ℤ) : x + x = 0 :=
begin simp with newattr,  end

-- work
example (x : ℤ) : x + x = 0 :=
begin simp [-badsimp] with newattr,  end

example (x : ℤ) : x + x = 0 :=
begin simp_with end

[Rob Lewis]

I removed the option to write simp_with only [...] because I'm not sure how simp only [-badsimp] behaves. It's probably fine and you could add it back.

[Sebastien Gouezel]

Thanks!