dsimp

Stream: new members

[Auguste Poiroux]

Hello!

I took a lemma in mathlib with the attribute simp and the proof rfl. I modified the proof to begin exact(rfl), end and it "broke" the proof of a following theorem which uses dsimp. I've observed this on several files.
For example in this modified file linear_pmap.lean, if you change the proof of mk_apply to rfl, the proof of mk_span_singleton_apply works again.
Why does changing the proof of mk_apply change the way dsimp works?
Why begin exact(rfl), end is not equivalent to rfl?

Thanks in advance!

[Reid Barton]

You have just described exactly how it works. Lemmas whose proofs are exactly rfl get a special "refl lemma" attribute, and dsimp will only apply such lemmas.

[Reid Barton]

dsimp only wants to apply definitional equalities, and this is how that is ensured.

[Auguste Poiroux]

Ok, thanks!

[Reid Barton]

My guess as for the reason that the check is so specific:
Lemmas are checked in parallel and a later lemma might want to use this one as a dsimp lemma.
So the test for "is this a refl lemma" needs to be something cheap that can be done in serial and not, say, running a tactic block and seeing what happens.