## Stream: maths

### Topic: linear algebra over semirings & semimodules

#### Yury G. Kudryashov (Apr 12 2020 at 03:39):

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 (Apr 12 2020 at 03:39):

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

#### Sebastien Gouezel (May 27 2020 at 21:04):

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 (May 27 2020 at 21:07):

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

#### Kevin Buzzard (May 27 2020 at 21:08):

We broke the pi barrier

#### Gabriel Ebner (May 27 2020 at 21:08):

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 (May 27 2020 at 21:10):

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 (May 27 2020 at 21:11):

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

#### Gabriel Ebner (May 27 2020 at 21:13):

I think the widget PR is almost done, yes.

#### Gabriel Ebner (May 27 2020 at 21:25):

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 : ι),
(@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_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 (May 27 2020 at 21:27):

It looks like another instance of lean#244

#### Gabriel Ebner (May 27 2020 at 21:54):

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

#### Yury G. Kudryashov (May 28 2020 at 00:24):

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

#### Yury G. Kudryashov (May 28 2020 at 00:25):

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

#### Mario Carneiro (May 28 2020 at 00:26):

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

#### Sebastien Gouezel (May 28 2020 at 09:02):

@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 (May 28 2020 at 09:03):

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 (May 28 2020 at 09:04):

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

#### Johan Commelin (May 28 2020 at 09:05):

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

#### Sebastien Gouezel (May 28 2020 at 09:06):

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 (May 28 2020 at 09:06):

@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 (May 28 2020 at 09:10):

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 (May 28 2020 at 09:12):

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

#### Johan Commelin (May 28 2020 at 09:12):

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

#### Johan Commelin (May 28 2020 at 09:40):

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


#### Johan Commelin (May 28 2020 at 10:02):

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


#### Johan Commelin (May 28 2020 at 10:03):

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

#### Scott Morrison (May 28 2020 at 10:04):

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

#### Johan Commelin (May 28 2020 at 10:05):

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

#### Sebastien Gouezel (May 28 2020 at 10:39):

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

#### Johan Commelin (May 28 2020 at 11:25):

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

#### Johan Commelin (May 28 2020 at 11:25):

@maintainers How are we going to review this?

#### Sebastien Gouezel (May 28 2020 at 11:37):

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 (May 28 2020 at 11:44):

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 (May 28 2020 at 12:01):

I've made a first pass over the diff.

#### Johan Commelin (May 28 2020 at 12:01):

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 (May 28 2020 at 12:02):

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 (May 28 2020 at 12:02):

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

Last updated: May 10 2021 at 23:11 UTC