simp and abbrev

Stream: mathlib4

[Yury G. Kudryashov]

When does simp unfold abbrevs? I don't have an #mwe right now, but I have a code, where simp fails to simplify (ContinuousLinearMap.comp g f).det even though docs#ContinuousLinearMap.det is an abbrev. Adding ContinuousLinearMap.det to the arguments of simp makes it work.

[Aaron Liu]

simp doesn't unfold abbrevs, it sees through them

[Jakub Nowak]

If you want simp to unfold definition you have to mark definition with @[simp]. abbrev in the context of simp I think boils down to telling simp that it should use simp lemmas about body of an abbrev to also simplify the definition. E.g. if you have abbrev foo .. := bar .. then the simp will use lemmas like bar .. ↔ something to simplify foo, or lemmas like bar .. → something_else to prove something_else from foo ...

[Aaron Liu]

I'm guessing you have something like this?

def A : Type := sorry
def A.comp (g f : A) : A := sorry
def A.det (f : A) : Nat := sorry

def B : Type := sorry
def B.toA (f : B) : A := sorry
def B.comp (g f : B) : B := sorry
@[simp] theorem B.toA_comp (g f : B) : (g.comp f).toA = g.toA.comp f.toA := sorry
abbrev B.det (f : B) : Nat := f.toA.det

example (g f : B) : (g.comp f).det = 0 := by
  fail_if_success simp
  guard_target =ₛ (g.comp f).det = 0
  unfold B.det
  guard_target =ₛ (g.comp f).toA.det = 0
  simp
  guard_target =ₛ (g.toA.comp f.toA).det = 0
  sorry

[Aaron Liu]

To me since I know how simp works this is somewhat expected but I can see how it would be unintuitive/confusing

[Yury G. Kudryashov]

So, it doesn't see through them well enough to apply B.toA_comp in this context, right? What are the practical recommendations then? Drop the abbrev? Turn it into a def and mirror API?

[Jakub Nowak]

I think you either have to mirror API or mark it with @[simp]? But the former is preferred usually. I think this is similar to e.g. Vector. We could just simp Vector.map f xs to Vector.mk (Array.map f xs.toArray), and then all the verification API about Array.map would apply. But we don't do that and instead mirror verification API about .map. There are plenty of examples like that.

[Yury G. Kudryashov]

In some cases, simp can see through an abbrev and apply a theorem about the underlying definition. While the rules are trivial for defs, they aren't as clear (at least, to me) for abbrevs.

[Yury G. Kudryashov]

For me, this part of the manual suggests that abbrevs should be regarded as syntactic sugar by most of the core tactics.

[Yury G. Kudryashov]

If the current behavior (don't apply B.toA_comp in the example above) is the expected behavior, then it should be better documented.

[Jakub Nowak]

I think what happens here is that given goal (g.comp f).det = 0 Lean will try to search for theorems that match (g.comp f).toA.det, and of course it fails. But because simp doesn't unfold the definition it won't recurse into subexpressions of unfolded definition.

[Yury G. Kudryashov]

While this looks like a plausible explanation, I think that the behavior should be clearly documented.

[Jakub Nowak]

Yup, I was also confused about simp "not working" with abbrev. Still somehow am. Tbh, even understanding the principles still doesn't really help in answering the question when and how should abbrev be used when programming or designing API.