# Zulip Chat Archive

## Stream: general

### Topic: (temporarily) modify the simp database

#### 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]
```

#### 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.

#### 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
```

#### 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.

#### 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

#### 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

#### Reid Barton (Nov 18 2020 at 15:50):

ohh, in a lemma yes

#### 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
```

#### 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: Dec 20 2023 at 11:08 UTC