# Zulip Chat Archive

## Stream: general

### Topic: assumptions in big_operators

#### Johan Commelin (Oct 02 2018 at 13:12):

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 (Oct 02 2018 at 13:21):

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

#### Johan Commelin (Oct 02 2018 at 13:22):

I don't know. Probably `nat.cast`

#### Chris Hughes (Oct 02 2018 at 13:25):

Johan just posted the output of `#print`

. In the actual theorem, the type is given explicitly

#### Johan Commelin (Oct 02 2018 at 13:30):

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

#### Johan Commelin (Oct 02 2018 at 13:30):

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

#### Johan Commelin (Oct 02 2018 at 13:30):

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

#### Johan Commelin (Oct 02 2018 at 13:30):

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

#### Patrick Massot (Oct 02 2018 at 13:31):

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

#### Kevin Buzzard (Oct 02 2018 at 13:31):

Johan just posted the output of

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

#### Johan Commelin (Oct 02 2018 at 13:36):

@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 (Oct 02 2018 at 13:41):

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

#### Chris Hughes (Oct 02 2018 at 13:46):

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.

Last updated: Dec 20 2023 at 11:08 UTC