Creating rw/simp sets "on the fly"

Stream: Is there code for X?

[Miguel Marco]

In certain contexts, it may be useful to simplify/rewrite using a specific set of rules. Is there a way to define such a set "on the fly"?

Something like

def my_rule_set : RuleSet := [mul_add, mul_sub, mul_neg]


example (a b c :  Nat) : a * (b + c - a) = 0 := by
  simp only  [my_rule_set]

[Aaron Liu]

I don't see how this is "on the fly"

[Miguel Marco]

I mean you can do it in your own file, without having to go through the code of each lemma you want to use to mark them.

[Aaron Liu]

oh is that how it usually works (I don't really make simp sets myself so I wouldn't know)

[Miguel Marco]

I think so. Am I wrong?

[Aaron Liu]

what's the syntax to declare a simp set?

[Aaron Liu]

found it

[Kenny Lau]

@Miguel Marco What about this?

import Mathlib

local macro "my_rule_set" : tactic => `(tactic|
  repeat first | rw [mul_add] | rw [mul_sub] | rw [mul_neg])

example (a b c : Int) : a * (b + c - a) = 0 := by
  my_rule_set

(I changed Nat to Int because mul_sub doesn't apply for Nat)

[Aaron Liu]

rw isnt the same as simp

[Miguel Marco]

So, that is defining a new tactic, rather than a simpset, right?

[Aaron Liu]

this should definitely be possible to declare a simp extension with all its theorems at the declaring site

[Kenny Lau]

Miguel Marco said:

So, that is defining a new tactic, rather than a simpset, right?

yes

[Kenny Lau]

this happens in mathlib all the time

[Aaron Liu]

I think the simplest to do it (if you know metaprogramming) would be

• obtain a simp extension with docs#Lean.Meta.mkSimpExt (unfortunately this starts you out with an empty extension)
• add all the theorems with docs#Lean.Meta.addSimpTheorem
• register it to the simp extension map by using docs#ST.Ref.modify to docs#Std.HashMap.insert it into docs#Lean.Meta.simpExtensionMapRef

[Robin Arnez]

Well, the usual thing is

/-- My attribute doc-string -/
initialize mySimpExtension : SimpExtension ← registerSimpAttr `special_simps "Special simps"

and then use @[special_simps] or attribute [special_simps] thm1 thm2 thm3 for tagging theorems and finally use simp only [special_simps] (note that you can't use the attribute in the file with the initialize directly though but only in a file that imports it)

[Kenny Lau]

Robin Arnez said:

note that you can't use the attribute in the file with the initialize directly

yeah, I find this a very annoying "feature"

[Kenny Lau]

can I declare inside a file that I want Lean to treat the code afterwards as part of a new file?

[Kim Morrison]

No.

[Kevin Buzzard]

This is of course an unsurprising answer! But it is on the face of it a bit weird that you can't use the attributes in the file where you define them.