## Stream: general

### Topic: simp lemma not firing

#### Markus Himmel (Apr 09 2020 at 16:25):

I need some assistance with a simp lemma not firing. Unfortunately, I understand too little about the problem (actually, I don't understand anything) to create a MWE, but the problematic lemma is at the arrow_category branch on mathlib (oleans should be available via leanproject, I think). The problematic lemma is in category_theory/limits/shapes/images.lean on line 325.

An example where the lemma does not fire is in line 375: simp only [image.map_comp_eq_comp_map] does not work, while rw image.map_comp_eq_comp_map does.

The simp linter also complains about this lemma with "Left-hand side does not simplify. You need to debug this yourself using set_option trace.simplify.rewrite true", but I can't seem to get that trace option to print anything interesting and I have no idea where to go from here, so any help would be appreciated.

#### Gabriel Ebner (Apr 09 2020 at 18:58):

Oh, the help from the linter is a bit misleading. You need to set set_option trace.simplify true then you also get information about lemmas that did not rewrite.

#### Gabriel Ebner (Apr 09 2020 at 18:58):

2. [simplify.failure] fail to instantiate emetas: 'category_theory.limits.image.map_comp_eq_comp_map' at
@image.map C 𝒞 f h _inst_1 _inst_4 (sq ≫ sq') _inst_6
partially instantiated lemma:
@image.map_comp_eq_comp_map C 𝒞 f g _inst_1 ?x_5 sq ?x_7 h _inst_4 sq' ?x_11 _inst_6


#### Gabriel Ebner (Apr 09 2020 at 19:13):

I think this is a bug in the simplifier, minimum wrecking example:

class A (α : Type)
class B (α : Type) [A α]

def P (α : Type) : Prop := true

@[simp] lemma foo (α : Type) [A α] [B α] : P α ↔ true := iff.rfl

-- fails
example (α : Type) [A α] [B α] : P α ↔ true := by simp only [foo]


#### Yury G. Kudryashov (Apr 09 2020 at 19:15):

It seems that foo has unused arguments. Does it work if P has arguments [A α] and [B α]?

#### Gabriel Ebner (Apr 09 2020 at 19:17):

Imagine that B is used in the proof. It will work if P has an argument for [B α] because then the argument to the simp lemma is filled in by unification.

#### Markus Himmel (Apr 09 2020 at 19:27):

Gabriel Ebner said:

Imagine that B is used in the proof. It will work if P has an argument for [B α] because then the argument to the simp lemma is filled in by unification.

Very interesting, thank you for looking into this. I'm still confused though, because what you said sounds like this bug should not trigger when the statement of the simp lemma in question already uses all arguments, but I believe that for image.map_comp_eq_comp_map, the statement does in fact already use all of the arguments.

#### Gabriel Ebner (Apr 09 2020 at 20:41):

lean#181

Last updated: May 08 2021 at 04:14 UTC