Zulip Chat Archive

Stream: mathlib4

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


Arien Malec (Jan 13 2023 at 19:27):

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 (Jan 13 2023 at 19:29):

yes, If and only if the original proof is rfl

Johan Commelin (Jan 13 2023 at 19:29):

Otherwise the test is whether by simp closes the proof

Arien Malec (Jan 13 2023 at 19:30):

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 (Jan 13 2023 at 19:31):

In all cases, leave a Porting note

Johan Commelin (Jan 13 2023 at 19:32):

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

Johan Commelin (Jan 13 2023 at 19:33):

@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 (Jan 13 2023 at 19:40):

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 (Jan 13 2023 at 19:41):

Oops. forgot the template. Will fix.

Arien Malec (Jan 13 2023 at 19:46):

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 (Jan 13 2023 at 19:48):

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 (Jan 13 2023 at 19:50):

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


Last updated: Dec 20 2023 at 11:08 UTC