Making a definition a `simp` lemma

Stream: mathlib4

[Etienne Marion]

Hi! I have a definition which I would like to be reduced by simp. Does it make sense (namely does it exist in Mathlib) to have a simp lemma which simply unfolds the definition? Something like this:

import Mathlib

variable {ι : Type*} {X : ι → Type*}

def proj (s : Finset ι) (x : (i : ι) → X i) (i : s) : X i := x i

@[simp]
lemma proj_eq (s : Finset ι) : proj (X := X) s = fun x i ↦ x i := rfl

[Violeta Hernández]

If that's what you want to do, you should make proj an abbrev instead

[Violeta Hernández]

I believe that makes it so that simp can "see through" it

[Etienne Marion]

Well I thought so, but it does not work

[Etienne Marion]

Here is an example, it all happens in the have block:

import Mathlib

variable {ι : Type*} {X : ι → Type*}


abbrev proj (s : Finset ι) (x : (i : ι) → X i) (i : s) : X i := x i

-- @[simp]
-- lemma proj_eq (s : Finset ι) : proj (X := X) s = fun x i ↦ x i := rfl

def cylinder (s : Finset ι) (S : Set ((i : s) → X i)) : Set ((i : ι) → X i) := proj s ⁻¹' S

@[simp]
theorem mem_cylinder (s : Finset ι) (S : Set (∀ i : s, X i)) (f : (i : ι) → X i) :
    f ∈ cylinder s S ↔ proj s f ∈ S :=
  Set.mem_preimage

example [h_nonempty : Nonempty ((i : ι) → X i)] (s : Finset ι) (S : Set ((i : s) → X i))
    (f : (i : s) → X i) (hf : f ∈ S) : cylinder s S ≠ ∅ := by
  classical
  let f' : (i : ι) → X i := fun i ↦ if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
  have : f' ∈ cylinder s S := by
    rw [mem_cylinder]
    -- simp? [proj, f'] -- suggests simp only [f'] and does not unfold proj
    unfold proj
    simp only [Finset.coe_mem, ↓reduceDIte, f']
    exact hf
  sorry

[Kyle Miller]

Etienne Marion said:

Does it make sense (namely does it exist in Mathlib) to have a simp lemma which simply unfolds the definition?

Yes, you can have proj_eq be a @[simp] lemma. There are some places where @[simp] is right on the definition, but you'll have to see whether it unfolds the definition the way you want.

If it's worth being a definition, and you want to unfold it immediately, there's a question of whether it's worth having the definition at all.

[Etienne Marion]

Thanks for the answers. I tried putting @[simp] on the def but it doesn't work. I definitely think this definition is worth for what I'm doing, because it gives nice interactions with other things I defined and it avoids a lot of type ascription. However I'm still not sure if I want it to be automatically simplified.

An other way would be that rw [proj]or simp [proj] would unfold the definition, but it does not, even when I make it an abbrev or I put a @[reducible]. Is it normal?

[Etienne Marion]

In fact it looks like simp [proj] will work with proj x i, but not with proj x.

[Kyle Miller]

If putting @[simp] directly on a def doesn't give the correct formulation (as you see, it wants it to be fully applied) then you need to put @[simp] on a custom-written lemma, like you originally had.

[Kyle Miller]

There's also simp (config := { unfoldPartialApp := true }) [proj], which might work here, but that's more inconvenient than simp [proj_def].

[Kyle Miller]

By the way, what putting @[simp] on a definition effectively does is make all the foo.eq_NNN theorems into simp lemmas. We can see what the equation theorem is using #check:

def proj (s : Finset ι) (x : (i : ι) → X i) (i : s) : X i := x i

#check proj.eq_1
/-
proj.eq_1.{u_1, u_2} {ι : Type u_1} {X : ι → Type u_2}
    (s : Finset ι) (x : (i : ι) → X i) (i : { x // x ∈ s }) :
  proj s x i = x ↑i
-/

There can be more than one for definitions made using pattern matching.

[Kyle Miller]

In the future there might be a way to adjust the equation theorem, but I believe this is currently a very-low-priority feature.

[Etienne Marion]

I see, thanks a lot for these explanations!