simp databases

Stream: lean4

[Jason Gross]

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]

In Lean 3 the answer is "yes", there is simp with attr_name. Not sure about Lean 4.

[Leonardo de Moura]

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]

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]

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]

scoped simp sounds great!

[Jason Gross]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

but I guess we don't have equation lemmas ATM

[Sebastian Ullrich]

We should do that eventually, yes :)

[Sebastian Ullrich]

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