Having to unfold abbrev for simp to work

Stream: general

[Daniel Weber]

From what I understand, simp is supposed to be able to see through the definition of abbrevs. However, in the following example, the unfold line is necessary, and without it simp doesn't work. What am I missing?

import Mathlib.SetTheory.Ordinal.Arithmetic

universe u

def Nimber : Type (u+1) := Ordinal.{u}

def toOrdinal (x : Nimber.{u}) : Ordinal.{u} := x
def toNimber (x : Ordinal.{u}) : Nimber.{u} := x

abbrev ordinalPow (a : Nimber) (b : ℕ) : Nimber := toNimber (toOrdinal a ^ b)

instance : One Nimber where one := toNimber 1
@[simp]
lemma toNimber_one : toNimber 1 = 1 := rfl

lemma ordinalPow_zero (a : Nimber) : ordinalPow a 0 = 1 := by
  unfold ordinalPow -- HERE
  simp only [pow_zero, toNimber_one]

[Chris Bailey]

Simp seems to work if I open this in the playground:

import Mathlib.SetTheory.Ordinal.Arithmetic

universe u

def Nimber : Type (u+1) := Ordinal.{u}

def toOrdinal (x : Nimber.{u}) : Ordinal.{u} := x
def toNimber (x : Ordinal.{u}) : Nimber.{u} := x

abbrev ordinalPow (a : Nimber) (b : ℕ) : Nimber := toNimber (toOrdinal a ^ b)

instance : One Nimber where one := toNimber 1
@[simp]
lemma toNimber_one : toNimber 1 = 1 := rfl

lemma ordinalPow_zero (a : Nimber) : ordinalPow a 0 = 1 := by
  simp only [ordinalPow, pow_zero, toNimber_one]

[Daniel Weber]

Yes, if you give it ordinalPow, but I made it an abbrev exactly to avoid having to tell simp to unfold it

[Chris Bailey]

I see what you mean now. I wasn't under the impression that abbrev automatically added something to the simp set, did you read that somewhere?

[Daniel Weber]

I don't want it to unfold it, just to see through it when applying lemmas