What's missing from `dfinsupp` / `simp` here?

Stream: general

[Eric Wieser]

I had a really nasty time writing the proof for mul_assoc in #4812, and kept having to use lots of convert and _ when I'd rather just throw the lemma at simp. My guess is either:

• Something is wrong with the implicitness of the lemma arguments
• simp is bad at dependent rewrites
• dfinsupp is missing some important lemmas that I should be using
• I'm bad at using sensible tactics

Right now, the proof takes multiple minutes, which is rather frustrating. Any suggestions for golfing would be appreciated!

[Kenny Lau]

one of the reasons we went classical is that decidable often times out

[Eric Wieser]

I'll try tomorrow with classical and see if that helps. I assume with classical I can't then compute with my definitions?

[Kenny Lau]

def lmul (i j) : G[i] →ₗ[R] G[j] →ₗ[R] G[i+j] :=
linear_map.mk₂ R (λ gi gj, ⟨gi * gj, G.3 _ _⟩)
  (λ gi₁ gi₂ gj, subtype.eq $ add_mul _ _ _)
  (λ c gi gj, subtype.eq $ algebra.smul_mul_assoc _ _ _)
  (λ gi gj₁ gj₂, subtype.eq $ mul_add _ _ _)
  (λ c gi gj, subtype.eq $ algebra.mul_smul_comm _ _ _)

namespace semiring

@[simps mul]
instance : has_mul G :=
⟨λ x y, (direct_sum.to_module R ι G
  (λ i, (direct_sum.to_module R ι _
    (λ j, (G.lmul j i).compr₂ (direct_sum.lof R ι (λ i, G[i]) (j + i))) :
      G →ₗ[R] G[i] →ₗ[R] G) y) : G →ₗ[R] G) x⟩

@[simps one]
instance : has_one G :=
⟨direct_sum.lof R ι (λ i, G[i]) 0 ⟨1, G.2⟩⟩

/-! These proofs are very slow, so these lemmas are defined separately -/

private lemma one_mul (x : G) : 1 * x = x :=
begin
  rw [has_mul_mul, has_one_one, direct_sum.to_module_lof, ← linear_map.flip_apply],
  conv_rhs { rw ← @linear_map.id_apply R G _ _ _ x },
  refine direct_sum.to_module.ext _ _ _,
  sorry
end

[Kenny Lau]

you might also want to make the definitions better like this

[Kenny Lau]

i.e. don't use dfinsupp.sum

[Kenny Lau]

because direct_sum (should) have its own API

[Kenny Lau]

i.e. you shouldn't need to unfold the definition of direct_sum to see the dfinsupp underneath

[Kenny Lau]

you'll find that direct_sum still has a lot of API to be written

[Kenny Lau]

using linear maps gives you also access to certain lemmas

[Kenny Lau]

I think zero_mul follows immediately from linear_map.map_zero

[Eric Wieser]

I hadn't considered writing it in terms of a bilinear map

[Eric Wieser]

My only concern is it becomes harder to generalize from submodules to submonoids.

[Eric Wieser]

Regarding dfinsupp vs direct_sum, I struggle to really see the intended difference between the APIs - the only one I can think of is that direct_sum probably ought not to have a coe_to_fun

[Kenny Lau]

direct_sum gives you an add_comm_monoid with instructions of how to build a hom to any other add_comm_monoid

[Kenny Lau]

essentially, going to dfinsupp is "working in the wrong category"

[Kenny Lau]

i.e. you're working with add_comm_monoid, so you shouldn't all of a sudden go back to working with sets (i.e. types)

[Eric Wieser]

docs#direct_sum, since Google isn't working and search is too slow on mobile

[Eric Wieser]

Other than providing a bundled hom, is docs#direct_sum.to_group different to docs#dfinsupp.sum?

[Eric Wieser]

I'm surprised they don't seem to share an implementation

[Kenny Lau]

well, as I explained, you shouldn't unfold direct_sum to become dfinsupp

[Eric Wieser]

Right, that was just an implementation question

[Eric Wieser]

Ah, I realize the key takeaway from your linear_map suggestion is that all my proofs of preserving zero and addition vanish, which represent a large amount of the boilerplate

[Kenny Lau]

right

[Eric Wieser]

docs#finsupp.lift_add_hom is the non-dependent version of docs#direct_sum.to_group, right?

[Kenny Lau]

yes

[Eric Wieser]

So arguably there should be a dfinsupp.lift_add_hom too, for which directsum.to_group is just an alias / wrapper?

[Yury G. Kudryashov]

Note that dfinsupp was written before I added lift_add_hom to finsupp.

[Yury G. Kudryashov]

Making API of dfinsupp and finsupp more similar to each other looks like a good idea to me.

[Eric Wieser]

That's good to know. I'm not blaming Kenny at all for the API, just trying to work out how to unify them

[Eric Wieser]

@Yury G. Kudryashov, based on that being a good idea, does #4801 seem fine to you?

[Eric Wieser]

Eric Wieser said:

Other than providing a bundled hom, is docs#direct_sum.to_group different to docs#dfinsupp.sum?

Answer: Yes, to_group uses map_zero to avoid needing decidable instances, which is clever

[Eric Wieser]

Eric Wieser said:

So arguably there should be a dfinsupp.lift_add_hom too, for which directsum.to_group is just an alias / wrapper?

Done in #4821

[Eric Wieser]

Kenny Lau said:

you might also want to make the definitions better like this

I found myself having a really hard time with the bilinear map APIs - I seem to have to aggressively unfold the linear_map compositions in order to get anywhere close to a form I would expect to have a lemma about

[Eric Wieser]

@Kenny Lau, I had another go at your approach in branch#eric-wieser/dadd_monoid_algebra-lmul, but I think overall it was worse just because the API of lsum is smaller than the API of dfinsupp.sum

[Eric Wieser]

Follow up thread, with everything working