simp lemma not firing

Stream: general

[Markus Himmel]

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]

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]

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]

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]

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

[Gabriel Ebner]

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]

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]

lean#181