finsupp.has_scalar

Stream: general

[Johan Commelin]

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?

[Eric Wieser]

Those don't really sound interchangable to me

[Eric Wieser]

Does refl not close that?

[Eric Wieser]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Eric Wieser]

Would you mind showing it with pp.all?

[Eric Wieser]

Sorry, just pp.implicit is enough

[Johan Commelin]

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

[Johan Commelin]

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

[Eric Wieser]

nat_semimodule is the culprit here

[Eric Wieser]

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)

[Eric Wieser]

These are rarely defeq

[Johan Commelin]

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

[Eric Wieser]

I'm beginning to think so

[Eric Wieser]

Or put it in a locale at least

[Johan Commelin]

Maybe that just shouldn't be a global instance

[Johan Commelin]

exactly

[Eric Wieser]

Along with the one for int and rat

[Eric Wieser]

And the algebras for the same

[Eric Wieser]

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

[Johan Commelin]

Well... will it really be a lot?

[Eric Wieser]

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"

[Eric Wieser]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Sebastien Gouezel]

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

[Eric Wieser]

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

[Eric Wieser]

But it wouldn't do any harm

[Sebastien Gouezel]

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

[Eric Wieser]

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.

[Sebastien Gouezel]

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.

[Eric Wieser]

Yes, that's what I'm thinking

[Eric Wieser]

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

[Johan Commelin]

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

solves all the issues

[Johan Commelin]

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)

[Johan Commelin]

Which seems slightly awkward

[Johan Commelin]

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Λ,

[Johan Commelin]

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

[Eric Wieser]

Shouldn't those be arguments not fields?

[Johan Commelin]

Then I can't use bundled to build the category

[Eric Wieser]

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

[Johan Commelin]

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

[Eric Wieser]

I feel like that's probably the better approach

[Eric Wieser]

But admittedly more work