Combination of `finsupp` and `dfinsupp`

Stream: general

[Antoine Labelle]

The following is not found by apply_instance. What's the easiest way to prove it?

import linear_algebra.dfinsupp

variables (R : Type*) [add_comm_monoid R]
variables {ι : Type*} (α : ι → Type*)

example : add_comm_monoid (Π₀ i, (α i →₀ R)) := sorry

[Heather Macbeth]

@Antoine Labelle This is a common problem with the direct sum. The instance is there, docs#dfinsupp.add_comm_monoid, but doesn't elaborate for some reason.

[Heather Macbeth]

My usual workaround is to write a bunch of rubbish with @ to help Lean find it ... not sure if there's a better way.

[Adam Topaz]

In this case you could also use docs#direct_sum

[Adam Topaz]

import linear_algebra.dfinsupp
import linear_algebra.direct_sum.finsupp

variables (R : Type*) [add_comm_monoid R]
variables {ι : Type*} (α : ι → Type*)

open_locale direct_sum

example : add_comm_monoid (⨁ (i : ι), ⨁ (j : α i), R) := infer_instance

noncomputable
example : add_comm_monoid (⨁ (i : ι), α i →₀ R) := infer_instance

[Adam Topaz]

(which is defined with dfinsupp btw)

[Adam Topaz]

One sec, let me fix that code with the proper notation (fixed)

[Antoine Labelle]

@Adam Topaz I also asked a question about the use of direct_sum versus dfinsupp (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/direct_sum.20vs.20dfinsup), so if you want to explain what direct_sum does differently I would be interested.

[Eric Wieser]

Instead of adding a bunch of @s to help lean find it, you can also track down which instance it is that lean can't find, and add instance : the_missing_one := @the_existing_one _ _ _ ...

[Riccardo Brasca]

As a mathematician, I would say we should add all these instances, and use direct_sum in doing mathematics.

[Eric Wieser]

I think there are infinitely many such missing instances, so at best we can add them as we need them

[Eric Wieser]

I think Lean 4 fixes the bug causing the issue

[Antoine Labelle]

I tried adding the instance used by docs#dfinsupp.add_comm_monoid, but I get weird problems when I try to do this for modules. In the following code, the two definitions compile correctly but the second haveI in tactic environment fails. Any ideas?

import linear_algebra.dfinsupp

variables (R : Type*) [semiring R]
variables {ι : Type*} (α : ι → Type*)

noncomputable
def example1 : Π i, add_comm_monoid (α i →₀ R) := λ i, by apply_instance

noncomputable
def example2 : Π i, module R (α i →₀ R) := λ i, by apply_instance

include R ι α

example : true :=
begin
  -- The second line fails, but it succeeds if I remove the first line.
  haveI : Π i, add_comm_monoid (α i →₀ R) := λ i, by apply_instance,
  haveI : Π i, module R (α i →₀ R) := λ i, by apply_instance,
end

[Yaël Dillies]

What happens if you replace the first haveI by letI?

[Antoine Labelle]

It works, thanks!

[Eric Wieser]

You should replace both!

[Anne Baanen]

The technical reason is that haveI, like lemma, forgets the definition, so it's like assuming each add_comm_monoid (α i →₀ R) has some random unknown add_comm_monoid structure. letI remembers that the add_comm_monoid structure actually derives from finsupp.

[Anne Baanen]

Basically, use haveI only with classes that live in Prop.

[Antoine Labelle]

I see, thanks for the explanation.

[Yaël Dillies]

Anne Baanen said:

Basically, use haveI only with classes that live in Prop.

This is a valid rule when proving a lemma, but the real rule is more "Use haveI unless you want to access the definition" because letI adds a let binding which will mess your defeq if you're constructing a definition.