custom simp-sets

Stream: new members

[Eric Rodriguez]

Is there any docs about how to make custom simp-sets? If not, I'll trade an explanation for writing them up :b

[Johan Commelin]

Here's an example: https://github.com/leanprover-community/mathlib/blob/master/src/algebra/group_with_zero/basic.lean#L43

[Bryan Gin-ge Chen]

There is some partial documentation at command#mk_simp_attribute.

[Bryan Gin-ge Chen]

It'd be good to add at least a mention of this command to the simp tutorial page: https://leanprover-community.github.io/extras/simp.html

[Eric Rodriguez]

brill, thanks guys - will get something written up soon!

[Eric Rodriguez]

whilst I'm at it, does anyone know what simp {contextual := tt} does? it seems to add more simp lemmas in some way, but I'm not sure how

[Eric Rodriguez]

may as well document that too as it pops up on mathlib from time to time

[Eric Rodriguez]

also, can I have branch perms for leanprover-community.github.io?

[Bryan Gin-ge Chen]

You can just make an ordinary PR to that repo.

[Bryan Gin-ge Chen]

(from a fork on GitHub)

[Eric Rodriguez]

oh dope, that's easier

[Bryan Gin-ge Chen]

Regarding an explanation of simp options, maybe @Mario Carneiro can be persuaded to help out (as he volunteered to a while ago... :wink: ).

[Eric Rodriguez]

PR done!

[Mario Carneiro]

simp {contextual := tt} will, when rewriting in a forall or lambda, add the variables in the binder to the simp set. So for example x = 0 -> x + x = 0 will be simplified to x = 0 -> 0 + 0 = 0 (and eventually proved) even though x = 0 was not passed as a simp lemma