Zulip Chat Archive

Stream: general

Topic: finsupp.has_scalar


view this post on Zulip Johan Commelin (Mar 16 2021 at 19:11):

In LTE I'm hitting goals of the form

smul_with_zero.to_has_scalar = finsupp.has_scalar

Should docs#finsupp.has_scalar be removed, now that we have smul_with_zero?

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:22):

Those don't really sound interchangable to me

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:23):

Does refl not close that?

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:23):

Ah, but the typeclass argument on that instance should now be relaxed from semimodule to smul_with_zero

view this post on Zulip Johan Commelin (Mar 16 2021 at 19:27):

refl doesn't have the slightest intention of closing this goal :sad:

view this post on Zulip Johan Commelin (Mar 16 2021 at 19:29):

If you are interested in seeing where these come from, see polyhedral_lattice/finsupp.lean in the polyhedral-basis branch of LTE

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:34):

Would you mind showing it with pp.all?

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:34):

Sorry, just pp.implicit is enough

view this post on Zulip Johan Commelin (Mar 16 2021 at 19:40):

Voila:

@smul_with_zero.to_has_scalar  (ι →₀ Λ)
      (@add_monoid.to_has_zero (ι →₀ Λ)
         (@add_comm_monoid.to_add_monoid (ι →₀ Λ)
            (@add_comm_group.to_add_comm_monoid (ι →₀ Λ)
               (@normed_group.to_add_comm_group (ι →₀ Λ) (@finsupp.normed_group ι Λ _inst_3 _inst_2)))))
      (@mul_zero_class.to_has_zero 
         (@monoid_with_zero.to_mul_zero_class  (@semiring.to_monoid_with_zero  nat.semiring)))
      (@mul_action_with_zero.to_smul_with_zero  (ι →₀ Λ)
         (@add_monoid.to_has_zero (ι →₀ Λ)
            (@add_comm_monoid.to_add_monoid (ι →₀ Λ)
               (@add_comm_group.to_add_comm_monoid (ι →₀ Λ)
                  (@normed_group.to_add_comm_group (ι →₀ Λ) (@finsupp.normed_group ι Λ _inst_3 _inst_2)))))
         (@semiring.to_monoid_with_zero  nat.semiring)
         (@semimodule.to_mul_action_with_zero  (ι →₀ Λ) nat.semiring
            (@add_comm_group.to_add_comm_monoid (ι →₀ Λ)
               (@normed_group.to_add_comm_group (ι →₀ Λ) (@finsupp.normed_group ι Λ _inst_3 _inst_2)))
            (@add_comm_monoid.nat_semimodule (ι →₀ Λ)
               (@add_comm_group.to_add_comm_monoid (ι →₀ Λ)
                  (@normed_group.to_add_comm_group (ι →₀ Λ) (@finsupp.normed_group ι Λ _inst_3 _inst_2)))))) =
    @finsupp.has_scalar ι Λ  nat.semiring
      (@add_comm_group.to_add_comm_monoid Λ (@normed_group.to_add_comm_group Λ (@to_normed_group Λ _inst_2)))
      (@add_comm_monoid.nat_semimodule Λ
         (@add_comm_group.to_add_comm_monoid Λ (@normed_group.to_add_comm_group Λ (@to_normed_group Λ _inst_2))))

view this post on Zulip Johan Commelin (Mar 16 2021 at 19:40):

ouch... lean could do a better job at linebreaks )-; there, that looks better

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:46):

nat_semimodule is the culprit here

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:49):

Every "compound" type built out of additive monoids gets two nat-module structures; one elementwise (as this is how all other semimodule structures are inherited), and one derived from addition (which itself is elementwise)

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:49):

These are rarely defeq

view this post on Zulip Johan Commelin (Mar 16 2021 at 19:51):

So we should kill the one coming from addition, right?

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:52):

I'm beginning to think so

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:52):

Or put it in a locale at least

view this post on Zulip Johan Commelin (Mar 16 2021 at 19:52):

Maybe that just shouldn't be a global instance

view this post on Zulip Johan Commelin (Mar 16 2021 at 19:52):

exactly

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:52):

Along with the one for int and rat

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:52):

And the algebras for the same

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:53):

But a lot of lemmas will then need to assume [semimodule \N M], which you could argue is mathematically redundant

view this post on Zulip Johan Commelin (Mar 16 2021 at 19:53):

Well... will it really be a lot?

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:55):

I'm less concerned about the cost of changing them, and more concerned about mathematicians thinking "this is stupid, why am I telling lean my additive monoid had a nat-module structure" and being told "it's an implementation detail"

view this post on Zulip Eric Wieser (Mar 16 2021 at 19:57):

It's all a bit annoying, because we have a proof that all these structures are equivalent, but it's not enough unless they're also defeq

view this post on Zulip Johan Commelin (Mar 16 2021 at 20:06):

Well, at least for semimodule nat M we know it's a subsingleton.

view this post on Zulip Johan Commelin (Mar 16 2021 at 20:07):

But for has_scalar nat M that's obviously not true.

view this post on Zulip Eric Wieser (Mar 16 2021 at 20:08):

Right, but I think in this case both instances are derived from semimodules, and somehow lean can't see that?

view this post on Zulip Johan Commelin (Mar 16 2021 at 20:11):

finsupp.has_scalar is not projecting out of a semimodule instance on finsupp, right?

view this post on Zulip Eric Wieser (Mar 16 2021 at 20:16):

Hmm, good point; the "project out of semimodule" path is lower priority

view this post on Zulip Sebastien Gouezel (Mar 16 2021 at 20:22):

What happens if you lower a lot the piority of the bad nat semimodule instance (setting it to 10 or whatever)?

view this post on Zulip Eric Wieser (Mar 16 2021 at 20:31):

I suspect there are few if any situations where that would actually help

view this post on Zulip Eric Wieser (Mar 16 2021 at 20:32):

But it wouldn't do any harm

view this post on Zulip Sebastien Gouezel (Mar 16 2021 at 20:33):

Normally, it means that the other instances should be found before, so I am curious what this gives in Johan's specific situation.

view this post on Zulip Eric Wieser (Mar 16 2021 at 20:56):

In my experience the usual cause is using nat's smul in a lemma statement about a general M, which has no other instances so chooses nat.semimodule, but then applying it to a compound type like M := prod N P which has a different instance.

view this post on Zulip Sebastien Gouezel (Mar 16 2021 at 21:15):

Does this mean that, just like for [decidable ...], we should just assume [semimodule \N E]in the lemmas that mention some nat multiplication. But the user is still free to use the nsmul multiplication if he likes.

view this post on Zulip Eric Wieser (Mar 16 2021 at 21:23):

Yes, that's what I'm thinking

view this post on Zulip Eric Wieser (Mar 16 2021 at 21:23):

At which point, we may as well just hide the global instance behind a locale

view this post on Zulip Johan Commelin (Mar 17 2021 at 06:57):

local attribute [-instance] add_comm_monoid.nat_semimodule add_comm_group.int_module

solves all the issues

view this post on Zulip Johan Commelin (Mar 17 2021 at 06:58):

But now I do use the following definition:

class polyhedral_lattice (Λ : Type*) extends normed_group Λ :=
-- unfortunately, we need the following assumptions, for technical reasons
[nat_semimodule : semimodule  Λ]
[int_semimodule : semimodule  Λ]
[is_scalar_tower : is_scalar_tower   Λ]
-- now we get to the actual definition
(finite_free : finite_free Λ)
(polyhedral [] :  (ι : Type) [fintype ι] (l : ι  Λ), generates_norm l)

view this post on Zulip Johan Commelin (Mar 17 2021 at 06:58):

Which seems slightly awkward

view this post on Zulip Johan Commelin (Mar 17 2021 at 07:13):

There is now just one place at the API boundary where I need

  have ffΛ : finite_free Λ := polyhedral_lattice.finite_free,
  have oops : @polyhedral_lattice.int_semimodule Λ _ = @add_comm_group.int_module Λ _,
  { exact subsingleton.elim _ _ },
  rw oops at ffΛ,

view this post on Zulip Johan Commelin (Mar 17 2021 at 07:13):

So with a more principled refactor, I guess those could also be removed

view this post on Zulip Eric Wieser (Mar 17 2021 at 07:25):

Shouldn't those be arguments not fields?

view this post on Zulip Johan Commelin (Mar 17 2021 at 07:27):

Then I can't use bundled to build the category

view this post on Zulip Eric Wieser (Mar 17 2021 at 07:27):

How do we bundle things like modules and algebras today, which also take multiple arguments?

view this post on Zulip Johan Commelin (Mar 17 2021 at 07:28):

By hand: https://github.com/leanprover-community/mathlib/blob/master/src/algebra/category/Algebra/basic.lean#L28

view this post on Zulip Eric Wieser (Mar 17 2021 at 07:31):

I feel like that's probably the better approach

view this post on Zulip Eric Wieser (Mar 17 2021 at 07:32):

But admittedly more work


Last updated: May 08 2021 at 03:17 UTC