Simps and `def`

Stream: mathlib4

[Wrenna Robson]

I can't recall if I've asked this before but it is an issue.

Suppose one has a def which defines a synonym to a structure for some special case. I would like to avoid using abbrev because I don't want this definition to be transparent, but it would be convenient to still generate projections - I want to do this using projection functions defined on my def, though, not the original projection functions defined on the more general type.

I would like to be able to use simps to generate these automatically... and I can: but actually it generates the latter, simps projections using the original (despite using def).

However, I cannot initialize_simps_projections because my def isn't recognised as a struct.

Here's what I think is an MWE.

structure myStruct (n : Nat) where
  foo : Fin n
  bar : Fin n → Fin n

def mySpecificStruct := myStruct 2

@[simps!]
def myMyStructThree : myStruct 3 where
  foo := 0
  bar := (·)

#check Fin.myMyStructThree_foo_val
#check Fin.myMyStructThree_bar

@[simps!]
def myMyStructTwo : myStruct 2 where
  foo := 3
  bar := (· + 1)

#check Fin.myMyStructTwo_foo_val
#check Fin.myMyStructTwo_bar_val

@[simps!]
def myMySpecificStruct : mySpecificStruct where
  foo := 3
  bar := (· + 1)

#check Fin.myMySpecificStruct_foo_val
#check Fin.myMySpecificStruct_bar_val

-- initialize_simps_projections myMySpecificStruct (PANIC)

As you can see, in fact attempting to run initialize_simps_projections myMySpecificStruct causes Lean to crash. But I would still like to use simps in this way! It is causing an actual issue in practice, because when, say, there is an instance of FunLike on both mySpecificStruct and myStruct, the simps projections generated use the latter but you will generally be in the former case when actually applying it - and simps can't see through the def so it gets stuck - i.e. the simps lemmas generated are not useful! It would be alright if one was forbidden from using simps at all here because then it would at least force you to create lemmas manually - it is unintuitive that it silently creates non-useful simps lemmas.

[Floris van Doorn]

I agree that this would be useful to implement.

[Wrenna Robson]

One way I guess would be to use an empty "extends"?

[Wrenna Robson]

But that seems a bit funny