Zulip Chat Archive

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:50):

using linear maps gives you also access to certain lemmas

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

Kenny Lau (Oct 28 2020 at 23:21):

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?

Kenny Lau (Oct 28 2020 at 23:27):

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

Eric Wieser (Feb 05 2021 at 10:53):

Follow up thread, with everything working


Last updated: Dec 20 2023 at 11:08 UTC