[Merged by Bors] - refactor(algebra/module): change module into an abbreviation for semimodule #2848

sgouezel · 2020-05-28T08:44:21Z

The file algebra/module.lean contains the lines

There were several attempts to make `module` an abbreviation of `semimodule` but this makes
  class instance search too hard for Lean 3.

It turns out that this was too hard for Lean 3 until recently, but this is not too hard for Lean 3.14. This PR removes these two lines, and changes the files accordingly.

This means that the basic objects of linear algebra are now semimodules over semiring, making it possible to talk about matrices with natural number coefficients or apply general results on multilinear maps to get the binomial or the multinomial formula.

A linear map is now defined over semirings, between semimodules which are add_comm_monoids. For some statements, you need to have an add_comm_group, and a ring or a comm_semiring or a comm_ring. I have not tried to lower the possible typeclass assumptions like this in all files, but I have done it carefully in the following files:

algebra/module
linear_algebra/basic
linear_algebra/multilinear
topology/algebra/module
topology/algebra/multilinear

Other files can be optimised later in the same way when needed, but this PR is already big enough.

I have also fixed the breakage in all the other files. It was sometimes completely mysterious (in tensor products, I had to replace several times linear_map.id.flip with linear_map.flip linear_map.id), but globally all right. I have tweaked a few instance priorities to make sure that things don't go too bad: there are often additional steps in typeclass inference, going from ring to semiring and from add_comm_group to add_comm_monoid, so I have increased their priority (putting it strictly between 100 and 1000), and adjusted some other priorities to get more canonical instance paths, fixing some preexisting weirdnesses (notably in multilinear maps). One place where I really had to help Lean is with normed spaces of continuous multilinear maps, where instance search is just too big.

I am aware that this will be a nightmare to refer, but as often with big refactor it's an "all or nothing" PR, impossible to split in tiny pieces.

The old behaviour caused `eq.mpr`'s in `pi_instance` output.

jcommelin

Looks very good to me. Thanks for doing this 🎉

I've flagged places where the instance priority is changed. This is something that we might want to discuss a bit.
I've also flagged places where proofs "downgraded". (Many proofs have moved around, so I probably didn't catch all of these cases.) We might want to discuss/investigate.

jcommelin · 2020-05-28T11:42:52Z

src/analysis/calculus/times_cont_diff.lean

@@ -138,6 +138,9 @@ open_locale classical

 universes u v w

+local attribute [instance, priority 1001]


I can't comment on whether this is a good setting. I don't understand the priorities well enough, so I would like a second pair of eyes here.

jcommelin · 2020-05-28T11:43:28Z

src/analysis/convex/basic.lean

-    (⇑((@finset.univ _ hs.fintype).sum (λ x, (linear_map.proj x : (s → ℝ) →ₗ[ℝ] ℝ).smul_right x.1))) ''
-      (@std_simplex _ hs.fintype) :=
+    (⇑((@finset.univ _ hs.fintype).sum
+      (λ x, (@linear_map.proj ℝ s _ (λ i, ℝ) _ _ x).smul_right x.1))) ''


This seems unfortunate.

jcommelin · 2020-05-28T11:43:59Z

src/analysis/normed_space/basic.lean

@@ -670,13 +670,15 @@ by rw [← rat.norm_cast_real, ← int.norm_cast_real]; congr' 1; norm_cast
 section normed_space

 section prio
-set_option default_priority 100 -- see Note [default priority]
-- see Note[vector space definition] for why we extend `module`.
+set_option default_priority 920 -- see Note [default priority]. Here, we set a rather high priority,


Second pair of eyes please.

jcommelin · 2020-05-28T11:44:45Z

src/algebra/ring.lean

+definitions are given in terms of semirings, but many applications use rings or fields. We increase
+a little bit its priority above 100 to try it quickly, but remaining below the default 1000 so that
+more specific instances are tried first. -/
+attribute [instance, priority 200] ring.to_semiring


Looks good to me. But flagging this so that other reviewers can easily find it.

jcommelin · 2020-05-28T11:45:21Z

src/analysis/normed_space/multilinear.lean

@@ -57,6 +57,8 @@ noncomputable theory
 open_locale classical
 open finset

+local attribute [instance, priority 1001]


Second pair of eyes please.

jcommelin · 2020-05-28T11:47:44Z

src/linear_algebra/finsupp.lean

 begin
-  show is_linear_map R ((lsubtype_domain s : (α →₀ M) →ₗ[R] (s →₀ M)).comp
-      (submodule.subtype (supported M R s))),
+  let F : (supported M R s) ≃ (s →₀ M) := restrict_support_equiv s M,


This seems unfortunate.

jcommelin · 2020-05-28T11:49:29Z

src/linear_algebra/tensor_product.lean

@@ -366,8 +369,10 @@ theorem ext_threefold {g h : (M ⊗[R] N) ⊗[R] P →ₗ[R] Q}
 begin
  let e := linear_equiv.to_equiv (lift.equiv R (M ⊗[R] N) P Q),
  apply e.symm.injective,
-  ext x y z,
-  exact H x y z,
+  refine ext _,


Do we need to tag something with @[ext] to fix this?

jcommelin · 2020-05-28T11:55:06Z

src/algebra/module.lean

@@ -171,6 +198,8 @@ theorem smul_eq_zero {R E : Type*} [division_ring R] [add_comm_group E] [module

 end module

+section
+set_option default_priority 910


Second pair of eyes please.

src/algebra/module.lean

sgouezel · 2020-05-29T09:12:55Z

I had to fix some additional failures after merging master. One of them is the following, in lie_algebra: the proof was

lie_equiv_matrix'.to_morphism.comp (skew_adjoint_lie_subalgebra J.to_bilin_form).incl

and I had to change it to

lie_algebra.morphism.comp (lie_algebra.equiv.to_morphism lie_equiv_matrix')
  (skew_adjoint_lie_subalgebra J.to_bilin_form).incl

So, exactly the same proof, but without the dot notation. I already had to make several changes with the same flavor when fixing the library, for instance going from linear_map.id.flip to linear_map.flip linear_map.id several times. I don't know if this is worth investigating, or if it was to be expected.

jcommelin · 2020-05-30T13:50:46Z

Thanks 🎉

bors merge

bors · 2020-05-30T13:52:08Z

Canceled.

jcommelin · 2020-05-30T13:52:41Z

bors merge

bors · 2020-05-30T14:02:34Z

Merge conflict.

jcommelin · 2020-05-30T15:16:15Z

🥺

bors merge

bors · 2020-05-30T16:17:05Z

Canceled.

rwbarton · 2020-05-30T16:18:26Z

bors merge

…module (#2848) The file `algebra/module.lean` contains the lines ``` There were several attempts to make `module` an abbreviation of `semimodule` but this makes class instance search too hard for Lean 3. ``` It turns out that this was too hard for Lean 3 until recently, but this is not too hard for Lean 3.14. This PR removes these two lines, and changes the files accordingly. This means that the basic objects of linear algebra are now semimodules over semiring, making it possible to talk about matrices with natural number coefficients or apply general results on multilinear maps to get the binomial or the multinomial formula. A linear map is now defined over semirings, between semimodules which are `add_comm_monoid`s. For some statements, you need to have an `add_comm_group`, and a `ring` or a `comm_semiring` or a `comm_ring`. I have not tried to lower the possible typeclass assumptions like this in all files, but I have done it carefully in the following files: * `algebra/module` * `linear_algebra/basic` * `linear_algebra/multilinear` * `topology/algebra/module` * `topology/algebra/multilinear` Other files can be optimised later in the same way when needed, but this PR is already big enough. I have also fixed the breakage in all the other files. It was sometimes completely mysterious (in tensor products, I had to replace several times `linear_map.id.flip` with `linear_map.flip linear_map.id`), but globally all right. I have tweaked a few instance priorities to make sure that things don't go too bad: there are often additional steps in typeclass inference, going from `ring` to `semiring` and from `add_comm_group` to `add_comm_monoid`, so I have increased their priority (putting it strictly between 100 and 1000), and adjusted some other priorities to get more canonical instance paths, fixing some preexisting weirdnesses (notably in multilinear maps). One place where I really had to help Lean is with normed spaces of continuous multilinear maps, where instance search is just too big. I am aware that this will be a nightmare to refer, but as often with big refactor it's an "all or nothing" PR, impossible to split in tiny pieces. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

bors · 2020-05-30T18:01:24Z

Pull request successfully merged into master.

Build succeeded:

…module (leanprover-community#2848) The file `algebra/module.lean` contains the lines ``` There were several attempts to make `module` an abbreviation of `semimodule` but this makes class instance search too hard for Lean 3. ``` It turns out that this was too hard for Lean 3 until recently, but this is not too hard for Lean 3.14. This PR removes these two lines, and changes the files accordingly. This means that the basic objects of linear algebra are now semimodules over semiring, making it possible to talk about matrices with natural number coefficients or apply general results on multilinear maps to get the binomial or the multinomial formula. A linear map is now defined over semirings, between semimodules which are `add_comm_monoid`s. For some statements, you need to have an `add_comm_group`, and a `ring` or a `comm_semiring` or a `comm_ring`. I have not tried to lower the possible typeclass assumptions like this in all files, but I have done it carefully in the following files: * `algebra/module` * `linear_algebra/basic` * `linear_algebra/multilinear` * `topology/algebra/module` * `topology/algebra/multilinear` Other files can be optimised later in the same way when needed, but this PR is already big enough. I have also fixed the breakage in all the other files. It was sometimes completely mysterious (in tensor products, I had to replace several times `linear_map.id.flip` with `linear_map.flip linear_map.id`), but globally all right. I have tweaked a few instance priorities to make sure that things don't go too bad: there are often additional steps in typeclass inference, going from `ring` to `semiring` and from `add_comm_group` to `add_comm_monoid`, so I have increased their priority (putting it strictly between 100 and 1000), and adjusted some other priorities to get more canonical instance paths, fixing some preexisting weirdnesses (notably in multilinear maps). One place where I really had to help Lean is with normed spaces of continuous multilinear maps, where instance search is just too big. I am aware that this will be a nightmare to refer, but as often with big refactor it's an "all or nothing" PR, impossible to split in tiny pieces. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

urkud and others added 26 commits April 3, 2020 01:03

fix(tactic/interactive): don't unfold non-Prop goals

c394815

The old behaviour caused `eq.mpr`'s in `pi_instance` output.

add a test file

4113461

move test

b3b9572

actually move test

cab90db

Merge branch 'master' into refine-struct

5874739

Update test/refine_struct.lean

61b5534

attempt to remove module

29fb1b1

Merge remote-tracking branch 'upstream/refine-struct' into remove_module

07e60a8

Merge remote-tracking branch 'upstream/master' into remove_module

2e8bea4

cleanup

2f875ef

cleanup

15655b0

fix dfinsupp

39a0639

merge master

b4e63d8

beginning to clean up the mess

4d7229c

clean up all the mess

683232e

tweak priorities

207be63

clean pi_instance

b384938

linting

24f3d4f

Merge remote-tracking branch 'upstream/master' into remove_module

2fd8cd8

fix build

108e0d5

more implicit parameters in pi instances

d38a1c5

play with instances

5181c8b

temporary workaround to have a working build

5588d58

tweak priorities

e0db676

move lemma around

084ea40

cleanup

d56cefe

sgouezel added the awaiting-review The author would like community review of the PR label May 28, 2020

jcommelin reviewed May 28, 2020

View reviewed changes

semorrison reviewed May 28, 2020

View reviewed changes

src/algebra/module.lean Outdated Show resolved Hide resolved

urkud reviewed May 28, 2020

View reviewed changes

src/algebra/module.lean Outdated Show resolved Hide resolved

urkud reviewed May 28, 2020

View reviewed changes

src/algebra/module.lean Outdated Show resolved Hide resolved

urkud reviewed May 28, 2020

View reviewed changes

src/algebra/module.lean Show resolved Hide resolved

urkud reviewed May 28, 2020

View reviewed changes

src/algebra/module.lean Outdated Show resolved Hide resolved

sgouezel added 4 commits May 28, 2020 22:48

urkud's comments

cafb0a7

Merge remote-tracking branch 'upstream/master' into remove_module

f5bf607

revert structure, fix new failures

5a88032

an sich -> as such

f29d957

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 30, 2020

Merge branch 'master' into remove_module

778e562

Merge branch 'master' into remove_module

99c50dd

fix merge

0d59187

bors bot changed the title ~~refactor(algebra/module): change module into an abbreviation for semimodule~~ [Merged by Bors] - refactor(algebra/module): change module into an abbreviation for semimodule May 30, 2020

bors bot closed this May 30, 2020

bors bot deleted the remove_module branch May 30, 2020 18:01

eric-wieser mentioned this pull request Jul 21, 2020

[Merged by Bors] - feat(data/dfinsupp): Relax requirements of semimodule conversion to add_comm_monoid #3490

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(algebra/module): change module into an abbreviation for semimodule #2848

[Merged by Bors] - refactor(algebra/module): change module into an abbreviation for semimodule #2848

sgouezel commented May 28, 2020

jcommelin left a comment

jcommelin May 28, 2020

jcommelin May 28, 2020

jcommelin May 28, 2020

jcommelin May 28, 2020

jcommelin May 28, 2020

jcommelin May 28, 2020

jcommelin May 28, 2020

jcommelin May 28, 2020

sgouezel commented May 29, 2020

jcommelin commented May 30, 2020

bors bot commented May 30, 2020

jcommelin commented May 30, 2020

bors bot commented May 30, 2020

jcommelin commented May 30, 2020

bors bot commented May 30, 2020

rwbarton commented May 30, 2020

bors bot commented May 30, 2020

		@@ -138,6 +138,9 @@ open_locale classical

		universes u v w

		local attribute [instance, priority 1001]

[Merged by Bors] - refactor(algebra/module): change module into an abbreviation for semimodule #2848

[Merged by Bors] - refactor(algebra/module): change module into an abbreviation for semimodule #2848

Conversation

sgouezel commented May 28, 2020

jcommelin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sgouezel commented May 29, 2020

jcommelin commented May 30, 2020

bors bot commented May 30, 2020

jcommelin commented May 30, 2020

bors bot commented May 30, 2020

jcommelin commented May 30, 2020

bors bot commented May 30, 2020

rwbarton commented May 30, 2020

bors bot commented May 30, 2020