Zulip Chat Archive

Stream: maths

Topic: linear algebra over semirings & semimodules


view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Apr 12 2020 at 03:39):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 27 2020 at 21:07):

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

view this post on Zulip Kevin Buzzard (May 27 2020 at 21:08):

We broke the pi barrier

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (May 27 2020 at 21:13):

I think the widget PR is almost done, yes.

view this post on Zulip 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 : ι),
          @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

view this post on Zulip Gabriel Ebner (May 27 2020 at 21:27):

It looks like another instance of lean#244

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 28 2020 at 00:24):

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

view this post on Zulip Yury G. Kudryashov (May 28 2020 at 00:25):

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

view this post on Zulip Mario Carneiro (May 28 2020 at 00:26):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 28 2020 at 09:05):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 28 2020 at 09:12):

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

view this post on Zulip Johan Commelin (May 28 2020 at 09:12):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 28 2020 at 10:03):

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

view this post on Zulip 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,

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Johan Commelin (May 28 2020 at 11:25):

@maintainers How are we going to review this?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 28 2020 at 12:01):

I've made a first pass over the diff.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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