refl

Stream: general

[Andrew Ashworth]

why does lean automatically tag certain theorems with @[_refl_lemma]?

[Simon Hudon]

I want to know too!

[Mario Carneiro]

That attribute means that it's a refl lemma (it was proven by rfl), and it is basically "@[simp] for dsimp"

[Andrew Ashworth]

someday i'd like to write a boilerplate macro that goes into definitions and creates lemmas for each branch

[Andrew Ashworth]

although even better is if we could suggest names while constructing a def using the equation compiler

[Simon Hudon]

That attribute means that it's a refl lemma (it was proven by rfl), and it is basically "@[simp] for dsimp"

Is this necessary because definitional equality is not transitive?

[Mario Carneiro]

No, it's just a way to guide the operation of dsimp. There are loads of things that are defeq, so how should it know you want a + succ b to "unfold" to succ (a + b) and not something else? Equation lemmas are used for this purpose, and the ones that are known to be definitional are legal for use by dsimp

[Simon Hudon]

Does dsimp use anything else?

[Mario Carneiro]

It uses the bracket list of course, but most of its stuff comes from equation lemmas

[Mario Carneiro]

someday i'd like to write a boilerplate macro that goes into definitions and creates lemmas for each branch

def does this currently...