## Stream: general

### Topic: What's missing from dfinsupp / simp here?

#### Eric Wieser (Oct 28 2020 at 22:05):

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 (Oct 28 2020 at 22:07):

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

#### Eric Wieser (Oct 28 2020 at 22:30):

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 (Oct 28 2020 at 22:47):

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 (Oct 28 2020 at 22:47):

you might also want to make the definitions better like this

#### Kenny Lau (Oct 28 2020 at 22:47):

i.e. don't use dfinsupp.sum

#### Kenny Lau (Oct 28 2020 at 22:47):

because direct_sum (should) have its own API

#### Kenny Lau (Oct 28 2020 at 22:47):

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

#### Kenny Lau (Oct 28 2020 at 22:48):

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

#### Kenny Lau (Oct 28 2020 at 22:51):

I think zero_mul follows immediately from linear_map.map_zero

#### Eric Wieser (Oct 28 2020 at 23:01):

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

#### Eric Wieser (Oct 28 2020 at 23:01):

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

#### Eric Wieser (Oct 28 2020 at 23:04):

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 (Oct 28 2020 at 23:05):

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

#### Kenny Lau (Oct 28 2020 at 23:05):

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

#### Kenny Lau (Oct 28 2020 at 23:06):

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 (Oct 28 2020 at 23:10):

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

#### Eric Wieser (Oct 28 2020 at 23:16):

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

#### Eric Wieser (Oct 28 2020 at 23:16):

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

#### Kenny Lau (Oct 28 2020 at 23:17):

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

#### Eric Wieser (Oct 28 2020 at 23:17):

Right, that was just an implementation question

#### Eric Wieser (Oct 28 2020 at 23:21):

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

right

#### Eric Wieser (Oct 28 2020 at 23:26):

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

yes

#### Eric Wieser (Oct 28 2020 at 23:30):

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

#### Yury G. Kudryashov (Oct 28 2020 at 23:31):

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

#### Yury G. Kudryashov (Oct 28 2020 at 23:32):

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

#### Eric Wieser (Oct 28 2020 at 23:32):

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 (Oct 29 2020 at 09:02):

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

#### Eric Wieser (Oct 29 2020 at 09:15):

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 (Oct 29 2020 at 17:32):

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 (Oct 30 2020 at 19:01):

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 (Jan 27 2021 at 17:55):

@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