Zulip Chat Archive

Stream: general

Topic: (temporarily) modify the simp database


view this post on Zulip Sorawee Porncharoenwase (Nov 18 2020 at 14:41):

Is it possible to temporarily modify the simp database?

For example:

lemma my_lemma ...
begin
  #modifies_temp_simp [+foo, +bar, -baz]
  ...
  simp,
  ...
  simp,
end

In the above proof, both simp would be equivalent to simp [foo, bar, -baz]. Outside of my-lemma, however, simp reverts back to its default behavior.

I can even imagine a fancier version where it is scoped, so:

lemma my_lemma ...
begin
  #modifies_scoped_simp [-baz]
  cases n,
  case zero {
    #modifies_scoped_simp [+foo]
    ...
    simp,
  },
  case succ {
    #modifies_scoped_simp [+bar]
    ...
    simp,
  }
end

would have simp acts like simp [+foo, -baz] in the zero case, and simp [+bar, -baz] in the succ case.

If the scoped version / temporary version is not possible, even the permanent one could still do the job. It's just slightly more annoying to work with.

#modifies_permanent_simp [+foo, +bar, -baz]

lemma my_lemma ...
begin
  ...
  simp,
  ...
  simp,
end

#modifies_permanent_simp [-foo, -bar, +baz]

view this post on Zulip Reid Barton (Nov 18 2020 at 14:50):

The last one is possible using local attribute inside a section. The first two are probably also possible in principle but it might be tricky to ensure that the attribute changes don't leak out of the lemma.

view this post on Zulip Reid Barton (Nov 18 2020 at 14:51):

It would be easier to implement something like

lemma my_lemma ...
begin
  with_temp_simp [+foo, +bar, -baz] {
    ...
    simp,
    ...
    simp }
end

view this post on Zulip Reid Barton (Nov 18 2020 at 14:54):

There's a (noninteractive) tactic docs#tactic.with_local_reducibility which does something like this but for irreducibility, which I guess is not really an attribute but is modified as though it were one.

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:42):

I think you can just make attribute changes from the lemma, because lean rolls back everything in the environment after a lemma

view this post on Zulip Mario Carneiro (Nov 18 2020 at 15:42):

this also makes me want a let_tac command for defining a temporary tactic in a proof

view this post on Zulip Reid Barton (Nov 18 2020 at 15:50):

ohh, in a lemma yes

view this post on Zulip Mario Carneiro (Nov 18 2020 at 16:00):

dang:

import tactic

namespace tactic
namespace interactive
setup_tactic_parser
meta def let_tac (f : parse (ident? <* tk ":="))
  (tac : parse (reflected_value.expr <$> parser.itactic_reflected)) :=
let name := `tactic.interactive ++ (f.get_or_else `tac) in
add_decl (declaration.defn name [] `(tactic unit) tac (reducibility_hints.regular 1 tt) ff)

meta def run_tac (f : parse ident?) :=
let name := `tactic.interactive ++ (f.get_or_else `tac) in
eval_expr (tactic unit) (expr.const name [])

end interactive
end tactic

example (x y z : ) : (x + y) + z = y + z + x  (x + y) + z = y + z + x :=
begin
  let_tac foo := {simp [add_comm, add_left_comm, add_assoc]},
  split,
  -- foo -- does not exist at parse time :(
  run_tac foo -- VM does not have code :(
end

view this post on Zulip Mario Carneiro (Nov 18 2020 at 16:05):

import tactic

namespace tactic
namespace interactive
setup_tactic_parser
meta def let_tac (f : parse (ident? <* tk ":="))
  (tac : parse (reflected_value.expr <$> parser.itactic_reflected)) :=
let name := `tactic.interactive ++ (f.get_or_else `tac) in
add_decl (declaration.defn name [] `(tactic unit) tac (reducibility_hints.regular 1 tt) ff)

meta def run_tac (f : parse ident?) :=
do env  get_env,
  let name := `tactic.interactive ++ (f.get_or_else `tac),
  val  declaration.value <$> env.get name,
  eval_expr (tactic unit) val >>= id

end interactive
end tactic

example (x y z : ) : (x + y) + z = y + z + x  (x + y) + z = y + z + x :=
begin
  let_tac foo := {simp [add_comm, add_left_comm, add_assoc]},
  split,
  run_tac foo, -- :)
  run_tac foo,
end

Last updated: May 12 2021 at 22:15 UTC