Alias of Prop type instances

Stream: mathlib4

[Jiang Jiedong]

Hi everyone,

I was trying to create some deprecated alias after renaming. The CI complains

/- The `defLemma` linter reports:
INCORRECT DEF/LEMMA: -/
-- Mathlib.Algebra.Group.Units.Hom
Error: ././././Mathlib/Algebra/Group/Units/Hom.lean:252:1: error: @MonoidHom.isLocalRingHom_comp is a def, should be lemma/theorem

The code is like this, where IsLocalHom takes values in Prop

instance MonoidHom.isLocalHom_comp (g : S →* T) (f : R →* S) [IsLocalHom g]
    [IsLocalHom f] : IsLocalHom (g.comp f) where
  map_nonunit a := IsLocalHom.map_nonunit a ∘ IsLocalHom.map_nonunit (f := g) (f a)

@[deprecated (since := "2024-10-10")]
alias MonoidHom.isLocalRingHom_comp := MonoidHom.isLocalHom_comp

Is this a bug? When creating an alias for Prop valued instances, it will be treated as def and further trigger the defLemma linter.

[Yaël Dillies]

Yes, that's a bug. But it's not the fault of alias. Instead, instance creates defs regardless of whether the typeclass is Prop- or Type-valued

[Jiang Jiedong]

Yes, but without alias, the defLemma linter does not complain. So maybe the true solution is that we should fix instances? (not alias nor linter)

[Jiang Jiedong]

I think for my PR I'll just drop these deprecated alias for instances.

[Matthew Ballard]

Silencing the linter seems to be the kick-the-can solution currently

[Jiang Jiedong]

And shall I write an issue in the GitHub page of Mathlib for this?

[Yaël Dillies]

There is already an issue on the lean4 repo

[Yaël Dillies]

Actually, I don't find it :thinking:

[Jiang Jiedong]

How to see whether a declaration (instance) is a def or a theorem?

[Jiang Jiedong]

I was trying to write a new issue but don't know the way to exhibit this def-or-theorem difference.

[Markus Himmel]

import Lean.Elab.Command

open Lean

class A : Prop

instance a : A where

/-- info: it's a definition -/
#guard_msgs in
run_meta do
  if let .defnInfo _ ← getConstInfo `a then
    logInfo "it's a definition"

[Kyle Miller]

Yaël Dillies said:

Actually, I don't find it :thinking:

It would be nice if someone reported this!

[Jiang Jiedong]

I opened lean#5672 to report this.

[Eric Wieser]

Does writing @[instance] theorem fix the problem for now?

[Jiang Jiedong]

Eric Wieser said:

Does writing @[instance] theorem fix the problem for now?

Yes, that would fix the problem.

[Jiang Jiedong]

Thank you! I've adopted this solution in my PR.

[Edward van de Meent]

Jiang Jiedong said:

How to see whether a declaration (instance) is a def or a theorem?

give it a name and use #print

[Eric Wieser]

Or hover over the word instance to find the generated name

[Junyan Xu]

The issue has been resolved by lean#5856