(temporarily) modify the simp database

Stream: general

[Sorawee Porncharoenwase]

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]

[Reid Barton]

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.

[Reid Barton]

It would be easier to implement something like

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

[Reid Barton]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

ohh, in a lemma yes

[Mario Carneiro]

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

[Mario Carneiro]

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