closing rfl

Stream: mathlib4

[Yury G. Kudryashov]

I see some PRs replacing rfls with extra rws/simp_rws. Do we have a style guide about this?

[Antoine Chambert-Loir]

Sometimes, I finish by simp because I guess that will work, without noticing rfl would.

[Yury G. Kudryashov]

I was talking about intentional replacement of ; rfl with extra rws.

[Antoine Chambert-Loir]

Is it possible to compare the compilation time: could one imagine that simp would conclude faster than the mere rfl.

[Yury G. Kudryashov]

If we want to do this, then we should add it to the style guide.

[Kyle Miller]

Can you point out examples of what you're talking about?

[Yury G. Kudryashov]

#10007

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathlib4/pull/10007/files#diff-1e9794c797a2e3fc46aa3c494bc7eb59061c316445f214b757820b3bc34e3b84

[Kyle Miller]

I'd guess that these are avoiding some defeq abuses, but it'd be good to ask @Ruben Van de Velde what's being tidied.

[Ruben Van de Velde]

Yeah, these all count as defeq abuse in my opinion

[Eric Wieser]

Removing trailing rfls is a nice way of confirming that we're not missing API lemmas

[Antoine Chambert-Loir]

Oh! Do you believe that rfl-lemmas should exist to do the rewriting we need to?

[Ruben Van de Velde]

Yeah (and they generally do)

[Yury G. Kudryashov]

Ruben Van de Velde said:

Yeah, these all count as defeq abuse in my opinion

Can you elaborate? Does any non-reducible rfl count as defeq abuse or not?

[Kyle Miller]

We don't have any codified rules for this, but this is roughly how I've thought about it:

1. If defeq needs to unfold a non-reducible definition, and this happens inside the API boundary for the mathematical theory, then it is OK. This usually necessary to set up the API.
2. If defeq needs to unfold a non-reducible definition, and the documentation clearly says that what this definition unfolds to is part of the API for the mathematical theory, then it is OK. This happens sometimes, for example with Function.Injective and many other predicates, or Nat.succ n =?= n + 1, though these aren't necessarily documented yet. Here is an example of an API defeq in a docstring.

A problem though is that there's often not a really a clear API boundary for theories.

[Matthew Ballard]

I think some clear guidelines would be helpful and Kyle’s suggestions are a good start.