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 #print. In the actual theorem, the type is given explicitly

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: May 14 2021 at 03:27 UTC