mkSimpAttr

Stream: lean4

[Simon Hudon]

In Lean 3, we have a meta function to create a customized simp attribute. Does that exist in Lean 4 already?

[Gabriel Ebner]

registerSimpAttr

[Simon Hudon]

Thanks!

[Simon Hudon]

Follow-up: I noticed something called preprocess and postprocess with simp. Does that mean that we can create our own pre / postprocessing functions, a bit like reassoc in mathlib / category theory?

[Gabriel Ebner]

rg -i postprocess src doesn't return anything, can you be more specific?

[Gabriel Ebner]

Big-picture wise nothing has changed. We still don't have simpprocs.

[Gabriel Ebner]

You can still write your own simplifiers, with blackjack and simpprocs.

[Simon Hudon]

What are blackjack and simpprocs?

[Gabriel Ebner]

Blackjack is a form of gambling. Simpprocs are a feature in the Isabelle simplifier, which allows you to register -- in the same way as simp lemmas -- functions that are executed during simplification.

[Gabriel Ebner]

The combination just means "with whatever features you want".

[Patrick Massot]

Standard link: https://github.com/leanprover/lean/wiki/Simplifier-Features

[Johan Commelin]

Standard link: https://en.wikipedia.org/wiki/Blackjack

[Simon Hudon]

Specifically, what I was referring to are ↑ ↓ in the syntax of simp attributes

[Gabriel Ebner]

Ah those. To be honest, today is the first time I've seen them. They allow you to specify if a simp lemma is applied before recursing into the arguments, or afterwards. (Default is post, for pre-lemmas you need to be super super careful not to run into confluence issues.) The pre/post-flag can't be used for anything like reassoc.

[Simon Hudon]

:+1:

[Simon Hudon]

I'm thinking about how reassoc could be redesigned so that we don't have to mark lemmas as reassoc. What I'm thinking of is that I'd create an additional simp attribute to use with a customized simp tactic. In that cache, I'd put all the simp lemmas but also their reassoc version as well. The reassoc versions would be created when the cache is updated and for the lemmas that you list as arguments to simp. Does that seem like a reasonable design to you?

[Gabriel Ebner]

I don't think a custom simp tactic is a good idea. The whole point of reassoc is to automate writing simp lemmas for the default simp tactic, not to add yet another tactic.

[Gabriel Ebner]

BTW, if you add @[simp] to a lemma like foo : a ↔ b, then Lean 4 will declare a helper lemma foo_aux : a = b and add that to the simp extension instead. So I think it's perfectly fine to have reassoc add helper lemmas as well.

[Simon Hudon]

The idea is that reassoc is not the only feature that needs to create buddy lemmas. In mathlib, there's also higher_order which creates point-free formulations which are very useful when working with Functor, Foldable and Traversable. I'd like to be able to declare once that reassoc lemmas are useful, point-free lemmas are useful and so on if necessary rather than going around tagging every possible lemma with both attributes. I think with a custom version of simp, you can create a scoped macro and have the same syntax as simp (down to the name) and the whole device can be made invisible

[Simon Hudon]

Gabriel Ebner said:

BTW, if you add @[simp] to a lemma like foo : a ↔ b, then Lean 4 will declare a helper lemma foo_aux : a = b and add that to the simp extension instead. So I think it's perfectly fine to have reassoc add helper lemmas as well.

Do you think the same machinery could be highjacked to create our own companion lemmas?