## Stream: lean4

### Topic: simp databases

Is there a way to annotate definitions with some variant of @[simp] so that when I do, say simp [$some_db] (or whatever) they get unfolded, but when I just do simp they do not? Relatedly, is there a variant of simp that unfolds all definitions, or unfolds all definitions except those given in a blacklist? #### Yury G. Kudryashov (Mar 16 2021 at 22:28): In Lean 3 the answer is "yes", there is simp with attr_name. Not sure about Lean 4. #### Leonardo de Moura (Mar 16 2021 at 23:34): We have scoped simp lemmas in Lean 4. constant f : Nat → Nat constant g : Nat → Nat namespace Foo @[scoped simp] axiom ax1 (x : Nat) : f (g x) = x @[scoped simp] axiom ax2 (x : Nat) : g (g x) = g x end Foo theorem ex1 : f (g (g (g x))) = x := by simp -- does not use ax1 and ax2 theorem ex2 : f (g (g (g x))) = x := open Foo in simp /- open Foo for this tactic only -/ /- open Foo for the following theorem only -/ open Foo in theorem ex3 : f (g (g (g x))) = x := by simp  #### Leonardo de Moura (Mar 16 2021 at 23:37): Is there a way to annotate definitions with some variant of @[simp] so that when I do, say simp [$some_db] (or whatever) they get unfolded, but when I just do simp they do not?

The SimpLemmas datastructure has a set of functions to be unfolded. We were planning to allow users to tag regular definitions with [simp] (and variants [scoped simp] and [local simp]) to indicate they want them to be unfolded.

#### Leonardo de Moura (Mar 16 2021 at 23:39):

Relatedly, is there a variant of simp that unfolds all definitions, or unfolds all definitions except those given in a blacklist?

We were not planning to support this variant. Do you have compelling examples where it is a must-have?

#### Jason Gross (Mar 17 2021 at 17:58):

scoped simp sounds great!

#### Jason Gross (Mar 17 2021 at 17:59):

Relatedly, is there a variant of simp that unfolds all definitions, or unfolds all definitions except those given in a blacklist?

We were not planning to support this variant. Do you have compelling examples where it is a must-have?

I think it is useful sometimes when doing quick-and-dirty debugging of goals, but I can be more systematic about things.

#### Jason Gross (Mar 17 2021 at 18:00):

How do I put the scoped simp unfolding in a different namespace than the definition? For example:

def MyNat := Nat
namespace Foo
@[scoped simp] MyNat
end Foo


or something?

#### Sebastian Ullrich (Mar 17 2021 at 18:07):

attribute [scoped simp] MyNat should work, I hope. Except that [simp] currently only works on Props in general.

#### Mario Carneiro (Mar 17 2021 at 18:18):

In lean 3 [simp] on a def will instead add [simp] to the def's equation lemmas

#### Mario Carneiro (Mar 17 2021 at 18:18):

but I guess we don't have equation lemmas ATM

#### Sebastian Ullrich (Mar 17 2021 at 18:18):

We should do that eventually, yes :)

#### Sebastian Ullrich (Mar 17 2021 at 18:24):

Mario Carneiro said:

but I guess we don't have equation lemmas ATM

We don't, but simp only needs the "smart unfolding" info that is already there

Last updated: May 18 2021 at 23:14 UTC