How to use `registerSimpAttr`?

Stream: lean4

[Tomas Skrivan]

Are simp sets supported and how am I supposed to use registerSimpAttr?

• It is unclear to me where am I supposed to call registerSimpAttr to properly register a simp attribute.
• Looking at Notation.lean it looks like that simp does not define simp (with simp sets)?, so simp sets are not currently supported? How difficult would it be to add the support?

My attempt, the stuff I would like to get working is commented out.

import Lean

open Lean.Meta

initialize mySimpExtension : SimpExtension  ← registerSimpAttr `mysimp "My simp set"

-- @[mysimp]
theorem expand_mul_add (x y z : Nat) : x * (y + z) = x * y + x * y := sorry

-- @[mysimp]
theorem expand_add_mul (x y z : Nat) : (x + y) * z = x * z + y * z := sorry

-- @[mysimp]
theorem lassoc_add (x y z : Nat) : x + (y + z) = x + y + z := sorry

example (x : Nat) : (x + x) * (x + x) = x * x + x * x + x * x + x * x :=
by
  simp only [expand_mul_add, expand_add_mul, lassoc_add]
  -- simp with mysimp
  done

[Arthur Paulino]

I think this is close:
First, declare this in a file:

import Lean
open Lean Meta in
initialize mySimpExtension : TagAttribute ← registerTagAttribute `mysimp "My simp set"

Then you should be able to use it in another file:

open Lean Elab.Tactic Parser.Tactic

#check simpLemma

def toSimpLemma (name : Name) : Syntax :=
  sorry

set_option hygiene false in
elab "simp " "with " tag:ident : tactic => do
  let tagName := tag.getId
  let env ← Lean.getEnv
  let simpMap := mySimpExtension.ext.getState env
  let mut decls : Array Name := #[]
  for declName in simpMap do
    decls := decls.push declName
  dbg_trace decls
  let simpLemmas : Array Syntax := #[] -- decls.map toSimpLemma
  evalTactic $ ← `(tactic|simp only [$simpLemmas,*])


@[mysimp]
theorem expand_mul_add (x y z : Nat) : x * (y + z) = x * y + x * y := sorry

@[mysimp]
theorem expand_add_mul (x y z : Nat) : (x + y) * z = x * z + y * z := sorry

@[mysimp]
theorem lassoc_add (x y z : Nat) : x + (y + z) = x + y + z := sorry

example (x : Nat) : (x + x) * (x + x) = x * x + x * x + x * x + x * x :=
by
  -- simp only [expand_mul_add, expand_add_mul, lassoc_add]
  simp with mysimp

[Arthur Paulino]

Someone else more skillful with terms of type Syntax might be able to help you with the implementation of toSimpLemma

[Arthur Paulino]

A flaw in my code: I'm not using tagName. I went straight to mySimpExtension.
Ideally mySimpExtension should be retrieved by using tagName

[Tomas Skrivan]

Cool this looks good!

First, declare this in a file:

In what file? How do I reference that file in the file where I want to use the mysimp attribute?

[Arthur Paulino]

Make a "dummy file" with that declaration alone. You can't use mySimpExtension in the same file it was registered

[Arthur Paulino]

Then make another file B with the syntax declaration and tactic implementation, which imports the previous file A. And to use your new simp, just import the file B (which will import the tag attribute transitively)

[Tomas Skrivan]

Ok, so I have to use lake to set up the project. There is no other way how to import a file, right?

[Arthur Paulino]

Not that I know of, at least

[Tomas Skrivan]

Great, so I have the attribute working!

[Arthur Paulino]

@Tomas Skrivan if you figure out how to implement toSimpLemma please let me know :eyes:

[Tomas Skrivan]

I'm looking at Lean's internals. It looks like that alternatively it would be possible to modify mkSimpContext

def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ignoreStarArg : Bool := false) : TacticM MkSimpContextResult := do
  if ctx && !stx[2].isNone then
    throwError "'simp_all' tactic does not support 'discharger' option"
  let dischargeWrapper ← mkDischargeWrapper stx[2]
  let simpOnly := !stx[3].isNone
  let simpTheorems ←
    if simpOnly then
      ({} : SimpTheorems).addConst ``eq_self
    else
      getSimpTheorems
   ...

I would modify getSimpTheorems to accept Name of the simp extension with default value simp.

def getSimpTheorems (attrName := `simp) : CoreM SimpTheorems :=
  (<- getSimpExtension attrName).getTheorems

The question is:

• How to turn Name to SimpExtension?
• How to get attrName from the syntax stx inside mkSimpContext. This probably requires modifying the syntax definition of simp in Notation.lean

[Tomas Skrivan]

I'm getting an error:

failed to synthesize instance for 'for_in%' notation
  ForIn (ReaderT Context (StateRefT' IO.RealWorld State Elab.TermElabM))
    (ScopedEnvExtension.StateStack Meta.SimpEntry Meta.SimpEntry Meta.SimpTheorems) ?m.221

on the line for declName in simpMap do

[Tomas Skrivan]

Ohh, I was using SimpExtension instead of TagAttribute. With TagAttribute it works.

[Arthur Paulino]

But then do you want to implement another tactic? I was trying to delegate the task to simp as is

[Tomas Skrivan]

Arthur Paulino said:

Tomas Skrivan if you figure out how to implement toSimpLemma please let me know :eyes:

This code reveals what needs to be created:

  let tc ← `(tactic|simp only [expand_mul_add])
  dbg_trace tc

The result is:

(Tactic.simp "simp" [] [] ["only"] ["[" [(Tactic.simpLemma [] [] `expand_mul_add._@.Main._hyg.869)] "]"] [])

[Arthur Paulino]

I think the ._@.Main._hyg.869 part can be ignored

[Arthur Paulino]

And yeah, the question is how to turn

`expand_mul_add

into

(Tactic.simpLemma [] [] `expand_mul_add)

[Mario Carneiro]

How to turn Name to SimpExtension?

This would be part of the simp with implementation: an environment extension for tracking associations of names to SimpExtensions

[Tomas Skrivan]

Arthur Paulino said:

And yeah, the question is how to turn

`expand_mul_add

into

(Tactic.simpLemma [] [] `expand_mul_add)

Maybe something like this:

mkNode `Lean.Parser.Tactic.simpLemma #[Syntax.node default nullKind #[], Syntax.node default nullKind #[], Syntax.ident SourceInfo.none default "expand_mul_add" []]

It is producing correct output on dbg_trace not sure if it is valid Syntax. I have to go now, so I can't test it.

[Mario Carneiro]

You shouldn't create a syntax to pass to simp, the point of SimpExtension is to store a compiled SimpLemmas object that can be passed directly to simp without having to break it down into lemmas again

[Tomas Skrivan]

Mario Carneiro said:

You shouldn't create a syntax to pass to simp, the point of SimpExtension is to store a compiled SimpLemmas object that can be passed directly to simp without having to break it down into lemmas again

I agree with that, but I'm just trying to finish Arthur's approach and learning about Lean in the process :)

[Arthur Paulino]

@Mario Carneiro I'm interested in knowing the proper way of doing this :eyes:

[Tomas Skrivan]

I think the correct way is to modify mkSimpContext to use the correct SimpExtension in getSimpTheorems.

This would also involve modifying the parser for simp such that it can accept the simp attribute.

[Tomas Skrivan]

Mario Carneiro said:

How to turn Name to SimpExtension?

This would be part of the simp with implementation: an environment extension for tracking associations of names to SimpExtensions

Where can I find an example of an environment extension? I have no clue how to do that.

[Arthur Paulino]

This worked:

-- file A
import Lean
open Lean Meta in
initialize mySimpExtension : SimpExtension ← registerSimpAttr `mysimp "My simp set"

import Lean
-- import file A
open Lean Elab.Tactic Parser.Tactic

def toSimpLemma (name : Name) : Syntax :=
  mkNode `Lean.Parser.Tactic.simpLemma
    #[mkNullNode, mkNullNode, mkIdent name]

elab "simp " "with " tag:ident : tactic => do
  let tagName := tag.getId
  let simpTheorems ← mySimpExtension.getTheorems
  let lemmas := simpTheorems.lemmaNames.fold
    (init := #[]) (fun acc n => acc.push (toSimpLemma n))
  evalTactic $ ← `(tactic|simp only [$lemmas.reverse,*])

@[mysimp]
theorem expand_mul_add (x y z : Nat) : x * (y + z) = x * y + x * y := sorry

@[mysimp]
theorem expand_add_mul (x y z : Nat) : (x + y) * z = x * z + y * z := sorry

@[mysimp]
theorem lassoc_add (x y z : Nat) : x + (y + z) = x + y + z := sorry

example (x : Nat) :
    (x + x) * (x + x) = x * x + x * x + x * x + x * x := by
  simp with mysimp

[Arthur Paulino]

But I still don't know how to retrieve mySimpExtension using tagName. I just hardcoded it instead

[Arthur Paulino]

So this is just as good for now:

elab "mysimp" : tactic => do
  let lemmas := (← mySimpExtension.getTheorems).lemmaNames.fold
    (init := #[]) (fun acc n => acc.push (toSimpLemma n))
  evalTactic $ ← `(tactic|simp only [$lemmas.reverse,*])

@[mysimp] theorem expand_mul_add (x y z : Nat) : x * (y + z) = x * y + x * y := sorry
@[mysimp] theorem expand_add_mul (x y z : Nat) : (x + y) * z = x * z + y * z := sorry
@[mysimp] theorem lassoc_add (x y z : Nat) : x + (y + z) = x + y + z := sorry

example (x : Nat) : (x + x) * (x + x) = x * x + x * x + x * x + x * x := by
  mysimp

[Leonardo de Moura]

Arthur Paulino said:

But I still don't know how to retrieve mySimpExtension using tagName. I just hardcoded it instead

I will add an API for this.

[Arthur Paulino]

@Leonardo de Moura My motivation was rather manual though. Mario said that this solution of building the sintax nodes for each lemma was not ideal

[Arthur Paulino]

Or do you intend to add an API for the native support of simp with <ident>?

[Leonardo de Moura]

@Arthur Paulino I didn't read the thread, but I am assuming the API is independently useful.

[Leonardo de Moura]

Arthur Paulino said:

Or do you intend to add an API for the native support of simp with <ident>?

We can add this to the core repo too, but I barely used this feature in Lean 3. If it is a popular, we can add it.

[Arthur Paulino]

I found this thread.

And this answer from Mario:

Mario Carneiro said:

Correct me if I'm wrong, but although registerSimpAttr can be used to declare simp sets, it isn't possible to use simp sets currently, because simp does not support the syntax simp [] with my_simp_set

[Mario Carneiro]

@Leonardo de Moura said:

Arthur Paulino said:

Or do you intend to add an API for the native support of simp with <ident>?

We can add this to the core repo too, but I barely used this feature in Lean 3. If it is a popular, we can add it.

It isn't very common but it is used by mathlib enough that we need it for mathport. Let me also take the opportunity to propose the alternative syntax simp [..my_simp_set] if you do implement this, I think it's a more intuitive way to write it than with since a simp set is basically a set of lemmas.

[Arthur Paulino]

Good one. Another point is that simpa has both using and with arguments. So either of those could be conflicting

[Sebastian Ullrich]

I think that could even work without the ..

[Arthur Paulino]

Although the absence of .. can add some overhead: since we can't know explicitly whether an argument is a simp set ot a simp lemma, we'd need to check everytime even though most of the times it won't be a simp set.

Regarding readability, I'd prefer the ..my_simp_set so I know before hand that my_simp_set is not a theorem (taking into consideration that the simp set name might not be so obvious)

[Mario Carneiro]

I don't think the overhead is anything to be concerned about. We already have to check the argument to see if it is a definition or a lemma; much more important is the effect on the user experience: is it important to visibly indicate that a simp set is not a lemma? Note that lemmas can sometimes act like simp sets all on their own, if they happen to be conjunctions of equalities