dfinsupp/finsupp type class issue

Stream: general

[Kevin Buzzard]

The discussion about type class inference going on here

https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/sigma_finsupp_to_dfinsupp/near/241170315

isn't really relevant to that stream. Here's what's going on:

import linear_algebra.dfinsupp

variables {ι : Type*} {R : Type*} {η : ι → Type*} {N : Type*}
variables [semiring R] [add_comm_monoid N] [module R N]

-- to see the traces uncomment this

--set_option trace.class_instances true

-- this fails

example : add_comm_monoid (Π₀ (i : ι), η i →₀ N) := by apply_instance -- fails

/-
Here's a part of the trace (click on "apply_instance"):

[class_instances] (0) ?x_0 : add_comm_monoid (Π₀ (i : ι), η i →₀ N) :=
  @dfinsupp.add_comm_monoid ?x_38 ?x_39 ?x_40
failed is_def_eq

??
-/

local attribute [-instance]
 finsupp.has_zero
 finsupp.add_zero_class
 finsupp.add_monoid

--set_option trace.class_instances true
noncomputable example : add_comm_monoid (Π₀ (i : ι), η i →₀ N) := by apply_instance -- works

/-

Part of the trace:

[class_instances] (0) ?x_0 : add_comm_monoid (Π₀ (i : ι), η i →₀ N) := @dfinsupp.add_comm_monoid ?x_38 ?x_39 ?x_40
[class_instances] caching instance for add_comm_monoid (Π₀ (i : ι), η i →₀ N)
@dfinsupp.add_comm_monoid ι (λ (i : ι), η i →₀ N) (λ (i : ι), @finsupp.add_comm_monoid (η i) N _inst_2)
-/

[Kevin Buzzard]

Now mathlib-free (and addition-free!):

class add_zero_class (M : Type) extends has_zero M.

variables {ι : Type} {N : Type} {η : ι → Type} (β : ι → Type)

structure dfinsupp [Π i, has_zero (β i)] : Type :=
(to_fun : Π i, β i)

instance dfinsupp.has_zero {ι : Type} {β : ι → Type} [Π (i : ι), has_zero (β i)] :
  has_zero (dfinsupp (λ i, β i)) := ⟨⟨λ _, 0⟩⟩

instance dfinsupp.add_zero_class [Π i, add_zero_class (β i)] :
  add_zero_class (dfinsupp (λ i, β i)) :=
{ zero      := 0 }

structure finsupp (α : Type) (M : Type) [has_zero M] :=
(to_fun             : α → M)

instance finsupp.has_zero (α : Type) (M : Type) [has_zero M] :
  has_zero (finsupp α M) := ⟨⟨λ i, 0⟩⟩

instance finsupp.add_zero_class (α : Type) (M : Type) [add_zero_class M] :
  add_zero_class (finsupp α M) :=
{ zero      := 0 }

example [add_zero_class N] : add_zero_class (dfinsupp (λ (i : ι), finsupp (η i) N)) :=
  by apply_instance -- fails

local attribute [-instance] finsupp.has_zero
-- now it works

example [add_zero_class N] : add_zero_class (dfinsupp (λ (i : ι), finsupp (η i) N)) :=
by apply_instance

What is mathlib doing wrong here?

[Sebastien Gouezel]

Can you also do the Lean 4 analogue? If it also fails in Lean 4, we could ask the devs if something can be done about it. And if it works, great!

[Kevin Buzzard]

Here's the Lean 3 trace. You can see failed is_def_eq failing but then succeeding with a definitionally equal problem. I'll try it in Lean 4.

example [add_zero_class N] : add_zero_class (dfinsupp (λ (i : ι), finsupp (η i) N)) :=
  by apply_instance -- fails
/-
[class_instances] (0) ?x_0 : add_zero_class
  (@dfinsupp ι (λ (i : ι), @finsupp (η i) N (@add_zero_class.to_has_zero N _inst_1))
     (λ (i : ι), @finsupp.has_zero (η i) N (@add_zero_class.to_has_zero N _inst_1))) := @dfinsupp.add_zero_class ?x_4 ?x_5 ?x_6
failed is_def_eq
-/
local attribute [-instance] finsupp.has_zero
-- now it works

example [add_zero_class N] : add_zero_class (dfinsupp (λ (i : ι), finsupp (η i) N)) :=
by apply_instance
/-
[class_instances] (0) ?x_0 : add_zero_class
  (@dfinsupp ι (λ (i : ι), @finsupp (η i) N (@add_zero_class.to_has_zero N _inst_1))
     (λ (i : ι),
        @add_zero_class.to_has_zero (@finsupp (η i) N (@add_zero_class.to_has_zero N _inst_1))
          (@finsupp.add_zero_class (η i) N _inst_1))) := @dfinsupp.add_zero_class ?x_4 ?x_5 ?x_6
[class_instances] caching instance for add_zero_class...
-/

example [add_zero_class N] : (@dfinsupp ι (λ (i : ι), @finsupp (η i) N (@add_zero_class.to_has_zero N _inst_1))
     (λ (i : ι), @finsupp.has_zero (η i) N (@add_zero_class.to_has_zero N _inst_1))) =
(@dfinsupp ι (λ (i : ι), @finsupp (η i) N (@add_zero_class.to_has_zero N _inst_1))
     (λ (i : ι),
        @add_zero_class.to_has_zero (@finsupp (η i) N (@add_zero_class.to_has_zero N _inst_1))
          (@finsupp.add_zero_class (η i) N _inst_1))) := rfl

[Riccardo Brasca]

Wow, thank you Kevin!! This looks deeper than I expected...

[Sebastien Gouezel]

The first trace you're showing is failing with @finsupp.add_zero_class, while the second one succeeds but with @dfinsupp.add_zero_class. I guess you wanted to tell us that the first one also fails with the dfinsupp version?

[Kevin Buzzard]

oh that is probably a typo on my part (I copied the wrong thing, let me check). Update: yes, I copied the wrong line. I fixed it now.

[Kevin Buzzard]

I couldn't get it to work in Lean 4 either.

[Riccardo Brasca]

I don't have time today to think about it, but in #7818 something even stranger happened. I was proving

local attribute [-instance] finsupp.has_zero

/-- `finsupp.split` is an additive equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
@[simps]
def sigma_finsupp_add_equiv_dfinsupp [add_zero_class N] : ((Σ i, η i) →₀ N) ≃+ (Π₀ i, (η i →₀ N)) :=
{ to_fun := sigma_finsupp_equiv_dfinsupp,
  inv_fun := sigma_finsupp_equiv_dfinsupp.symm,
  map_add' := λ f g, by {ext, refl},
  .. sigma_finsupp_equiv_dfinsupp }

that worked very well. Then @Eric Wieser suggested to have map_add' as an isolated lemma, so I wanted to prove

local attribute [-instance] finsupp.has_zero

lemma sigma_finsupp_equiv_dfinsupp_add [add_zero_class N] (f g : (Σ i, η i) →₀ N) :
  (sigma_finsupp_equiv_dfinsupp (f + g) : Π₀ i, (η i →₀ N)) = (sigma_finsupp_equiv_dfinsupp f) +
  (sigma_finsupp_equiv_dfinsupp g) :=

/-- `finsupp.split` is an additive equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
@[simps]
def sigma_finsupp_add_equiv_dfinsupp [add_zero_class N] : ((Σ i, η i) →₀ N) ≃+ (Π₀ i, (η i →₀ N)) :=
{ to_fun := sigma_finsupp_equiv_dfinsupp,
  inv_fun := sigma_finsupp_equiv_dfinsupp.symm,
  map_add' := λ f g, by {ext, refl},
  .. sigma_finsupp_equiv_dfinsupp }

The strange thing is that I get the failed to synthesize type class instance for error about has_add (Π₀ (i : ι), η i →₀ N) in sigma_finsupp_equiv_dfinsupp_add, but still sigma_finsupp_add_equiv_dfinsupp just below works.

[Riccardo Brasca]

A simpler example

local attribute [-instance] finsupp.has_zero

variables [add_zero_class N] (f g : (Σ i, η i) →₀ N)

example : has_add (Π₀ (i : ι), η i →₀ N) := by apply_instance -- works

#check (sigma_finsupp_equiv_dfinsupp f) --Π₀ (i : ι), η i →₀ N

#check (sigma_finsupp_equiv_dfinsupp f) + (sigma_finsupp_equiv_dfinsupp g) --fails

[Eric Wieser]

What if you add an explicit type ascription to the failing check? (Maybe to both operands)

[Eric Wieser]

I think sometimes that forces lean to redo a typeclass search

[Riccardo Brasca]

Ah, #check ((sigma_finsupp_equiv_dfinsupp f) + (sigma_finsupp_equiv_dfinsupp g) : (Π₀ (i : ι), η i →₀ N)) works!

[Eric Wieser]

I think I had to do this higher up in the file you're working in

[Riccardo Brasca]

But smul is different

example [add_comm_monoid N] [module R N] : has_scalar R (Π₀ i, (η i →₀ N)) := by apply_instance --fails

example [add_comm_monoid N] [module R N] : has_scalar R (Π₀ i, (η i →₀ N)) := dfinsupp.has_scalar --OK

-- no problem here
/-- `finsupp.split` is a linear equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
@[simps]
def sigma_finsupp_lequiv_dfinsupp [add_comm_monoid N] [module R N] :
  ((Σ i, η i) →₀ N) ≃ₗ[R] (Π₀ i, (η i →₀ N)) :=
{ map_smul' := λ r f, by {ext, refl},
  .. sigma_finsupp_add_equiv_dfinsupp }

[Eric Wieser]

I assume you run into trouble again if you try to declare a standalone smul lemma?

[Riccardo Brasca]

Yes, that's what I was trying to do

[Eric Wieser]

Your snippet above doesn't show that attempt

[Riccardo Brasca]

example [add_comm_monoid N] [module R N] : has_scalar R (Π₀ i, (η i →₀ N)) := by apply_instance --fails

example [add_comm_monoid N] [module R N] : has_scalar R (Π₀ i, (η i →₀ N)) := dfinsupp.has_scalar --OK

--this fails
@[simp]
lemma sigma_finsupp_equiv_dfinsupp_smul [add_comm_monoid N] [module R N] (r : R)
  (f : (Σ i, η i) →₀ N) : sigma_finsupp_equiv_dfinsupp (r • f) =
  r • (sigma_finsupp_equiv_dfinsupp f : (Π₀ (i : ι), η i →₀ N)) :=
by {ext, refl}

/-- `finsupp.split` is a linear equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
@[simps]
def sigma_finsupp_lequiv_dfinsupp [add_comm_monoid N] [module R N] :
  ((Σ i, η i) →₀ N) ≃ₗ[R] (Π₀ i, (η i →₀ N)) :=
{ map_smul' := λ r f, by {ext, refl},
  .. sigma_finsupp_add_equiv_dfinsupp }

In the add lemma both examples worked :thinking:

[Eric Wieser]

What if you relax module to distrib_mul_action?

[Eric Wieser]

module is only needed for the bundled map

[Riccardo Brasca]

This works

example [add_comm_monoid N] [module R N] : distrib_mul_action R (Π₀ i, (η i →₀ N)) := by apply_instance

[Eric Wieser]

I mean replace module R N

[Eric Wieser]

Since docs#dfinsupp.distrib_mul_action doesn't need it

[Eric Wieser]

Oh...

[Eric Wieser]

You need #7664 for that to work

[Riccardo Brasca]

Ah yes, that doesn't work but indeed the lemma is really missing

[Eric Wieser]

Does attribute [-instance] dfinsupp.distrib_mul_action dfinsupp.has_scalar help?

[Eric Wieser]

To force it to find the module instance

[Riccardo Brasca]

Hmm...

example [add_comm_monoid N] [module R N] : module R (Π₀ i, (η i →₀ N)) := by apply_instance

works, even without local attribute [-instance] dfinsupp.distrib_mul_action dfinsupp.has_scalar. But has_scalar does not.

[Riccardo Brasca]

And has_scalar doesn't work even with local attribute [-instance] dfinsupp.distrib_mul_action dfinsupp.has_scalar.

[Eric Wieser]

This works:

@[simp]
lemma sigma_finsupp_equiv_dfinsupp_smul [add_comm_monoid N] [module R N] (r : R)
  (f : (Σ i, η i) →₀ N) :
  sigma_finsupp_equiv_dfinsupp (r • f) =
  @has_scalar.smul R (Π₀ i, η i →₀ N) mul_action.to_has_scalar r (sigma_finsupp_equiv_dfinsupp f) :=
by { ext, refl }

[Eric Wieser]

Typeclass search shows that it while trying to satisfy finsupp.distrib_mul_action it ends up rejecting module.to_distrib_mul_action

[Eric Wieser]

I think i'm seeing a similar issue to this one in #7834