linear algebra over semirings & semimodules

Stream: maths

[Yury G. Kudryashov]

Recently @Sebastien Gouezel tried to make module an abbreviation for semimodule, see branch remove-module. CI build fails in direct_sum_module but a build with -T100000 times out in linear_algebra.basic on comap_smul.

[Yury G. Kudryashov]

Why is it so hard for Lean? Can we help it?

[Sebastien Gouezel]

Finally, I have been able to get rid completely of modules, replacing them by semimodules everywhere, see the branch remove-module which mostly builds -- Lean 3.15 is really awesome, this was completely impossible two months ago. This means you can talk of matrices with natural number coefficients, or apply results on multilinear functions to deduce the binomial formula over naturals numbers.

This is not PRed yet because there is something I don't understand and that I would like to understand. In two files that are hard from the point of view of typeclass search, I had to tweak the priorities to help Lean be faster. What I don't get is around https://github.com/leanprover-community/mathlib/blob/5181c8bf841995e17ede1dfeebb9febcff24c7ac/src/analysis/normed_space/multilinear.lean#L561: I have an instance that fails quickly if I don't tweak the instances, and succeeds quickly if I tweak them. I thought that changing the priorities would only change the speed of success of failure, but here it changes the outcome. Is that normal/expected to you?

[Johan Commelin]

This is amazing! I'm really excited that this is now working!

[Kevin Buzzard]

We broke the pi barrier

[Gabriel Ebner]

It is definitely expected. If there are two instances, we often use priorities to prefer one over the other. (E.g. the two coercions ℕ → ℤ) Priorities can of course also have an effect on success: type class search terminates once a solution has been found. If you had exactly the right priorities, type class search would only need to try one instance. With the wrong priorities, you could make it loop instead.

[Gabriel Ebner]

Sebastien Gouezel said:

Lean 3.15 is really awesome

A minor correction: Lean 3.15 will be very awesome when it is released in the coming days. But we're still at 3.14.

[Bryan Gin-ge Chen]

3.15 will have widget support, right? Or will there be a release before that?

[Gabriel Ebner]

I think the widget PR is almost done, yes.

[Gabriel Ebner]

Re: type class issues. The problem isn't that type class search fails without the problems, it's that the type of the instance you want to derive is different:

example :
normed_group.{(max v u w₂)}
    (@continuous_multilinear_map.{u v u w₂} 𝕜 ι (λ (i : ι), 𝕜) E₂ (λ (a b : ι), _inst_1 a b)
       (@ring.to_semiring.{u} 𝕜
          (@normed_ring.to_ring.{u} 𝕜
             (@normed_field.to_normed_ring.{u} 𝕜 (@nondiscrete_normed_field.to_normed_field.{u} 𝕜 _inst_3))))
       (λ (i : ι),
          @semiring.to_add_comm_monoid.{u} 𝕜
            (@ring.to_semiring.{u} 𝕜
               (@normed_ring.to_ring.{u} 𝕜
                  (@normed_field.to_normed_ring.{u} 𝕜
                     (@nondiscrete_normed_field.to_normed_field.{u} 𝕜 _inst_3)))))
       (@add_comm_group.to_add_comm_monoid.{w₂} E₂ (@normed_group.to_add_comm_group.{w₂} E₂ _inst_7))
       (λ (i : ι),
          @semiring.to_semimodule.{u} 𝕜
            (@ring.to_semiring.{u} 𝕜
               (@normed_ring.to_ring.{u} 𝕜
                  (@normed_field.to_normed_ring.{u} 𝕜
                     (@nondiscrete_normed_field.to_normed_field.{u} 𝕜 _inst_3)))))
       (@normed_space.to_semimodule.{u w₂} 𝕜 E₂ (@nondiscrete_normed_field.to_normed_field.{u} 𝕜 _inst_3)
          _inst_7
          _inst_11)
       (λ (i : ι),
          @uniform_space.to_topological_space.{u} 𝕜
            (@metric_space.to_uniform_space'.{u} 𝕜
               (@normed_field.to_metric_space.{u} 𝕜 (@nondiscrete_normed_field.to_normed_field.{u} 𝕜 _inst_3))))
       (@uniform_space.to_topological_space.{w₂} E₂
          (@metric_space.to_uniform_space'.{w₂} E₂ (@normed_group.to_metric_space.{w₂} E₂ _inst_7))))
:= by apply_instance -- fails even with the priority changed

[Gabriel Ebner]

It looks like another instance of lean#244

[Gabriel Ebner]

BTW, the ∀ i : ι, ... in the type class instances inhibit some heuristic tricks. If they can be easily removed, it would help.

[Yury G. Kudryashov]

I don't think that we can easily remove them when dealing with multilinear forms.

[Yury G. Kudryashov]

Unless we assume that all arguments are of the same type.

[Mario Carneiro]

We could have a typeclass semimodule_family etc but that seems like a pretty big move

[Sebastien Gouezel]

@Gabriel Ebner thanks for the clarification. I have slightly adjusted the priorities globally to make sure that the "right" instance path is favored. PRed in #2848

[Sebastien Gouezel]

Is there a way to see how much this affects performance? Build time by github actions is not very reliable as it starts over from a previous set of oleans, so maybe it doesn't recompile everything. @Scott Morrison , can your build bot check a PR build time?

[Bryan Gin-ge Chen]

You could always temporarily comment out this build step: https://github.com/leanprover-community/mathlib/blob/master/.github/workflows/build.yml#L47

[Johan Commelin]

But we still wouldn't know what to compare it against, right?

[Sebastien Gouezel]

Do you mean that if in the PR I modify this file, then the github action for the PR will use the modified build rules?

[Gabriel Ebner]

@Sebastien Gouezel I wouldn't worry too much about a performance difference. The number one priority is that it works. And the current priorities have been chosen without any big plan, only that they are less than 1000.

[Sebastien Gouezel]

Well, if instance search becomes twice as long in half of the library because of the change, this would be pretty bad, so I'd rather check this.

[Johan Commelin]

@Sebastien Gouezel I can build master and your branch from scratch.

[Johan Commelin]

Master takes ~20 minutes, I think. So I can hopefully give you numbers within 1 hour.

[Johan Commelin]

Building master
configuring mathlib 0.1
> lean --make src
real    20m15.275s
user    225m16.657s
sys     2m19.933s

[Johan Commelin]

Building remove_module
configuring mathlib 0.1
> lean --make src
real    20m52.771s
user    230m25.838s
sys     2m27.667s

[Johan Commelin]

@Sebastien Gouezel :up: It seems to be about 5 minutes longer (on a total of ~225).

[Scott Morrison]

On the other hand, looking at the noise levels from the build bot, there may be no difference at all,

[Johan Commelin]

Yup... I tried to do nothing else on my server, but hey, it's also running a web server etc...

[Sebastien Gouezel]

Thanks for having looked at this. 5 minutes out of 225 is negligible, so I just set #2848 to request review.

[Johan Commelin]

@Sebastien Gouezel What do you think of renaming semimodule to module? (This can certainly be done in a follow-up PR)

[Johan Commelin]

@maintainers How are we going to review this?

[Sebastien Gouezel]

Johan Commelin said:

Sebastien Gouezel What do you think of renaming semimodule to module? (This can certainly be done in a follow-up PR)

Yes, I want to do this, but I decided it would be done in a later PR, to make the current PR less confusing.

[Gabriel Ebner]

Johan Commelin said:

@maintainers How are we going to review this?

LGTM, but I'll let somebody r+ it who's actually used vector spaces.

[Johan Commelin]

I've made a first pass over the diff.

[Johan Commelin]

Whenever instance priorities changed, I left a comment. This should make it very easy for @Mario Carneiro or @Gabriel Ebner to quickly look whether it looks reasonable.

[Johan Commelin]

I've also left comments in some places where proofs became uglier/longer. We can discuss/investigate more, or simply ignore those comments.

[Johan Commelin]

In total, I left 8 comments. I think we can get this merged quickly.