Zulip Chat Archive

Stream: general

Topic: simp lemma not firing


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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 α]?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Apr 09 2020 at 20:41):

lean#181


Last updated: May 08 2021 at 04:14 UTC