Zulip Chat Archive

Stream: general

Topic: Why doesn't this loop?

Gabriel Ebner (Feb 22 2020 at 20:12):

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 (Feb 22 2020 at 20:16):

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

Patrick Massot (Feb 22 2020 at 20:39):

Does it mean the linter should change?

Floris van Doorn (Feb 24 2020 at 18:26):

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 (Feb 24 2020 at 20:13):

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

Last updated: Aug 03 2023 at 10:10 UTC