Why doesn't this loop?

Stream: general

[Gabriel Ebner]

My newest linter tells me that this lemma is bad:

@[simp] lemma finset.filter_congr_decidable {α} (s : finset α) (p : α → Prop) (h : decidable_pred p)
  [_inst : decidable_pred p] : @filter α p h s = @filter α p (λ a, _inst a) s :=
by congr

I would have expected that this lemma would cause nontermination, since the left-hand side matches the right-hand side. But it doesn't. git blames @Floris van Doorn: how does this work? Bonus question: if I change λ a, _inst a to _inst, then it doesn't rewrite at all. Why?!

[Gabriel Ebner]

Ah, found the explanation: https://github.com/leanprover-community/mathlib/pull/1477#discussion_r327315504

[Patrick Massot]

Does it mean the linter should change?

[Floris van Doorn]

Yeah, when I added this, it looked pretty dangerous, but after some experiments, Lean seems to handle simp-lemmas like these well, and only applies them when they actually change something in the goal. Ideally the linter should be fine with simp-lemmas like these. We could add simp-lemmas like these for other cases where we might find the "wrong" instance of a type-class (if the typeclass is a subsingleton).

[Gabriel Ebner]

The linter (#2045) now handles this trick correctly, I've even added a test for it: https://github.com/leanprover-community/mathlib/commit/76f6cba857e893a49c5dc0880fe97d6ec3bf3c29#diff-931415e3cdd2239495b8753332fb7fefR21-R43