Zulip Chat Archive

Stream: new members

Topic: trying out a `simp` lemma

Damiano Testa (Apr 12 2021 at 02:52):

Dear All,

what constitutes a good test for trying out a simp lemma? I list below what comes to mind: is there any other "standard" test that you would do?

  • Check that #lint is happy.
  • Make sure that CI is successful with the simp tag.
  • Check that the statement of the new simp lemma can be proven by simp only after you tag the lemma with simp.
  • Modify the statement a bit, in such a way that simp "should prove it" and check that it does.
  • Ask on Zulip?

I have ticked all of the above, except that I am still waiting on CI to finish.

Anything else?


Damiano Testa (Apr 12 2021 at 02:52):

The reason for asking is I would like to tag the lemmas below with simp and Scott suggested to "try it out"!

import algebra.module.basic
import algebra.algebra.basic

@[simp] lemma nat.smul_one_eq_coe {R : Type*} [semiring R] [semimodule  R] (m : ) :
  m  (1 : R) = m :=
by rw [nsmul_eq_smul, nsmul_eq_mul, mul_one]

@[simp] lemma int.smul_one_eq_coe {R : Type*} [ring R] [semimodule  R] (m : ) :
  m  (1 : R) = m :=
by rw [ gsmul_eq_smul, gsmul_eq_mul, mul_one]

@[simp] lemma rat.smul_one_eq_coe {A : Type*} [division_ring A] [algebra  A] (m : ) :
  m  (1 : A) = m :=
by rw [algebra.smul_def, mul_one, ring_hom.eq_rat_cast]

Damiano Testa (Apr 12 2021 at 05:15):

PR #7166

CI was successful with the simp tag for the three lemmas!

Scott Morrison (Apr 12 2021 at 05:36):


Scott Morrison (Apr 12 2021 at 05:38):

(Also, this would be better in general than in new members)

Last updated: Dec 20 2023 at 11:08 UTC