assumptions in big_operators

Stream: general

[Johan Commelin]

I was browsing through big_operators and found:

#print finset.sum_nat_cast
-- gives
theorem finset.sum_nat_cast : ∀ {α : Type u} {β : Type v} [_inst_1 : comm_monoid β] [_inst_2 : add_comm_monoid β] [_inst_3 : has_one β]
(s : finset α) (f : α → ℕ), ↑(sum s f) = sum s (λ (a : α), ↑(f a)) :=
λ {α : Type u} {β : Type v} [_inst_1 : comm_monoid β] [_inst_2 : add_comm_monoid β] [_inst_3 : has_one β]
(s : finset α) (f : α → ℕ), eq.symm (sum_hom coe nat.cast_zero nat.cast_add)

Is this bad? I assume [_inst_1 : comm_monoid β] [_inst_2 : add_comm_monoid β] is not intended.

[Kevin Buzzard]

How does Lean know that the up-arrows mean "coerce to beta"?

[Johan Commelin]

I don't know. Probably nat.cast

[Chris Hughes]

Johan just posted the output of #print. In the actual theorem, the type is given explicitly

[Johan Commelin]

Sorry, I could have been clearer about that...

[Johan Commelin]

Is there a way to see if this happens more often in mathlib?

[Johan Commelin]

Chris, you can probably use your tools to figure out if this theorem is actually ever used.

[Johan Commelin]

I predict it isn't. Because otherwise this double instance problem would have been noticed before.

[Patrick Massot]

I'm not sure. As I already pointed out, there are theorems with redundant instances in mathlib

[Kevin Buzzard]

Johan just posted the output of #print. In the actual theorem, the type is given explicitly

Oh -- I'm an idiot. Thanks Chris.

[Johan Commelin]

@Patrick Massot hmmm... can your tools help to discover this? Of course not very automatically. But maybe generate a list of all theorems that assume [blah X] and [add_blah X]. I guess it almost never happens that this is intended.

[Patrick Massot]

doing this is in my long TODO list, but it's very low priority

[Chris Hughes]

Searching sum_nat_cast in VScode tells me it's used once in probability mass function. It's casting to $\mathbb{R}$ there, so no problems synthesizing the comm_monoid instance. It is a mistake though and should be changed.