Test for `dsimp` vs `simp` with simp lint?

Stream: mathlib4

[Arien Malec]

In mathlib4#1517 encode_ofEquiv I have a simp can prove this lint -- @Johan Commelin asked if dsimp can prove it (and if not we want to mark a nolint).

Is the discriminating test whether by dsimp closes the original proof?

[Johan Commelin]

yes, If and only if the original proof is rfl

[Johan Commelin]

Otherwise the test is whether by simp closes the proof

[Arien Malec]

So decision tree is: If proof is rfl and we have a simp can prove lint, if by dsimp closes the goal, we remove the simp attribute; if not, we keep, mark nolint, and put a porting annotation. I'll update the porting wiki.

[Johan Commelin]

In all cases, leave a Porting note

[Johan Commelin]

The reasoning behind these tests is that dsimp only uses simp-lemmas that were proven by rfl.

[Johan Commelin]

@Arien Malec if you are updating the wiki, please leave templates for the porting notes, which should mention dsimp in the case of rfl proofs.

[Arien Malec]

Current text added:

If you get a simp can prove this lint, check if by simp can close the original goal and consider removing the simp attribute to address the lint. Put porting comments to indicate the change. If the original proof is rfl, check if by dsimp can close the goal. If not, do not remove the simp, instead add a nolint simpNF (and again, document the decision via porting notes). In some cases, the path to simp can prove this is very complicated or nonsensical - in such cases ask for guidance on the Zulip.

[Arien Malec]

Oops. forgot the template. Will fix.

[Arien Malec]

Template porting notes: "-- porting notes: removed simp attribute as simp can already prove this" OR "-- porting notes: retained simp as dsimp can not prove this" or "-- porting notes: retained simp as [...reasons...]"

[Johan Commelin]

I would prefer the templates that I suggested on the PR:

• -- @[simp] -- Porting note: simp can prove this -- if proof is not rfl
• -- @[simp] -- Porting note: dsimp can prove this -- if proof is rfl
• @[simp, nolint simpNF] -- Porting note: dsimp can not prove this -- if proof is rfl

[Eric Wieser]

Presumably in the cases where mathlib3 already contains a comment that says "for dsimp", we don't need the last one?