Custom unfold

Stream: general

[Alfredo Moreira-Rosa]

Hello,

for my library on dimensional analysis and units, i have used @[simp] to allow to unfold derived definitions for simp, like this :

@[simp] def inch := defineDerivedUnit "in" meter (Conversion.scale (254/10000) (by simp))
@[simp] def foot := defineDerivedUnit "ft" inch (Conversion.scale (12) (by simp))
@[simp] def yard := defineDerivedUnit "yd" foot (Conversion.scale (3) (by simp))
@[simp] def mile := defineDerivedUnit "mi" yard (Conversion.scale (1760) (by simp))

And i use it to unfold the definition, so that simp will unfold the derived units into their base units recusively automatically to be able to have a simple tactic that simplify the units and apply module tactic in the end.
like this :

macro "auto_dim" : tactic =>
  `(tactic|
    (first | rfl
           | try simp [𝒟,HasDimension.dimension, instHMul, instHDiv, instHPow,
                      HasEquiv.Equiv,Unit.instSetoidUnit]
             try module
    ))

Is there a way to evoid using @[simp] or have a custom @[simp-derived] so that i can run simp with only the definitions marked with it ?

[Kyle Miller]

Take a look at custom simp sets

All you have to do is write something like this in one module

initialize mySimpSetExt : SimpExtension ←
  registerSimpAttr `my_simp_set
    "lemmas for my application"

and then in another module start using @[my_simp_set] and simp [my_simp_set]. It has to be imported, it can't be done in the same module.

[Alfredo Moreira-Rosa]

Thank you very much, exactly what i need!